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.
Complete list of metadatas

https://hal.inria.fr/inria-00116918
Contributor : Rapport de Recherche Inria <>
Submitted on : Thursday, November 30, 2006 - 10:42:38 AM
Last modification on : Friday, November 16, 2018 - 1:24:06 AM
Long-term archiving on : Monday, September 20, 2010 - 4:31:24 PM

Files

RR-6039.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

539

Files downloads

114