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

Charu Arora (1) , Mathieu Turuani (2)

1 IIT Delhi - Indian Institute of Technology Delhi
2 CASSIS - Combination of approaches to the security of infinite states systems

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.

Domaines: Automatique

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⟩