Computationally Sound Implementations of Equational Theories Against Passive Adversaries

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 and a theory of ciphers and lists.

• Type: Conference
• Year: 2005
• Where: ICALP
• Authors: Mathieu Baudet, Véronique Cortier, Steve Kremer
• Keywords: Arbitrary Equational Theory, Cryptographic, Cryptographic Pi Calculi, ICALP 2005, Theoretical Computer Science