2005 | OriginalPaper | Buchkapitel
A Fully Abstract Encoding of the π-Calculus with Data Terms
(Extended Abstract)
verfasst von : Michael Baldamus, Joachim Parrow, Björn Victor
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The
π
-calculus with data terms (
π
T) extends the pure
π
-calculus by data constructors and destructors and allows data to be transmitted between agents. It has long been known how to encode such data types in
π
, but until now it has been open how to make the encoding
fully abstract
, meaning that two encodings (in
π
) are semantically equivalent precisely when the original
π
T agents are semantically equivalent. We present a new type of encoding and prove it to be fully abstract with respect to may-testing equivalence. To our knowledge this is the first result of its kind, for any calculus enriched with data terms. It has particular importance when representing security properties since attackers can be regarded as may-test observers. Full abstraction proves that it does not matter whether such observers are formulated in
π
or
π
T, both are equally expressive in this respect. The technical new idea consists of achieving full abstraction by encoding data as table entries rather than active processes, and using a firewalled central integrity manager to ensure data security.