{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T04:45:27Z","timestamp":1741668327338,"version":"3.38.0"},"reference-count":30,"publisher":"SAGE Publications","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2023,10,13]]},"abstract":"<jats:p>Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied \u03c0-calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has\u00a0\u2013 maybe surprisingly\u00a0\u2013 a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.<\/jats:p>","DOI":"10.3233\/jcs-230037","type":"journal-article","created":{"date-parts":[[2023,6,13]],"date-time":"2023-06-13T14:27:34Z","timestamp":1686666454000},"page":"501-538","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic protocol verification with dice1"],"prefix":"10.1177","volume":"31","author":[{"given":"Vincent","family":"Cheval","sequence":"first","affiliation":[{"name":"Inria Paris, France"}]},{"given":"Rapha\u00eblle","family":"Crubill\u00e9","sequence":"additional","affiliation":[{"name":"CNRS, LIS, Aix Marseille Univ, Universit\u00e9 de Toulon, France"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[{"name":"Inria Nancy, LORIA,Universit\u00e9 de Lorraine, France"}]}],"member":"179","reference":[{"doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi, B.\u00a0Blanchet and C.\u00a0Fournet, The applied pi calculus: Mobile values, new names, and secure communication, Journal of the ACM (JACM) (2017).","key":"10.3233\/JCS-230037_ref1","DOI":"10.1145\/3127586"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref2","DOI":"10.1007\/978-3-642-15240-5_5"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref4","DOI":"10.1145\/3243734.3243846"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref5","DOI":"10.1109\/SP40001.2021.00037"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref6","DOI":"10.1007\/978-3-319-96142-2_10"},{"doi-asserted-by":"crossref","unstructured":"K.\u00a0Bhargavan, B.\u00a0Blanchet and N.\u00a0Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, in: IEEE Symposium on Security and Privacy (S&P\u201917), IEEE, 2017, pp.\u00a0483\u2013502.","key":"10.3233\/JCS-230037_ref7","DOI":"10.1109\/SP.2017.26"},{"doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security (2016).","key":"10.3233\/JCS-230037_ref8","DOI":"10.1561\/9781680832075"},{"doi-asserted-by":"crossref","unstructured":"F.\u00a0Bonchi, A.\u00a0Sokolova and V.\u00a0Vignudelli, The theory of traces for systems with nondeterminism and probability, in: 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), IEEE, 2019, pp.\u00a01\u201314.","key":"10.3233\/JCS-230037_ref9","DOI":"10.1109\/LICS.2019.8785673"},{"doi-asserted-by":"crossref","unstructured":"V.\u00a0Castiglioni, Trace and testing metrics on nondeterministic probabilistic processes, in: Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics and 15th Workshop on Structural Operational Semantics, (EXPRESS\/SOS) 2018, Vol.\u00a0276, 2018, pp.\u00a019\u201336.","key":"10.3233\/JCS-230037_ref10","DOI":"10.4204\/EPTCS.276.0"},{"doi-asserted-by":"crossref","unstructured":"R.\u00a0Chadha, A.P.\u00a0Sistla and M.\u00a0Viswanathan, Verification of randomized security protocols, in: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917), IEEE, 2017, pp.\u00a01\u201312.","key":"10.3233\/JCS-230037_ref11","DOI":"10.1109\/LICS.2017.8005126"},{"issue":"6","key":"10.3233\/JCS-230037_ref12","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1016\/j.ic.2009.06.006","article-title":"Making random choices invisible to the scheduler","volume":"208","author":"Chatzikokolakis","year":"2010","journal-title":"Inf. Comput."},{"issue":"2","key":"10.3233\/JCS-230037_ref13","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/358549.358563","article-title":"Untraceable electronic mail, return addresses, and digital pseudonyms","volume":"24","author":"Chaum","year":"1981","journal-title":"Commun. ACM"},{"issue":"1","key":"10.3233\/JCS-230037_ref14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","article-title":"The dining cryptographers problem: Unconditional sender and recipient untraceability","volume":"1","author":"Chaum","year":"1988","journal-title":"J. Cryptol."},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref15","DOI":"10.1007\/11555827_8"},{"key":"10.3233\/JCS-230037_ref16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.04.016","article-title":"Deciding equivalence-based properties using constraint solving","volume":"492","author":"Cheval","year":"2013","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref18","DOI":"10.1109\/SP.2018.00033"},{"issue":"4","key":"10.3233\/JCS-230037_ref19","doi-asserted-by":"publisher","first-page":"1914","DOI":"10.1007\/s00145-020-09360-1","article-title":"A formal security analysis of the signal messaging protocol","volume":"33","author":"Cohn-Gordon","year":"2020","journal-title":"Journal of Cryptology"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref20","DOI":"10.1145\/1455770.1455786"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref21","DOI":"10.1109\/CSF.2009.9"},{"issue":"3\u20134","key":"10.3233\/JCS-230037_ref22","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s10817-010-9187-9","article-title":"A survey of symbolic methods in computational analysis of cryptographic systems","volume":"46","author":"Cortier","year":"2010","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"C.\u00a0Cremers, M.\u00a0Horvat, J.\u00a0Hoyland, S.\u00a0Scott and T.\u00a0van der Merwe, A comprehensive symbolic analysis of TLS 1.3, in: ACM SIGSAC Conference on Computer and Communications Security (CCS\u201917), ACM, 2017, pp.\u00a01773\u20131788.","key":"10.3233\/JCS-230037_ref23","DOI":"10.1145\/3133956.3134063"},{"doi-asserted-by":"crossref","unstructured":"Y.\u00a0Deng, R.\u00a0Van Glabbeek, M.\u00a0Hennessy and C.\u00a0Morgan, Testing finitary probabilistic processes, in: International Conference on Concurrency Theory, Springer, 2009, pp.\u00a0274\u2013288.","key":"10.3233\/JCS-230037_ref25","DOI":"10.1007\/978-3-642-04081-8_19"},{"issue":"2","key":"10.3233\/JCS-230037_ref26","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inf. Theory"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref28","DOI":"10.1007\/978-3-540-76637-7_12"},{"doi-asserted-by":"publisher","key":"10.3233\/JCS-230037_ref29","DOI":"10.1007\/3-540-10003-2_79"},{"issue":"1","key":"10.3233\/JCS-230037_ref30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, I","volume":"100","author":"Milner","year":"1992","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0Parma and R.\u00a0Segala, Logical characterizations of bisimulations for discrete probabilistic systems, in: International Conference on Foundations of Software Science and Computational Structures, Springer, 2007, pp.\u00a0287\u2013301.","key":"10.3233\/JCS-230037_ref31","DOI":"10.1007\/978-3-540-71389-0_21"},{"issue":"1","key":"10.3233\/JCS-230037_ref32","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","article-title":"Crowds: Anonymity for web transactions","volume":"1","author":"Reiter","year":"1998","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"2","key":"10.3233\/JCS-230037_ref33","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala","year":"1995","journal-title":"Nordic Journal of Computing"},{"doi-asserted-by":"crossref","unstructured":"R.J.\u00a0van Glabbeek, Bounded nondeterminism and the approximation induction principle in process algebra, in: Annual Symposium on Theoretical Aspects of Computer Science, Springer, 1987, pp.\u00a0336\u2013347.","key":"10.3233\/JCS-230037_ref36","DOI":"10.1007\/BFb0039617"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-230037","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T02:53:38Z","timestamp":1741661618000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/JCS-230037"}},"subtitle":["Process equivalences in the presence of probabilities"],"editor":[{"given":"Stefano","family":"Calzavara","sequence":"additional","affiliation":[]},{"given":"David","family":"Naumann","sequence":"additional","affiliation":[]}],"short-title":[],"issued":{"date-parts":[[2023,10,13]]},"references-count":30,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.3233\/jcs-230037","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"type":"electronic","value":"1875-8924"},{"type":"print","value":"0926-227X"}],"subject":[],"published":{"date-parts":[[2023,10,13]]}}}