Paper 2005/074 Original: eprint.iacr.org/2005/074 ↗
Computationally sound implementations of equational theories against passive adversaries
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 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.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2008-12-30: last updated
- 2005-03-08: published
- Short URL
- https://ia.cr/2005/074
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2005/074,
author = {Mathieu Baudet and Vëronique Cortier and Steve Kremer},
title = {Computationally sound implementations of equational theories against passive adversaries},
howpublished = {Cryptology {ePrint} Archive, Paper 2005/074},
year = {2005},
url = {https://eprint.iacr.org/2005/074}
}