The Applied pi-calculus: Type Systems and Expresiveness
Authors
Bloch, Anders ; Frederiksen, Morten V. ; Haagensen, Bjørn
Term
4. term
Education
Publication year
2004
Abstract
Dette speciale undersøger formelle modeller for kommunikerende systemer. Vi giver en kodning af Applied pi-calculus (AppPi) i pi-kalkylen og viser, hvordan AppPi kan instansieres, så man får spi-kalkylen. Vi definerer to typesystemer for AppPi: et basalt system, der fanger typiske fejl som aritetsfejl (forkert antal argumenter) og forkert brug af navne (såsom kanaler), og et sikkerhedsorienteret system, der er ækvivalent med Abadis typesystem for spi-kalkylen til at kontrollere sikkerhedsegenskaber. Vores repræsentation af spi-kalkylen bevarer typer i forhold til dette system. Vi viser, at kodningen af spi-kalkylen i den nævnte instans af AppPi er lydig og fuldstændig med hensyn til operationel korrespondance, dvs. at adfærd i kilde og mål stemmer nøje overens. For at understøtte beviserne giver vi spi-kalkylen en semantik i samme stil som for AppPi, nemlig en tidlig mærket transitionsrelation, og vi viser, at denne semantik er stærkt ækvivalent med den oprindelige semantik af Abadi og Gordon, som bygger på abstraktioner og koncretioner. Vi koder ikke AppPi's ækvationsteori direkte, men bygger på velkendte resultater, der omskriver sådanne teorier til konfluente og terminerende omskrivningssystemer, som vi så koder på. Denne kodning er lydig med hensyn til operationel korrespondance. I lyset af den sparsomme mængde arbejde, der fulgte den oprindelige AppPi-publication, er en vigtig fordel ved vores tilgang, at den gør de mange teoretiske og praktiske værktøjer fra pi-kalkylen tilgængelige for ræsonnering i AppPi.
This thesis studies formal models for communicating systems. We give an encoding of the Applied pi-calculus (AppPi) into the pi-calculus and show how AppPi can be instantiated to obtain the spi-calculus. We define two type systems for AppPi: a basic system that catches common mistakes such as arity mismatches (wrong number of arguments) and incorrect use of names (such as channels), and a security-oriented system equivalent to Abadi's type system for the spi-calculus for checking security properties. Our representation of the spi-calculus preserves types with respect to this system. We prove that the encoding of the spi-calculus within the AppPi instance is sound and complete with respect to operational correspondence, meaning that behaviors in the source and target match closely. To support these proofs, we give the spi-calculus a semantics in the same style as AppPi, namely an early labelled transition relation, and we show that this semantics is strongly equivalent to the original one by Abadi and Gordon, which uses abstractions and concretions. We do not encode AppPi's equational theory directly. Instead, we rely on established results that transform such a theory into a confluent and terminating rewrite system, on which our encoding is carried out. This encoding is sound with respect to operational correspondence. Given the limited follow-up work on AppPi, a key benefit of our approach is that it makes the extensive theoretical and practical tools developed for the pi-calculus available for reasoning in AppPi.
[This abstract was generated with the help of AI]
Documents