Relating two standard notions of secrecy

Eugen Zalinescu, VéRonique Cortier & MichaëL Rusinowitch
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...