Projects per year
Abstract
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 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.
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.
Original language  English 

Title of host publication  Principles of Security and Trust 
Subtitle of host publication  Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 513, 2014, Proceedings 
Editors  Martin Abadi, Steve Kremer 
Publisher  Springer 
Pages  2241 
Volume  8414 
ISBN (Electronic)  9783642547928 
ISBN (Print)  9783642547911 
DOIs  
Publication status  Published  2014 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  8414 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Fingerprint
Dive into the research topics of 'Stateful Applied Pi Calculus'. Together they form a unique fingerprint.Projects
 1 Finished

Leadership Fellowships 2009 : Analysing Security and Privacy Properties
ENGINEERING & PHYSICAL SCIENCE RESEARCH COUNCIL
1/04/10 → 30/09/15
Project: Research Councils