The Community for Technology Leaders
Ninth IEEE International Symposium on High-Assurance Systems Engineering (HASE'05) (2004)
Tampa, Florida
Mar. 25, 2004 to Mar. 26, 2004
ISSN: 1530-2059
ISBN: 0-7695-2094-4
pp: 231-240
Jan Jürjens , Technical University at München
ABSTRACT
<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>
INDEX TERMS
high assurance systems, security software engineering, security engineering, security verification, formal methods in security, security evaluation, security models, cryptographic protocols, electronic purses
CITATION
Jan Jürjens, "Developing High-Assurance Secure Systems with UML: A Smartcard-Based Purchase Protocol", Ninth IEEE International Symposium on High-Assurance Systems Engineering (HASE'05), vol. 00, no. , pp. 231-240, 2004, doi:10.1109/HASE.2004.1281747
100 ms
(Ver 3.3 (11022016))