Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Two styles of definitions are usually considered to
express that a security protocol preserves the confidentiality of a
data { t s}. Reach-ability-based secrecy means that { t s} should
never be disclosed while equi-valence-based secrecy states that two
executions of a protocol with distinct instances for { t s} should
be indistinguishable to an attacker. Although the second formulation
ensures a higher level of security and is closer to cryptographic
notions of secrecy, decidability results and automatic tools have
mainly focused on the first definition so far.
This paper initiates a systematic investigation of situations where
syntactic secrecy entails strong secrecy.
We show that in the passive case, reachability-based secrecy
actually implies equivalence-based secrecy for signatures, symmetric
and asymmetric encryption provided that the primitives are
probabilistic. For active adversaries in the case of symmetric
encryption, we provide sufficient (and rather tight) conditions on
the protocol for this implication to hold.
@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
author = {Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
title = {{Relating two standard notions of secrecy}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--29},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-02-6},
ISSN = {2190-6807},
year = {2006},
volume = {3},
editor = {Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.691},
URN = {urn:nbn:de:0030-drops-6911},
doi = {10.4230/OASIcs.TrustworthySW.2006.691},
annote = {Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}