Cryptology ePrint Archive: Report 2005/074

Computationally sound implementations of equational theories against passive adversaries

Mathieu Baudet and V{\'e}ronique Cortier and Steve Kremer

Abstract: In this paper we study the link between formal and cryptographic models for security protocols in the presence of a passive adversary. In contrast to other works, we do not consider a fixed set of primitives but aim at results for an arbitrary equational theory. We define a framework for comparing a cryptographic implementation and its idealization w.r.t. various security notions. In particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, we establish new soundness results for the Exclusive Or, as well as a theory of ciphers and lists.

Category / Keywords: foundations / cryptographic protocols, computational soundness of formal methods, static equivalence, equational theories

Publication Info: preprint submitted to Elsevier

Date: received 4 Mar 2005, last revised 30 Dec 2008

Contact author: baudet at lsv ens-cachan fr

Available formats: Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20081230:123149 (All versions of this report)

Discussion forum: Show discussion | Start new discussion