Computationally Sound Implementations of Equational Theories against Passive Adversaries

Mathieu Baudet 1 Véronique Cortier 2 Steve Kremer 1
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 various security notions. In particular, we concentrate on the computationnal 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.
Complete list of metadatas

https://hal.inria.fr/inria-00000555
Contributor : Véronique Cortier <>
Submitted on : Wednesday, November 2, 2005 - 2:53:15 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

Citation

Mathieu Baudet, Véronique Cortier, Steve Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. 32nd International Colloquium on Automata, Languages and Programming - ICALP 2005, Jul 2005, Lisbonne/Portugal, pp.652-663, ⟨10.1007/11523468⟩. ⟨inria-00000555⟩

Share

Metrics

Record views

227