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

Handling Algebraic Properties in Automatic Analysis of Security Protocols

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 : This paper extends the approximation-based theoretical framework in which the security problem secrecy preservation against an intruder may be semi-decided through a reachability verification. We explain how to cope with algebraic properties for an automatic approximation-based analysis of security protocols. We prove that if the initial knowledge of the intruder is a regular tree language, then the security problem may by semi-decided for protocols using cryptographic primitives with algebraic properties. More precisely, an automatically generated approximation function enables us 1) an automatic normalization of transitions, and 2) an automatic completion procedure. The main advantage of our approach is that the approximation function makes it possible to verify security protocols with an arbitrary number of sessions. The concepts are illustrated on an example of the view-only protocol using a cryptographic primitive with the exclusive or algebraic property.
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:18:56 PM
Last modification on : Friday, January 21, 2022 - 3:09:49 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:23:17 PM


  • HAL Id : inria-00070169, version 1


Yohan Boichut, Pierre-Cyrille Héam, Olga Kouchnarenko. Handling Algebraic Properties in Automatic Analysis of Security Protocols. [Research Report] RR-5857, INRIA. 2006, pp.18. ⟨inria-00070169⟩



Record views


Files downloads