Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

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

Identifiers

  • HAL Id : inria-00071986, version 1

Citation

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⟩

Share

Metrics

Record views

259

Files downloads

680