Automatic Abstraction Generation : How to Make an Expert Verification Technique for Security Protocols available to Non-expert Users

Yohan Boichut 1 Pierre-Cyrille Héam 2 Olga Kouchnarenko 2
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 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 : The security problem for protocols with an unbounded number of sessios is in general undecidable. However, a solution may consist of performing reachability analysis on safety-preserving abstractions of security protocols. In order to make this technique available for high level specification languages like HLPSL and PROUVE, we define safe and sound abstractions of protocol transition systems into rewriting systems. These abstractions allow the automated generation of approximation functions to ensure soundness of the reachability analysis. As our main purpose is to automate in so far as possible the analysis of protocols for an unbounded number of sessions, our abstraction/approximation based approach provides an efficient verification tool, TA4SP. This way, the requirement of an expert user can be removed from the verification chain.
Type de document :
Rapport
[Research Report] RR-6039, INRIA. 2006, pp.21
Liste complète des métadonnées

https://hal.inria.fr/inria-00116918
Contributeur : Rapport de Recherche Inria <>
Soumis le : jeudi 30 novembre 2006 - 10:42:38
Dernière modification le : vendredi 16 novembre 2018 - 01:24:06
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:31:24

Fichiers

RR-6039.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00116918, version 2

Citation

Yohan Boichut, Pierre-Cyrille Héam, Olga Kouchnarenko. Automatic Abstraction Generation : How to Make an Expert Verification Technique for Security Protocols available to Non-expert Users. [Research Report] RR-6039, INRIA. 2006, pp.21. 〈inria-00116918v2〉

Partager

Métriques

Consultations de la notice

434

Téléchargements de fichiers

109