Excommunication: transforming pi-calculus specifications to remove internal communication

Geoff W. Hamilton, Benjamin Aziz

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

Abstract

In this paper, we present a new automatic transformation algorithm called excommunication that transforms pi-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 defined 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 languageEnglish
Title of host publicationProceedings of the 25th Brazilian Symposium on Formal Methods
PublisherSpringer
Publication statusAccepted for publication - 20 Sep 2022
Event25th Brazilian Symposium on Formal Methods - Online
Duration: 5 Dec 20229 Dec 2022
https://sites.google.com/dcomp.ufs.br/sbmf2022/home

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th Brazilian Symposium on Formal Methods
Abbreviated titleSBMF 2022
Period5/12/229/12/22
Internet address

Keywords

  • Formal Methods
  • Pi Calculus
  • Process Algebra
  • Program Transformation
  • Security

Fingerprint

Dive into the research topics of 'Excommunication: transforming pi-calculus specifications to remove internal communication'. Together they form a unique fingerprint.

Cite this