Eighth IEEE International Symposium on High Assurance Systems Engineering, 2004. Proceedings. (2004)
Mar. 25, 2004 to Mar. 26, 2004
Jan Jürjens , Technical University at München
<p>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.</p> <p>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).</p> <p>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.</p>
high assurance systems, security software engineering, security engineering, security verification, formal methods in security, security evaluation, security models, cryptographic protocols, electronic purses
J. Jürjens, "Developing High-Assurance Secure Systems with UML: A Smartcard-Based Purchase Protocol," Eighth IEEE International Symposium on High Assurance Systems Engineering, 2004. Proceedings.(HASE), Tampa, Florida, 2004, pp. 231-240.