Cited By
View all- Horne RMauw SYurkov S(2023)When privacy fails, a formula describes an attackTheoretical Computer Science10.1016/j.tcs.2023.113842959:COnline publication date: 30-May-2023
Compositional Analysis of Protocol Equivalence in the Applied -Calculus Using Quasi-open Bisimilarity
Pages 235 - 255
Abstract
This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied -calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so.
References
[1]
Abadi M and Cortier V Deciding knowledge in security protocols under equational theories Theor. Comput. Sci. 2006 367 1–2 2-32
[2]
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104–115 (2001).
[3]
Abadi M and Fournet C Private authentication Theor. Comput. Sci. 2004 322 3 427-476
[4]
Abadi M and Gordon AD A bisimulation method for cryptographic protocols Nord. J. Comput. 1998 5 4 267-303
[5]
Abadi M, Blanchet B, and Fournet C The applied pi calculus: mobile values, new names, and secure communication J. ACM 2017 65 1 1-41
[6]
Ahn, K.Y., Horne, R., Tiu, A.: A characterisation of open bisimilarity using an intuitionistic modal logic. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory, CONCUR 2017, 5–8 September 2017, Berlin, Germany, vol. 85 of LIPIcs, pp. 7:1–7:17 (2017).
[7]
Ahn, K.Y., Horne, R., Tiu, A.: A characterisation of open bisimilarity using an intuitionistic modal logic. Log. Meth. Comp. Sci. (2021). https://arxiv.org/abs/1701.05324. In press
[8]
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In 23rd IEEE Computer Security Foundations Symposium, pp. 107–121 (2010).
[9]
Ayala-Rincón M, Fernández M, and Nantes-Sobrinho D Intruder deduction problem for locally stable theories with normal forms and inverses Theor. Comput. Sci. 2017 672 64-100
[10]
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Log. Meth. Comp. Sci. 7(1) (2011).
[11]
Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 Proceedings of IEEE Symposium on Security and Privacy, pp. 86–100. IEEE (2004).
[12]
Blanchet B, Abadi M, and Fournet C Automated verification of selected equivalences for security protocols J. Log. Algebr. Program. 2008 75 1 3-51
[13]
Bonchi, F., König, B., Montanari, U.: Saturated semantics for reactive systems. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12–15 August 2006, Seattle, WA, USA, Proceedings, pp. 69–80. IEEE Computer Society (2006).
[14]
Bonchi F, Gadducci F, and Monreale GV A general theory of barbs, contexts, and labels ACM Trans. Comput. Log. 2014 15 4 35:1-35:27
[15]
Boreale M, De Nicola R, and Pugliese R Proof techniques for cryptographic processes SIAM J. Comput. 2001 31 3 947-986
[16]
Borgström J A complete symbolic bisimilarity for an extended Spi calculus Electron. Notes Theor. Comput. Sci. 2009 242 3 3-20
[17]
Borgström J and Nestmann U On bisimulations for the Spi calculus Math. Struct. Comput. Sci. 2005 15 3 487-552
[18]
Borgström J, Briais S, and Nestmann U Gardner P and Yoshida N Symbolic bisimulation in the Spi calculus CONCUR 2004 - Concurrency Theory 2004 Heidelberg Springer 161-176
[19]
Briais S and Nestmann U Open bisimulation, revisited Theor. Comput. Sci. 2007 386 3 236-271
[20]
Bursuc S, Comon-Lundh H, and Delaune S Deducibility constraints and blind signatures Inf. Comput. 2014 238 106-127
[21]
Cheval V and Blanchet B Basin D and Mitchell JC Proving more observational equivalences with ProVerif Principles of Security and Trust 2013 Heidelberg Springer 226-246
[22]
Cheval V, Comon-Lundh H, and Delaune S A procedure for deciding symbolic equivalence between sets of constraint systems Inf. Comput. 2017 255 Part 1 94-125
[23]
Cortier, V., Smyth, B.: Attacking and fixing Helios: an analysis of ballot secrecy. In: 2011 IEEE 24th Computer Security Foundations Symposium, pp. 297–311, June 2011.
[24]
Delaune, S.: Analysing privacy-type properties in cryptographic protocols. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of LIPIcs, Dagstuhl, Germany, pp. 1:1–1:21. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018).
[25]
Delaune S, Kremer S, and Ryan MD Symbolic bisimulation for the applied pi calculus J. Comput. Secur. 2010 18 2 317-377
[26]
Filimonov I, Horne R, Mauw S, and Smith Z Sako K, Schneider S, and Ryan PYA Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity Computer Security – ESORICS 2019 2019 Cham Springer 577-594
[27]
Horne, R.: A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties. Arxiv, arXiv:1811.02536, pp. 1–31 (2018.). https://arxiv.org/abs/1811.02536
[28]
Horne R and Mauw S Discovering ePassport vulnerabilities using bisimilarity Logical Methods in Computer Science 2021 17 2 24:1-24:52
[29]
Horne, R., Ahn, K.Y., Lin, S., Tiu, A.: Quasi-open bisimilarity with mismatch is intuitionistic. In: Dawar, A., Grädel, E. (eds.) Proceedings of LICS 2018: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), Oxford, United Kingdom, 9–12 July 2018, p. 10 (2018).
[30]
Horne, R., Mauw, S., Yurkov, S.: Breaking and fixing unlinkability of the key agreement protocol for 2nd gen EMV payments (2021). https://arxiv.org/abs/2105.02029
[31]
Johansson, M., Bengtson, J., Victor, B., Parrow, J.: Weak equivalences in psi-calculi. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp. 322–331, July 2010.
[32]
Johansson M, Victor B, and Parrow J Computing strong and weak bisimulations for psi-calculi J. Logic Algebraic Program. 2012 81 3 162-180
[33]
Kremer S and Ryan M Sagiv M Analysis of an electronic voting protocol in the applied pi calculus Programming Languages and Systems 2005 Heidelberg Springer 186-200
[34]
Liu J and Lin H A complete symbolic bisimulation for full applied pi calculus Theor. Comput. Sci. 2012 458 76-112
[35]
Milner, R.: The polyadic -calculus: a tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. NATO ASI Series, vol. 94, pp. 203–246 (1993).
[36]
Milner, R., Sangiorgi, D.: Barbed bisimulation, pp. 685–695 (1992).
[37]
Milner R, Parrow J, and Walker D A calculus of mobile processes, Part I and II Inf. Comput. 1992 100 1 1-100
[38]
Montanari U and Sassone V Dynamic congruence vs. progressing bisimulation for CCS Fundam. Inf. 1992 16 2 171-199
[39]
Sangiorgi D Wiedermann J and Hájek P On the proof method for bisimulation Mathematical Foundations of Computer Science 1995 1995 Heidelberg Springer 479-488
[40]
Sangiorgi D A theory of bisimulation for the -calculus Acta Inf. 1996 33 1 69-97
[41]
Sangiorgi D and Walker D Larsen KG and Nielsen M On barbed equivalences in -calculus CONCUR 2001—Concurrency Theory 2001 Heidelberg Springer 292-304
[42]
Tiu A Shao Z A trace based bisimulation for the Spi calculus: an extended abstract Programming Languages and Systems 2007 Heidelberg Springer 367-382
[43]
Tiu A, Nguyen N, and Horne R Igarashi A SPEC: an equivalence checker for security protocols Programming Languages and Systems 2016 Cham Springer 87-95
[44]
Glabbeek, R.J.: The linear time—branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). ISBN 3-540-57208-2
[45]
van Glabbeek RJ and Goltz U Refinement of actions and equivalence notions for concurrent systems Acta Inf. 2001 37 4/5 229-327
Index Terms
- Compositional Analysis of Protocol Equivalence in the Applied -Calculus Using Quasi-open Bisimilarity
Index terms have been assigned to the content through auto-classification.
Recommendations
When privacy fails, a formula describes an attack: A complete and compositional verification method for the applied π-calculus
AbstractWe prove that three semantics for the applied π-calculus coincide – a testing semantics, a labelled equivalence, and a modal logic – and explain how design decisions in each of these semantics are objectively supported by this convergence. Each ...
Highlights- Postulates that a powerful testing equivalence (open barbed bisimilarity) is suited to modelling attacker capabilities in privacy problems.
- Proves that quasi-open bisimilarity, better suited to giving proofs of privacy properties, is ...
Quasi-Open Bisimilarity with Mismatch is Intuitionistic
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceQuasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity ...
Probabilistic bisimilarity as testing equivalence
Larsen and Skou initiated the study of probabilistic bisimilarity and its characterisation in terms of tests. Later on, van Breugel et al. showed that, for labelled Markov processes with continuous state spaces, probabilistic bisimilarity nicely ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sep 2021
406 pages
© The Author(s) 2021.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 06 September 2021
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Horne RMauw SYurkov S(2023)When privacy fails, a formula describes an attackTheoretical Computer Science10.1016/j.tcs.2023.113842959:COnline publication date: 30-May-2023
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in