In this paper we introduce our model-driven software engineering method, called SecureMDD, which facilitates the development of security-critical applications that are based on cryptographic protocols. The approach seamlessly integrates the generation of code and formal methods. Starting with a platform-independent UML model of a system under development, we generate executable Java (Card) code as well as a formal model from the UML model. Subsequent to this, the formal model is used to verify the security of the modeled system. Our goal is to prove that the generated code is correct w.r.t. the generated formal model in terms of formal refinement. The approach is tailored to the domain of security-critical systems, e.g. smart card applications.

Abstract The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation.

There is a mismatch between the data format used in implementations of security protocols and the data types used in formal verification of security protocols. We present a verified encoding scheme for data used in security protocols, which links the abstract data types of the formal world to a byte format usable in implementations. The encoding is inspired by the ASN1 encoding scheme. The encoding is implemented in Java and the implementation is proven to be correct against a formal specification. The implementation can be used as a reusable reference library in security protocol implementations. The benefit is a separation of concerns: The protocol can be verified on an abstract level. The mapping to bytes is automatically correct by linking the library. Additionally the encoding is a challenging Java verification case study in its own.

This paper presents an approach to the verification of large Java programs. The focus lies on programs that implement a distributed communicating system e.g. in a M- or E-commerce scenario. When trying to verify such programs, thousands of Java classes with tens of thousands of lines of code would have to be taken into consideration. That is impossible. The paper introduces a technique that dramatically reduces the amount of source code that must be considered. Additionally, a suitable method for programming security critical systems is introduced. The reduction is achieved by extracting a verification kernel from the program, which is sufficient for proving the correctness of the relevant part. An algorithm for the automatic computation of the verification kernel has been developed and is presented in the paper. The correctness of the verification kernel approach is proved on the level of the Java language semantics.