Selected publications at LSV: 2009

BCK09: Mathieu Baudet, Véronique Cortier and Steve Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. Information and Computation 207(4), pages 496-520, 2009. ( PDF )
doi: 10.1016/j.ic.2008.12.005

Abstract:: 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.

`@article{BCK-IC09,`
	`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 =`	`{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf},`
	`volume =`	`{207},`
	`year =`	`{2009},`
`}`

About LSV