Excommunication: transforming π-calculus specifications to remove internal communication

Geoff W. Hamilton; Benjamin Aziz

doi:10.1007/978-3-031-22476-8_7

Excommunication: transforming π-calculus specifications to remove internal communication

Geoff W. Hamilton, Benjamin Aziz

Dublin City University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.

Original language	English
Title of host publication	Proceedings of the 25th Brazilian Symposium on Formal Methods
Publisher	Springer
Pages	109-123
Number of pages	15
ISBN (Electronic)	9783031224768
ISBN (Print)	9783031224751
DOIs	https://doi.org/10.1007/978-3-031-22476-8_7
Publication status	Published - 1 Dec 2022
Event	25th Brazilian Symposium on Formal Methods - Online Duration: 5 Dec 2022 → 9 Dec 2022 https://sites.google.com/dcomp.ufs.br/sbmf2022/home

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13768
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th Brazilian Symposium on Formal Methods
Abbreviated title	SBMF 2022
Period	5/12/22 → 9/12/22
Internet address	https://sites.google.com/dcomp.ufs.br/sbmf2022/home

Keywords

Formal Methods
Pi Calculus
Process Algebra
Program Transformation
Security

Access to Document

10.1007/978-3-031-22476-8_7

Embargoed Document

Excommunication
Accepted author manuscript (Post-print), 386 KB
Due to publisher’s copyright restrictions, this document is not freely available to download from this website until: 1/12/23

Cite this

@inproceedings{746f1ac709ee4c1fb40ad6b355bdc3a2,

title = "Excommunication: transforming π-calculus specifications to remove internal communication",

abstract = "In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.",

keywords = "Formal Methods, Pi Calculus, Process Algebra, Program Transformation, Security",

author = "Hamilton, {Geoff W.} and Benjamin Aziz",

note = "12 month embargo - Springer; 25th Brazilian Symposium on Formal Methods, SBMF 2022 ; Conference date: 05-12-2022 Through 09-12-2022",

year = "2022",

month = dec,

day = "1",

doi = "10.1007/978-3-031-22476-8_7",

language = "English",

isbn = "9783031224751",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "109--123",

booktitle = "Proceedings of the 25th Brazilian Symposium on Formal Methods",

url = "https://sites.google.com/dcomp.ufs.br/sbmf2022/home",

}

TY - GEN

T1 - Excommunication: transforming π-calculus specifications to remove internal communication

AU - Hamilton, Geoff W.

AU - Aziz, Benjamin

N1 - 12 month embargo - Springer

PY - 2022/12/1

Y1 - 2022/12/1

N2 - In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.

AB - In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.

KW - Formal Methods

KW - Pi Calculus

KW - Process Algebra

KW - Program Transformation

KW - Security

UR - https://sites.google.com/dcomp.ufs.br/sbmf2022

U2 - 10.1007/978-3-031-22476-8_7

DO - 10.1007/978-3-031-22476-8_7

M3 - Conference contribution

SN - 9783031224751

T3 - Lecture Notes in Computer Science

SP - 109

EP - 123

BT - Proceedings of the 25th Brazilian Symposium on Formal Methods

PB - Springer

T2 - 25th Brazilian Symposium on Formal Methods

Y2 - 5 December 2022 through 9 December 2022

ER -

Excommunication: transforming π-calculus specifications to remove internal communication

Abstract

Publication series

Conference

Keywords

Access to Document

Embargoed Document

Fingerprint

Cite this