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.
Keywords : cryptographic protocols automatic approximation verification secrecy authenticity property
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

Files

Vignette du document
RR-4599.pdf

Identifiers

  • HAL Id : inria-00071986, version 1

Collections

INRIA | INRIA-RRRT | CNRS | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LARA | LORIA | UNIV-LORRAINE | LORIA-FM

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

259

Files downloads

680

 

Contact                    Legal Notice                    Personal Data