HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Automatic Approximation for the Verification of Cryptographic Protocols

Frédéric Oehl Gérard Cécé Olga Kouchnarenko 1 David Sinclair
1 CASSIS - Combination of approaches to the security of infinite states systems
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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 7:25:13 PM
Last modification on : Friday, January 21, 2022 - 3:09:04 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:47:43 PM


  • HAL Id : inria-00071986, version 1


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⟩



Record views


Files downloads