Formal Verification of Application-Specific Security Properties in a Model-Driven Approach

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 tins 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.