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

Ross Horne, Sjouke Mauw, Semen Yurkov

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)
7 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2021
EditorsAntonio Cerone, Peter Csaba Ölveczky
Place of PublicationCham
Pages235-255
Number of pages21
Volume12819
ISBN (Electronic)9783030853150
DOIs
Publication statusPublished - 20 Aug 2021
Event18th International Colloquium - Theoretical Aspects of Computing – ICTAC 2021 - Nur-Sultan, Kazakhstan
Duration: 8 Sept 202110 Sept 2021

Publication series

Name Lecture Notes in Computer Science - LNCS
PublisherSpringer
Volume12819
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Colloquium - Theoretical Aspects of Computing – ICTAC 2021
Abbreviated titleICTAC 2021
Country/TerritoryKazakhstan
CityNur-Sultan
Period8/09/2110/09/21

Keywords

  • compositional analysis
  • protocol equivalence
  • quasi-open bisimilarity
  • security and privacy problems
  • cryptographic calculi
  • bisimilarity
  • security
  • privacy
  • compositionality

Fingerprint

Dive into the research topics of 'Compositional analysis of protocol equivalence in the applied pi-calculus using quasi-open bisimilarity'. Together they form a unique fingerprint.

Cite this