A Model-Driven Development Method for Secure Applications

Start date: 01.08.2008
End date: 31.10.2012
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local scientists: Wolfgang Reif
Publications: Publication list


SecureMDD is a model-driven approach to develop secure applications.


SecureMDD 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 and web service applications.

The SecureMDD approach is based on our work and experience with the Go!Card project. The SecureMDD project was funded by the Deutsche Forschungsgemeinschaft DFG from 2008 to 2012.


The slides of the SecSE talk give a short overview of the approach.

Case Studies

A tour through several security-critical applications

A short modeling tour of a simple CopyCard example and the generated Java Card code for the example. And the KIV security proofs (uses xml/xsl).

CopyCard with two kinds of terminals (platform-independent model)

CopyCard with two kinds of terminals (platform-specific model)

Mondex electronic purse (with security proofs)

Banking System (with ATM withdrawal and online money transfer between different banks) (with security proofs)

Age Verification


E-Ticket  (and interactive proofs - big)

E-Ticket (with ASLan++ specification and automatic abstractions)

E-Ticket (with ASLan++ specification and manual abstractions)


The German Electronic Health Card (big, with security proofs)