Document Open Access Logo

Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus

Authors Clément Aubert , Ross Horne , Christian Johansen

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.30.pdf
  • Filesize: 1.6 MB
  • 26 pages

Document Identifiers

Author Details

Clément Aubert
  • Augusta University, Augusta, GA, USA
Ross Horne
  • University of Luxembourg, Luxembourg
Christian Johansen
  • NTNU - Norwegian University of Science and Technology, Gjøvik, Norway

Acknowledgements

The authors wish to express their gratitude to the reviewers for their recommendations, that helped us improve our presentation.

Cite AsGet BibTex

Clément Aubert, Ross Horne, and Christian Johansen. Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.30

Abstract

We introduce a non-interleaving structural operational semantics for the applied π-calculus and prove that it satisfies the properties expected of a labelled asynchronous transition system (LATS). LATS have well-studied relations with other standard non-interleaving models, such as Mazurkiewicz traces or event structures, and are a natural extension of labelled transition systems where the independence of transitions is made explicit. We build on a considerable body of literature on located semantics for process algebras and adopt a static view on locations to identify the parallel processes that perform a transition. By lifting, in this way, work on CCS and π-calculus to the applied π-calculus, we lay down a principled foundation for reusing verification techniques such as partial-order reduction and non-interleaving equivalences in the field of security. The key technical device we develop is the notion of located aliases to refer unambiguously to a specific output originating from a specific process. This light mechanism ensures stability, avoiding disjunctive causality problems that parallel extrusion incurs in similar non-interleaving semantics for the π-calculus.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Theory of computation → Concurrency
  • Theory of computation → Process calculi
Keywords
  • Security
  • Processes
  • Structural operational semantics
  • Asynchronous transition systems
  • Applied pi-calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: Mobile values, new names, and secure communication. J. ACM, 65(1):1:1-1:41, 2018. URL: https://doi.org/10.1145/3127586.
  2. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pages 104-115, 2001. URL: https://doi.org/10.1145/360204.360213.
  3. Reynald Affeldt and Naoki Kobayashi. Partial order reduction for verification of spatial properties of pi-calculus processes. Electron. Notes Theor. Comput. Sci., 128(2):151-168, 2004. Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004). URL: https://doi.org/10.1016/j.entcs.2004.11.034.
  4. Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 107-121, 2010. URL: https://doi.org/10.1109/CSF.2010.15.
  5. David Baelde. Contributions à la Vérification des Protocoles Cryptographiques. Habilitation à diriger des recherches, Université Paris-Saclay, February 2021. URL: http://www.lsv.fr/~baelde/hdr/habilitation_baelde.pdf.
  6. David Baelde, Stéphanie Delaune, and Lucca Hirschi. POR for security protocol equivalences - beyond action-determinism. In Javier López, Jianying Zhou, and Miguel Soriano, editors, Computer Security - 23rd European Symposium on Research in Computer Security, ESORICS 2018, Barcelona, Spain, September 3-7, 2018, Proceedings, Part I, volume 11098 of LNCS, pages 385-405. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99073-6_19.
  7. David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial order reduction for security protocols. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 497-510. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.497.
  8. David Baelde, Stéphanie Delaune, and Lucca Hirschi. A reduced semantics for deciding trace equivalence. Log. Meth. Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:8)2017.
  9. Marek A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, Brighton, UK, 1988. Google Scholar
  10. Bruno Blanchet. Modeling and verifying security protocols with the applied pi calculus and proverif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, 2016. URL: https://doi.org/10.1561/3300000004.
  11. Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Inform., 35(5):353-400, 1998. Google Scholar
  12. Gérard Boudol and Ilaria Castellani. A non-interleaving semantics for CCS based on proved transitions. Fund. Inform., 11:433-452, 1988. Google Scholar
  13. Gérard Boudol, Ilaria Castellani, Matthew Hennessy, and Astrid Kiehn. Observing localities. Theor. Comput. Sci., 114(1):31-61, 1993. URL: https://doi.org/10.1016/0304-3975(93)90152-J.
  14. Sergiu Bursuc, Christian Johansen, and Shiwei Xu. Automated verification of dynamic root of trust protocols. In Matteo Maffei and Mark Ryan, editors, International Conference on Principles of Security and Trust, volume 10204 of LNCS, pages 95-116. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54455-6_5.
  15. Georgia Carabetta, Pierpaolo Degano, and Fabio Gadducci. CCS semantics via proved transition systems and rewriting logic. In Claude Kirchner and Hélène Kirchner, editors, 1998 International Workshop on Rewriting Logic and its Applications, WRLA 1998, Abbaye des Prémontrés at Pont-à-Mousson, France, September 1998, volume 15 of Electron. Notes Theor. Comput. Sci., pages 369-387. Elsevier, 1998. URL: https://doi.org/10.1016/S1571-0661(05)80023-4.
  16. Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log., 17(4):23:1-23:32, September 2016. URL: https://doi.org/10.1145/2926715.
  17. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Exploiting symmetries when proving equivalence properties for security protocols. In Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan Katz, editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 905-922. ACM, 2019. URL: https://doi.org/10.1145/3319535.3354260.
  18. Edmund M. Clarke, Somesh Jha, and Wilfredo R. Marrero. Efficient verification of security protocols using partial-order reductions. Int. J. Softw. Tools Technol. Transf., 4(2):173-188, 2003. URL: https://doi.org/10.1007/s10009-002-0103-4.
  19. Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. SAT-Equiv: An efficient tool for equivalence properties. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pages 481-494, August 2017. URL: https://doi.org/10.1109/CSF.2017.15.
  20. Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Event structure semantics of parallel extrusion in the pi-calculus. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of LNCS, pages 225-239. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_15.
  21. Cas J. F. Cremers and Sjouke Mauw. Checking secrecy by means of partial order reduction. In Daniel Amyot and Alan W. Williams, editors, System Analysis and Modeling, 4th International SDL and MSC Workshop, SAM 2004, Ottawa, Canada, June 1-4, 2004, Revised Selected Papers, volume 3319 of LNCS, pages 171-188. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-31810-1_12.
  22. Ioana Cristescu, Jean Krivine, and Daniele Varacca. Rigid families for CCS and the π-calculus. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, volume 9399 of LNCS, pages 223-240. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_14.
  23. Pierpaolo Degano, Fabio Gadducci, and Corrado Priami. Causality and replication in concurrent processes. In Manfred Broy and Alexandre V. Zamulin, editors, Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003, Revised Papers, volume 2890 of LNCS, pages 307-318. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39866-0_30.
  24. Pierpaolo Degano and Corrado Priami. Proved trees. In Werner Kuich, editor, Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings, volume 623 of LNCS, pages 629-640. Springer, 1992. URL: https://doi.org/10.1007/3-540-55719-9_110.
  25. Pierpaolo Degano and Corrado Priami. Non-interleaving semantics for mobile processes. Theor. Comput. Sci., 216(1-2):237-270, 1999. URL: https://doi.org/10.1016/S0304-3975(99)80003-6.
  26. Pierpaolo Degano and Corrado Priami. Enhanced operational semantics. ACM Comput. Surv., 33(2):135-176, 2001. URL: https://doi.org/10.1145/384192.384194.
  27. Wan Fokkink, Mohammad Torabi Dashti, and Anton Wijs. Partial order reduction for branching security protocols. In 2010 10th International Conference on Application of Concurrency to System Design, pages 191-200. IEEE, 2010. URL: https://doi.org/10.1109/ACSD.2010.19.
  28. Éric Goubault. Labelled cubical sets and asynchronous transition systems: an adjunction. In Preliminary Proceedings CMCIM'02, 2002. URL: http://www.lix.polytechnique.fr/~goubault/papers/cmcim02.ps.gz.
  29. Thomas Troels Hildebrandt. Categorical Models for Concurrency: Independence, Fairness and Dataflow. PhD thesis, BRICS, University of Aarhus, February 2000. URL: http://www.brics.dk/DS/00/1/.
  30. Thomas Troels Hildebrandt, Christian Johansen, and Håkon Normann. A stable non-interleaving early operational semantics for the pi-calculus. J. Log. Algebr. Methods Program., 104:227-253, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.02.006.
  31. Ross Horne and Sjouke Mauw. Discovering epassport vulnerabilities using bisimilarity. Log. Meth. Comput. Sci., 17(2):24, 2021. URL: https://doi.org/10.23638/LMCS-17(2:24)2021.
  32. Ross Horne, Sjouke Mauw, and Semen Yurkov. Compositional analysis of protocol equivalence in the applied π-calculus using quasi-open bisimilarity. In Antonio Cerone and Peter Csaba Ölveczky, editors, Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings, volume 12819 of LNCS, pages 235-255. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_14.
  33. Ross Horne, Sjouke Mauw, and Semen Yurkov. Unlinkability of an improved key agreement protocol for emv 2nd gen payments. In Stefano Calzavara, editor, IEEE Computer Security Foundations Symposium 2022 (CSF2022), August, 2022, Haifa, Israel, 2022. to appear. URL: https://satoss.uni.lu/members/ross/pdf/emv.pdf.
  34. Lalita Jategaonkar Jagadeesan and Radha Jagadeesan. Causality and true concurrency: A data-flow analysis of the pi-calculus. In International Conference on Algebraic Methodology and Software Technology, pages 277-291. Springer, 1995. Google Scholar
  35. Steve Kremer and Robert Künnemann. Automated analysis of security protocols with global state. JCS, 24(5):583-616, 2016. URL: https://doi.org/10.3233/JCS-160556.
  36. Steve Kremer and Mark Ryan. Analysis of an electronic voting protocol in the applied pi calculus. In Mooly Sagiv, editor, Programming Languages and Systems: 14th European Symposium on Programming (ESOP'05 at ETAPS'05), volume 3444 of LNCS, pages 186-200. Springer-Verlag, 2005. URL: https://doi.org/10.1007/978-3-540-31987-0_14.
  37. Ivan Lanese, Iain C. C. Phillips, and Irek Ulidowski. An axiomatic approach to reversible computation. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of LNCS, pages 442-461. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_23.
  38. Sebastian Mödersheim, Luca Viganò, and David Basin. Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. J. Comput. Secur., 18(4):575-618, 2010. URL: https://doi.org/10.3233/JCS-2009-0351.
  39. Madhavan Mukund and Mogens Nielsen. CCS, Location and Asynchronous Transition Systems. In R. K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18-20, 1992, Proceedings, volume 652 of LNCS, pages 328-341. Springer, 1992. URL: https://doi.org/10.1007/3-540-56287-7_116.
  40. Kirstin Peters, Jens-Wolfhard Schicke-Uffmann, Ursula Goltz, and Uwe Nestmann. Synchrony versus causality in distributed systems. Math. Struct. Comput. Sci., 26(8):1459-1498, 2016. URL: https://doi.org/10.1017/S0960129514000644.
  41. Carl Adam Petri. Fundamentals of a theory of asynchronous information flow. In Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27 - September 1, 1962, pages 386-390. North-Holland, 1962. Google Scholar
  42. Iain Phillips and Irek Ulidowski. Reversibility and models for concurrency. Electron. Notes Theor. Comput. Sci., 192(1):93-108, 2007. URL: https://doi.org/10.1016/j.entcs.2007.08.018.
  43. Mark Dermot Ryan and Ben Smyth. Applied pi calculus. In Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 112-142. IOS Press, 2011. URL: https://doi.org/10.3233/978-1-60750-714-7-112.
  44. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. Acta Inform., 33(1):69-97, 1996. URL: https://doi.org/10.1007/s002360050036.
  45. Michael W. Shields. Concurrent machines. Comput. J., 28(5):449-465, 1985. URL: https://doi.org/10.1093/comjnl/28.5.449.
  46. Alwen Tiu, Nam Nguyen, and Ross Horne. Spec: An equivalence checker for security protocols. In Atsushi Igarashi, editor, 14th Asian Symposium on Programming Languages and Systems (APLAS'16), volume 10017 of LNCS, pages 87-95. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_5.
  47. Rob van Glabbeek. On the Expressiveness of Higher Dimensional Automata. Theor. Comput. Sci., 356(3):265-290, 2006. Google Scholar
  48. Rob van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Inform., 37(4/5):229-327, 2001. URL: https://doi.org/10.1007/s002360000041.
  49. Rob van Glabbeek and Gordon D. Plotkin. Configuration structures, event structures and petri nets. Theor. Comput. Sci., 410(41):4111-4159, 2009. URL: https://doi.org/10.1016/j.tcs.2009.06.014.
  50. Daniele Varacca and Nobuko Yoshida. Typed event structures and the linear pi-calculus. Theor. Comput. Sci., 411(19):1949-1973, 2010. URL: https://doi.org/10.1016/j.tcs.2010.01.024.
  51. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Samson Abramsky, Dov M. Gabbay, and Thomas Stephen Edward Maibaum, editors, Semantic Modelling, volume 4 of Handbook of Logic in Computer Science, pages 1-148. Oxford University Press, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact