Tags:bisimilarity, compositionality, cryptographic calculi, privacy and security
Abstract:
This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity it a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approch to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so.
Compositional Analysis of Protocol Equivalence in the Applied Pi-Calculus Using Quasi-Open Bisimilarity