Projects per year
Abstract
We extend AbadiFournet’s 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 AbadiFournet’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.
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 language  English 

Pages (fromto)  95149 
Number of pages  88 
Journal  Journal of Logical and Algebraic Methods in Programming 
Volume  89 
Early online date  18 Mar 2017 
DOIs  
Publication status  Published  1 Jun 2017 
Fingerprint
Dive into the research topics of 'Stateful Applied Pi Calculus: Observational Equivalence and Labelled Bisimilarity'. Together they form a unique fingerprint.Projects
 1 Finished

Verifying Interoperability requirements in Pervasive Systems
Engineering & Physical Science Research Council
8/10/08 → 7/03/13
Project: Research Councils