Diamonds for security: a non-interleaving operational semantics for the applied pi-calculus

Clément Aubert, Ross Horne, Christian Johansen

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

3 Citations (Scopus)
7 Downloads (Pure)

Abstract

We introduce a non-interleaving structural operational semantics for the applied π-calculus and prove that it satisfies the properties expected of a labelled asynchronous transition system (LATS). LATS have well-studied relations with other standard non-interleaving models, such as Mazurkiewicz traces or event structures, and are a natural extension of labelled transition systems where the independence of transitions is made explicit. We build on a considerable body of literature on located semantics for process algebras and adopt a static view on locations to identify the parallel processes that perform a transition. By lifting, in this way, work on CCS and π-calculus to the applied π-calculus, we lay down a principled foundation for reusing verification techniques such as partial-order reduction and non-interleaving equivalences in the field of security. The key technical device we develop is the notion of located aliases to refer unambiguously to a specific output originating from a specific process. This light mechanism ensures stability, avoiding disjunctive causality problems that parallel extrusion incurs in similar non-interleaving semantics for the π-calculus.
Original languageEnglish
Title of host publication33rd International Conference on Concurrency Theory
EditorsBartek Klin, Sławomir Lasota, Anca Muscholl
Place of PublicationWadern, Germany
Pages30:1-30:26
Number of pages26
ISBN (Electronic)9783959772464
DOIs
Publication statusPublished - 6 Sept 2022
Event33rd International Conference on Concurrency Theory - Warsaw, Poland
Duration: 12 Sept 202216 Sept 2022

Conference

Conference33rd International Conference on Concurrency Theory
Abbreviated titleCONCUR 2022
Country/TerritoryPoland
CityWarsaw
Period12/09/2216/09/22

Keywords

  • security
  • processes
  • structural operational semantics
  • asynchronous transition systems
  • applied pi-calculus

Fingerprint

Dive into the research topics of 'Diamonds for security: a non-interleaving operational semantics for the applied pi-calculus'. Together they form a unique fingerprint.

Cite this