FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents an approximation function developed for the verification of cryptographic protocols. The main properties of this approximation are that it can be build automatically and its computation is guaranteed to terminate unlike the Genet and Klay's one. This approximation has been used for the verification of the Needham-Schroeder, Otway-Rees and Woo Lam protocols. To be more precise, the approximation allows us to check secrecy and authenticity properties of the protocols.
https://hal.inria.fr/inria-00071986
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:25:13 PM Last modification on : Friday, January 15, 2021 - 3:24:28 AM Long-term archiving on: : Sunday, April 4, 2010 - 10:47:43 PM
Frédéric Oehl, Gérard Cécé, Olga Kouchnarenko, David Sinclair. Automatic Approximation for the Verification of Cryptographic Protocols. [Research Report] RR-4599, INRIA. 2002, pp.18. ⟨inria-00071986⟩