Computationally sound implementations of equational theories against passive adversaries |
| |
Authors: | Mathieu Baudet Véronique Cortier Steve Kremer |
| |
Affiliation: | 1. DCSSI, Paris, France;2. Loria/CNRS & INRIA Lorraine Projet Cassis, France;3. LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan, France |
| |
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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|