Sound methods and effective tools for model-based security engineering with UML

Developing security-critical systems is difficult and there are many well-known examples of security weaknesses exploited in practice. Thus a sound methodology supporting secure systems development is urgently needed. We present an extensible verification framework for verifying UML models for security requirements. In particular, it includes various plugins performing different security analyses on models of the security extension UMLsec of UML. Here, we concentrate on an automated theorem prover binding to verify security properties of UMLsec models which make use of cryptography (such as cryptographic protocols). The paper aims to contribute towards usage of UML for secure systems development in practice by offering automated analysis routines connected to popular CASE tools. We present an example of such an application where our approach found and corrected several serious design flaws in an industrial biometric authentication system.