Compositional analysis of protocol equivalence in the applied pi-calculus using quasi-open bisimilarity

Horne, Ross and Mauw, Sjouke and Yurkov, Semen; Cerone, Antonio and Ölveczky, Peter Csaba, eds. (2021) Compositional analysis of protocol equivalence in the applied pi-calculus using quasi-open bisimilarity. In: Theoretical Aspects of Computing – ICTAC 2021. Lecture Notes in Computer Science - LNCS, 12819 . Springer: Lecture Notes in Computer Science, KAZ, pp. 235-255. ISBN 9783030853150 (https://doi.org/10.1007/978-3-030-85315-0_14)

[thumbnail of Horne-etal-ICTAC2021-Compositional-analysis-protocol-equivalence-applied-pi-calculus-using-quasi-open-bisimilarity]
Preview
Text. Filename: Horne-etal-ICTAC2021-Compositional-analysis-protocol-equivalence-applied-pi-calculus-using-quasi-open-bisimilarity.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo

Download (869kB)| Preview

Abstract

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied -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.