OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

UML-based modeling and formal verification of authentication protocols

Fontan, Benjamin and Mota, Sara and Villemur, Thierry and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre UML-based modeling and formal verification of authentication protocols. (2006) In: ICSSE'06 - IEEE International Conference on Secure Software Engineering, March 2006, Washington, United States .

[img] (Document in English)

PDF ( Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > Instituto Tecnologico y de Estudios Superiores de Monterrey - ITESM (MEXICO)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Laboratory name:
Deposited On:12 Mar 2009 09:31

Repository Staff Only: item control page