Compositional Analysis of Protocol Equivalence in the Applied pi-Calculus Using Quasi-open Bisimilarity

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 is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach 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.