Selected publications at LSV: 2009

Mathieu Baudet, Véronique Cortier and Steve KremerComputationally Sound Implementations of Equational Theories against Passive AdversariesInformation and Computation 207(4), pages 496-520, 2009. ( PDF )
doi: 10.1016/j.ic.2008.12.005
In this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In contrast to other works, we do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization with respect to 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, to illustrate our framework, we establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.

   author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer, Steve},
   DOI = {10.1016/j.ic.2008.12.005},
   journal = {Information and Computation},
   month = apr,
   number = {4},
   pages = {496-520},
   publisher = {Elsevier Science Publishers},
   title = {Computationally Sound Implementations of Equational Theories against Passive Adversaries},
   url = {},
   volume = {207},
   year = {2009},

About LSV