Modeling and verifying security protocols using UML 2

Large scale distributed systems often require security protocols to ensure high integrity. We present a modeling approach that uses UML 2 without extensions to support the design, composition and verification of security protocols. The approach assumes a strong threat model, in which an attacker can intercept, modify, and spoof all communications, with the exception of those protected by known-strong encryption. Through a series of models of extensively-studied protocols we demonstrate that the approach allows protocol properties to be accurately represented, and protocols to be automatically tested to detect potential security flaws. The approach benefits from the existing strong tool support for UML 2, allowing automatic generation of protocol implementations from the models.