Verifying Privacy-Type Properties in a Modular Way

—Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlinkability) that play an important role in many modern applications are formalised using a notion of equivalence. In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches. As an e...

• Type: Journal
• Year: 2012
• Where: CSFW
• Authors: Myrto Arapinis, Vincent Cheval, Stéphanie Delaune
• Keywords: Composition Works, Cryptographic Primitives, CSFW 2012, Security Privacy, Trace Equivalence