inria-00116918, version 2
Automatic Abstraction Generation : How to Make an Expert Verification Technique for Security Protocols available to Non-expert Users
N° RR-6039 (2006)
Résumé : 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.
- a – Université Rennes I
- 1 :
- CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1
- 2 :
- INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domaine : Informatique/Cryptographie et sécurité
Informatique/Génie logiciel - Mots-clés : security protocols – safe and sound abstractions – verifications – approximations – abstractions
- Référence interne : RR-6039
- Versions disponibles : v1 (28-11-2006) v2 (30-11-2006)
- inria-00116918, version 2
- http://hal.inria.fr/inria-00116918
- oai:hal.inria.fr:inria-00116918
- Contributeur :
- Soumis le : Jeudi 30 Novembre 2006, 10:42:38
- Dernière modification le : Vendredi 19 Janvier 2007, 14:11:19
Documents associés
Exporter