@inproceedings{b24bf16833984387b8dde03fec9117af,
title = "Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus",
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.",
keywords = "Applied pi-calculus, Asynchronous transition systems, Processes, Security, Structural operational semantics",
author = "Cl{\'e}ment Aubert and Ross Horne and Christian Johansen",
note = "Publisher Copyright: {\textcopyright} Cl{\'e}ment Aubert, Ross Horne, and Christian Johansen; licensed under Creative Commons License CC-BY 4.0.; 33rd International Conference on Concurrency Theory, CONCUR 2022 ; Conference date: 12-09-2022 Through 16-09-2022",
year = "2022",
month = sep,
day = "1",
doi = "10.4230/LIPIcs.CONCUR.2022.30",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Bartek Klin and Slawomir Lasota and Anca Muscholl",
booktitle = "33rd International Conference on Concurrency Theory, CONCUR 2022",
address = "Germany",
}