Modeling Security-Critical Applications with UML in the SecureMDD Approach

Developing security-critical applications is very difficult and the past has shown that many applications turned out to be erroneous after years of usage. For this reason it is desirable to have a sound methodology for developing security-critical applications. We present our approach, called SecureMDD, to model these applications with the unified modeling language (UML) extended by a UML profile to tailor our models to security applications. We automatically generate a formal specification suitable for verification as well as an implementation from the model. Therefore we offer a model-driven development method seamlessly integrating semi-formal and formal methods as well as the implementation. This is a significant advantage compared to other approaches not dealing with all aspects from abstract models down to code. Based on this approach we can prove security properties on the abstract protocol level as well as the correctness of the protocol implementation in Java with respect to the formal model. In this paper we concentrate on the modeling with UML and some details regarding the transformation of this model into the formal specification. We illustrate our approach on an electronic payment system called Mondex. Mondex has become famous for being the target of the first ITSEC evaluation of the highest level E6 which requires formal specification and verification.