Stateful Applied Pi Calculus

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution

Colleges, School and Institutes


We extend the applied pi calculus with state cells, which are used to reason about protocols that store persistent information. Examples are protocols
involving databases or hardware modules with internal state. We distinguish between private state cells, which are not available to the attacker, and public state cells, which arise when a private state cell is compromised by the attacker. For processes involving only private state cells we define observational equivalence and labelled bisimilarity in the same way as in the original applied pi calculus, and show that they coincide. Our result implies Abadi-Fournet’s theorem – the coincidence of observational equivalence and labelled bisimilarity – in a revised version of the applied pi calculus. For processes involving public state cells, we can essentially keep the definition of observational equivalence, but need to strengthen the definition of labelled bisimulation in order to show that observational equivalence and labelled bisimilarity coincide in this case as well.


Original languageEnglish
Title of host publicationPrinciples of Security and Trust
Subtitle of host publicationThird International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings
EditorsMartin Abadi, Steve Kremer
Publication statusPublished - 2014

Publication series

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