Abstracting Security-Critical Applications for Model Checking in a Model-Driven Approach

Model checking at the design level makes it possible to find protocol flaws in security-critical applications automatically. But depending on the size of the application and especially on the abstraction of the application model, model checking may need a lot of resources, primarily time. To reduce the complexity, the application models are usually highly abstracted. But in a model-driven approach with automatic generation of runnable applications the application models need to be detailed and are often too complex to check in reasonable time. In this paper we describe an approach to handle this problem by using additional UML models to restrict the protocol runs, the attacker abilities and the numbers of participants. This makes model checking of large applications in our model-driven approach called SecureMDD possible without manual abstraction of the generated specifications. For model checking we use AVANTSSAR and show how the restrictions modeled within UML are translated. We demonstrate our approach with a smart card based electronic ticketing example.