International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Mathieu Baudet

Affiliation: ANSSI

Publications

Year
Venue
Title
2011
JOFC
2005
EPRINT
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, as well as a theory of ciphers and lists.