Relating two standard notions of secrecy

TL;DR

This paper explores the relationship between reachability-based and equivalence-based secrecy in security protocols, showing conditions under which one implies the other for various cryptographic primitives and adversary models.

Contribution

It systematically investigates when syntactic secrecy guarantees strong secrecy, establishing implications for passive and active adversaries across different cryptographic primitives.

Findings

Reachability-based secrecy implies equivalence-based secrecy for passive cases with probabilistic primitives.

Conditions are identified under which strong secrecy follows from syntactic secrecy in active adversary scenarios.

The results bridge the gap between different secrecy notions, aiding automated verification tools.

Abstract

Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for 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 the situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for digital signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.