Skip to Main content Skip to Navigation

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 7:56:54 PM
Last modification on : Friday, January 21, 2022 - 3:09:49 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:51:39 PM


  • HAL Id : inria-00070291, version 1


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⟩



Record views


Files downloads