Automatic Verification of Security Protocols Using Approximations

Yohan Boichut 1 Pierre-Cyrille Héam 1 Olga Kouchnarenko 1
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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Security protocols are widely used in open modern networks to ensure safe communications. It is now recognized that formal analysis can provide the level of assurance required by both developers and users of the protocols. Unfortunately it is generally undecidable to certify whether a protocol is safe or not. However the automatic verification of security protocols can be attempted using abstraction-based approximation. For this purpose, tree automata approximations were introduced by Genet and Klay in 2000. In this paper, we propose an extension of their techniques making the approach efficiently automatic. Our contribution has been implementing in the TA4SP tool with a high level specification language as input format, providing positive practical results on industrial security protocols.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00070291
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 7:56:54 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Sunday, April 4, 2010 - 8:51:39 PM

Identifiers

  • HAL Id : inria-00070291, version 1

Citation

Yohan Boichut, Pierre-Cyrille Héam, Olga Kouchnarenko. Automatic Verification of Security Protocols Using Approximations. [Research Report] RR-5727, INRIA. 2005, pp.27. ⟨inria-00070291⟩

Share

Metrics

Record views

288

Files downloads

182