The pi-calculus with polyadic synchronization - REVISED
Author
Martinho, Joana
Term
10. Term
Education
Publication year
2004
Abstract
I denne afhandling undersøger vi pi-calculus med polyadisk synkronisering, et formelt sprog til at beskrive kommunikerende, samtidige systemer, hvor kanaler kan være sekvenser af navne. Vi udvider denne ramme med kryptografiske primitiver—grundlæggende operationer til at modellere sikker kommunikation—og viser derefter, at enhver anvendelse af disse kan indkodes systematisk tilbage i den oprindelige pi-calculus med polyadisk synkronisering uden at ændre den observerbare adfærd. Vi beviser, at indkodningen er lyd og fuldstændig med hensyn til barbed congruence, en standard adfærdslig ækvivalens baseret på observerbare interaktioner, og vi viser, at barbed congruence i denne sammenhæng falder sammen med early congruence.
In this thesis, we study the pi-calculus with polyadic synchronization, a formal language for describing communicating, concurrent systems where channels can be sequences of names. We extend this framework with cryptographic primitives—basic operations used to model secure communication—and then show that every use of these features can be systematically encoded back into the original pi-calculus with polyadic synchronization without changing observable behavior. We prove that the encoding is sound and complete with respect to barbed congruence, a standard behavioral equivalence based on observable interactions, and we show that in this setting barbed congruence coincides with early congruence.
[This abstract was generated with the help of AI]
Documents