Validating Integrity for the Ephemerizer's Protocol with CL-Atse

Charu Arora 1 Mathieu Turuani 2
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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : It is usually very difficult in Computer Science to make an information "disappear" after a certain time, once it has been published or mirrored by servers world wide. This, however, is the goal of the IBM ephemerizer's protocol by Radia Perlman. We present in this paper the general structure of the CL-Atse protocol analysis tool from the AVISPA's tool-suite, and symbolic analysis of the ephemerizer's protocol and its extensions using CL-Atse. This protocol allows transmitting a data which retrieval is guarantied to be impossible after a certain time. We show that this protocol is secure for this property plus the secrecy of the data, but is trivially non secure for its integrity. We model a standard integrity check as a first extension to this protocol, which is natural and close to common usage, and we present a second extension for integrity that is much less obvious and deeply integrated in the structure of the ephemerizer's protocol. Then, we show that while the first extension guaranty the basic integrity property under certain conditions, the second one is much stronger and allows faster computations.
Type de document :
Chapitre d'ouvrage
Véronique Cortier and Claude Kirchner and Mitsuhiro Okada and Hideki Sakurada. Formal to Practical Security : Papers Issued from the 2005-2008 French-Japanese Collaboration, 5458, Springer Berlin Heidelberg, pp.21-32, 2009, Lecture Notes in Computer Science, 978-3-642-02002-5. 〈10.1007/978-3-642-02002-5_2〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00758659
Contributeur : Mathieu Turuani <>
Soumis le : jeudi 29 novembre 2012 - 10:11:21
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

Citation

Charu Arora, Mathieu Turuani. Validating Integrity for the Ephemerizer's Protocol with CL-Atse. Véronique Cortier and Claude Kirchner and Mitsuhiro Okada and Hideki Sakurada. Formal to Practical Security : Papers Issued from the 2005-2008 French-Japanese Collaboration, 5458, Springer Berlin Heidelberg, pp.21-32, 2009, Lecture Notes in Computer Science, 978-3-642-02002-5. 〈10.1007/978-3-642-02002-5_2〉. 〈hal-00758659〉

Partager

Métriques

Consultations de la notice

295