2010 | OriginalPaper | Buchkapitel
Formal Verification of Application-Specific Security Properties in a Model-Driven Approach
verfasst von : Nina Moebius, Kurt Stenzel, Wolfgang Reif
Erschienen in: Engineering Secure Software and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a verification method that allows to prove security for security-critical systems based on cryptographic protocols. Designing cryptographic protocols is very difficult and error-prone and most tool-based verification approaches only consider standard security properties such as secrecy or authenticity. In our opinion, application-specific security properties give better guarantees. In this paper we illustrate how to verify properties that are relevant for e-commerce applications, e.g. ’The provider of a copying service does not lose money’. This yields a more complex security property that is proven using interactive verification. The verification of this kind of application-specific property is part of the SecureMDD approach which provides a method to model a security-critical application with UML and automatically generates executable code as well as a formal specification for interactive verification from the UML models.