Document Open Access Logo

Open Bisimilarity for the π-Calculus with Mismatch

Authors Tiange Liu , Alwen Tiu , Ross Horne

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.30.pdf
  • Filesize: 0.78 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • mismatch
  • open bisimilarity
  • pi calculus

Metrics

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

Abstract

Open bisimilarity is an equivalence relation for the π-calculus that is also congruence, making it suitable to use in compositional reasoning for mobile processes and communication protocols. The original definition of open bisimilarity, due to Sangiorgi, does not account for the mismatch operator, that is crucial in modelling real-world protocols. When mismatch is present, the congruence property no longer holds for open bisimilarity. In a LICS 2018 paper, Horne et al. proposed an extension of open bisimilarity, using a history-indexed class of relations, to address this problem. That definition, however, turns out to be non-compositional as we shall demonstrate in this paper. This paper presents a new definition of open bisimilarity in the π-calculus that incorporates mismatch. This is achieved by augmenting the transition semantics of the π-calculus with an explicit assumption about name distinctions, and by requiring that open bisimulation to be closed under an arbitary extension of the name distinctions assumption. We then prove that the resulting open bisimilarity is both an equivalence relation and a congruence.

Cite As Get BibTex

Tiange Liu, Alwen Tiu, and Ross Horne. Open Bisimilarity for the π-Calculus with Mismatch. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.30

Author Details

Tiange Liu
  • School of Computing, The Australian National University, Canberra, Australia
Alwen Tiu
  • School of Computing, The Australian National University, Canberra, Australia
Ross Horne
  • University of Strathclyde, Glasgow, UK

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 Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Richard Graveman, Philippe A. Janson, Clifford Neuman, and Li Gong, editors, CCS '97, Proceedings of the 4th ACM Conference on Computer and Communications Security, Zurich, Switzerland, April 1-4, 1997, pages 36-47. ACM, 1997. URL: https://doi.org/10.1145/266420.266432.
  3. Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimilarity using an intuitionistic modal logic. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.7.
  4. Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 107-121. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CSF.2010.15.
  5. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The bedwyr system for model checking over syntactic expressions. In Frank Pfenning, editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 391-397. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73595-3_28.
  6. Jesper Bengtson. The pi-calculus in nominal logic. Arch. Formal Proofs, 2012, 2012. URL: https://www.isa-afp.org/entries/Pi_Calculus.shtml.
  7. Michele Boreale and Rocco De Nicola. A symbolic semantics for the pi-calculus. Inf. Comput., 126(1):34-52, 1996. URL: https://doi.org/10.1006/INCO.1996.0032.
  8. Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, and Björn Victor. The psi-calculi workbench: A generic tool for applied process calculi. ACM Trans. Embed. Comput. Syst., 14(1):9:1-9:25, 2015. URL: https://doi.org/10.1145/2682570.
  9. Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Trace equivalence decision: negative tests and non-determinism. In Yan Chen, George Danezis, and Vitaly Shmatikov, editors, Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 321-330. ACM, 2011. URL: https://doi.org/10.1145/2046707.2046744.
  10. Stéphanie Delaune, Steve Kremer, and Mark Ryan. Symbolic bisimulation for the applied pi calculus. In Vikraman Arvind and Sanjiva Prasad, editors, FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings, volume 4855 of Lecture Notes in Computer Science, pages 133-145. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-77050-3_11.
  11. Yuxi Fu and Zhenrong Yang. Tau laws for pi calculus. Theoretical Computer Science, 308(1-3):55-130, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00202-0.
  12. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theor. Comput. Sci., 138(2):353-389, 1995. URL: https://doi.org/10.1016/0304-3975(94)00172-F.
  13. Ross Horne, Ki Yung Ahn, Shang-Wei Lin, and Alwen Tiu. Quasi-open bisimilarity with mismatch is intuitionistic. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 26-35. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209125.
  14. Ross Horne and Sjouke Mauw. Discovering epassport vulnerabilities using bisimilarity. Log. Methods Comput. Sci., 17(2):24, 2021. URL: https://doi.org/10.23638/LMCS-17(2:24)2021.
  15. Ross Horne, Sjouke Mauw, and Semen Yurkov. When privacy fails, a formula describes an attack: A complete and compositional verification method for the applied π-calculus. Theor. Comput. Sci., 959:113842, 2023. URL: https://doi.org/10.1016/J.TCS.2023.113842.
  16. Jia Liu and Huimin Lin. A complete symbolic bisimulation for full applied pi calculus. Theor. Comput. Sci., 458:76-112, 2012. URL: https://doi.org/10.1016/J.TCS.2012.07.034.
  17. Tiange Liu, Alwen Tiu, and Jim de Groot. Modal logics for mobile processes revisited. In 34th International Conference on Concurrency Theory (CONCUR 2023). Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2023. Google Scholar
  18. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i. Information and computation, 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  19. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Information & Computation, 100:41-77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5.
  20. Joachim Parrow and Davide Sangiorgi. Algebraic theories for name-passing calculi. Information and Computation, 120(2):174-197, 1995. URL: https://doi.org/10.1006/INCO.1995.1108.
  21. Joachim Parrow and Björn Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 98CB36226), pages 176-185. IEEE, 1998. URL: https://doi.org/10.1109/LICS.1998.705654.
  22. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 127-142. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_10.
  23. Davide Sangiorgi and David Walker. On barbed equivalences in pi-calculus. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 292-304. Springer, 2001. URL: https://doi.org/10.1007/3-540-44685-0_20.
  24. Davide Sangiorgi and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. Google Scholar
  25. Alwen Tiu. A trace based bisimulation for the spi calculus: An extended abstract. In Zhong Shao, editor, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, volume 4807 of Lecture Notes in Computer Science, pages 367-382. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_25.
  26. Alwen Tiu and Jeremy E. Dawson. Automating open bisimulation checking for the spi calculus. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 307-321. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CSF.2010.28.
  27. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log., 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
  28. Christian Urban. Nominal techniques in isabelle/hol. J. Autom. Reason., 40(4):327-356, 2008. URL: https://doi.org/10.1007/S10817-008-9097-2.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact