Developing high-assurance secure systems with UML: a smartcard-based purchase protocol

Developing high-assurance 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. Our aim is to aid the task of developing security-critical systems in an approach based on the notation of the Unified Modeling Language (UML). Towards this aim, we use an extension of UML, called UMLsec, that allows expressing security-relevant information within the diagrams in a system-specification. We present tool-support which has been developed for the UMLsec approach. We apply UMLsec to the example of an electronic purse protocol proposed as a global standard. We demonstrate how to detect some vulnerabilities using our approach, suggest improvements, and show that the improved protocol is secure in a precise sense, by using a tool that implements a formal semantics of a simplified fragment of UML.