UML-based modeling and formal verification of authentication protocols

Authentication protocols are so complex to analyze against intruder attacks, that they deserve to be modeled and verified using formal description techniques. The paper discusses how to model and formally verify authentication protocols using TURTLE, a UML profile based on the formal description technique RT-LOTOS. Joint use of observers and verification by abstraction makes the proposed design method original in the context of authentication protocols. The Needham-Schroeder Public Key (NSPK) Protocol serves as running example. The “Man_in_the_Middle” attack originally identified by Lowe is pointed out in a few seconds without writing any complex formula characterizing the properties to be verified. The paper also includes a corrected version of the NSPK protocol. With its UML editor and formal verification toolkit, the TURTLE modeling language is currently applied to the design of a multicast authentication protocol.