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 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.
Chapter PDF
Similar content being viewed by others
References
LinkedIn investigates hacking claims, http://www.guardian.co.uk/technology/2012/jun/06/linkedin-hacking
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2–32 (2006)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM Press (2001)
Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427–476 (2004)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: 4th ACM Conference on Computer and Communications Security, pp. 36–47. ACM Press (1997)
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of IEEE 23rd Computer Security Foundations Symposium, CSF 2010, pp. 107–121 (2010)
Arapinis, M., Ritter, E., Ryan, M.D.: Statverif: Verification of stateful processes. In: Proceedings of IEEE 24th Computer Security Foundations Symposium, CSF 2011, pp. 33–47 (2011), http://markryan.eu/research/statverif/
Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: IEEE Symposium on Security and Privacy, pp. 202–215 (2008)
Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic 14 (2013)
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science 7(1) (2011)
Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, CCS 2008, pp. 459–468. ACM (2008)
Blanchet, B.: Automatic Proof of Strong Secrecy for Security Protocols. In: IEEE Symposium on Security and Privacy, pp. 86–100 (2004)
Blanchet, B.: Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security 17(4), 363–434 (2009)
Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012)
Cheval, V., Comon-Lundh, H., Delaune, S.: Automating security analysis: Symbolic equivalence of constraint systems. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 412–426. Springer, Heidelberg (2010)
Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011), pp. 321–330 (2011)
Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoretical Computer Science 492, 1–39 (2013)
Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF 2009, pp. 266–276. IEEE Computer Society Press (July 2009)
Cortier, V., Rusinowitch, M., Zalinescu, E.: Relating two standard notions of secrecy. Logical Methods in Computer Science 3, 1–29 (2007)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security (2009)
Delaune, S., Kremer, S., Ryan, M.D.: Symbolic bisimulation for the applied pi calculus. Journal of Computer Security 18(2), 317–377 (2010)
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proc. of the 24th IEEE Computer Security Foundations Symposium (CSF 2011). IEEE Computer Society Press (2011)
Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A relational modal logic for higher-order stateful ADTs. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 185–198 (2010)
Garcia, F.D., van Rossum, P.: Modeling privacy for off-line RFID systems. In: Gollmann, D., Lanet, J.-L., Iguchi-Cartigny, J. (eds.) CARDIS 2010. LNCS, vol. 6035, pp. 194–208. Springer, Heidelberg (2010)
Guttman, J.D.: Fair exchange in strand spaces. Journal of Automated Reasoning (2012)
Koutarou, M.O., Suzuki, K., Kinoshita, S.: Cryptographic approach to “privacy-friendly” tags. RFID Privacy Workshop (2003)
Künnemann, R., Steel, G.: YubiSecure? formal security analysis results for the Yubikey and YubiHSM. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 257–272. Springer, Heidelberg (2013)
Liu, J.: A proof of coincidence of labeled bisimilarity and observational equivalence in applied pi calculus. Technical Report, ISCAS-SKLCS-11-05 (2011), http://mail.ios.ac.cn/~jliu/papers/Proof.pdf
Liu, J., Lin, H.: A complete symbolic bisimulation for full applied pi calculus. Theoretical Computer Science 458, 76–112 (2012)
Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proc. 17th ACM Conference on Computer and Communications Security (CCS 2010), pp. 351–360. ACM (2010)
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols. Pearson Education (2001)
Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of diffie-hellman protocols and advanced security properties. In: 25th Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)
Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP 2013, pp. 377–390 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arapinis, M., Liu, J., Ritter, E., Ryan, M. (2014). Stateful Applied Pi Calculus. In: Abadi, M., Kremer, S. (eds) Principles of Security and Trust. POST 2014. Lecture Notes in Computer Science, vol 8414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54792-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-54792-8_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54791-1
Online ISBN: 978-3-642-54792-8
eBook Packages: Computer ScienceComputer Science (R0)