{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T15:51:13Z","timestamp":1781797873065,"version":"3.54.5"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>The formal analysis of cryptographic protocols traditionally focuses on trace and equivalence properties, for which decision procedures in the symbolic (or Dolev-Yao, or DY) model are known. However, many relevant security properties are expressed as DY hyperproperties that involve quantifications over both execution paths and attacker computations (which are constrained by the attacker\u2019s knowledge in the underlying model of computation). DY hyperproperties generalise hyperproperties, for which many decision procedures exist, to the setting of DY models. Unfortunately, the subtle interactions between both forms of quantifications have been an obstacle to lifting decision procedures from hyperproperties to DY hyperproperties.<\/jats:p>\n          <jats:p>The central contribution of the paper is the first procedure for deciding DY hyperproperties, in the usual setting where the number of protocol sessions is bounded and where the equational theory modelling cryptography is subterm-convergent. We prove that our decision procedure can decide the validity of any hyperproperty in which quantifications over messages are guarded and quantifications over attacker computations are limited to expressing the attacker\u2019s knowledge. We also establish the complexity of the decision problem for several important fragments of the hyperlogic. Further, we illustrate the techniques and scope of our contributions through examples of related hyperproperties.<\/jats:p>","DOI":"10.1145\/3632906","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1913-1944","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Decision and Complexity of Dolev-Yao Hyperproperties"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6587-971X","authenticated-orcid":false,"given":"Itsaka","family":"Rakotonirina","sequence":"first","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"},{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5471-8454","authenticated-orcid":false,"given":"Clara","family":"Schneidewind","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi Bruno Blanchet and C\u00e9dric Fournet. 2018. The Applied Pi Calculus: Mobile Values New Names and Secure Communication. Journal of the ACM (JACM) (2018).","DOI":"10.1145\/3127586"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_2"},{"key":"e_1_3_1_5_1","doi-asserted-by":"crossref","unstructured":"Elvira Albert Shelly Grossman Noam Rinetzky Clara Rodr\u00edguez-N\u00fa\u00f1ez Albert Rubio and Mooly Sagiv. 2020. Taming callbacks for smart contract modularity. Proceedings of the ACM on Programming Languages (2020).","DOI":"10.1145\/3428277"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"e_1_3_1_8_1","doi-asserted-by":"crossref","unstructured":"Lukas Aumayr Matteo Maffei Oguzhan Ersoy Andreas Erwig Sebastian Faust Siavash Riahi Kristina Host\u00e1kov\u00e1 and Pedro Moreno-Sanchez. 2021. Bitcoin-compatible virtual channels. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE 901\u2013918.","DOI":"10.1109\/SP40001.2021.00097"},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"Lukas Aumayr Pedro Moreno-Sanchez Aniket Kate and Matteo Maffei. 2023. Breaking and Fixing Virtual Channels: Domino Attack and Donner. In Network and Distributed System Security Symposium (NDSS).","DOI":"10.14722\/ndss.2023.24370"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Michael Backes Jannik Dreier Steve Kremer and Robert K\u00fcnnemann. 2017. A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange. In IEEE European Symposium on Security and Privacy (EuroS&P).","DOI":"10.1109\/EuroSP.2017.12"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166956.2166962"},{"key":"e_1_3_1_12_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Ugo Dal Lago Giulio Malavolta and Itsaka Rakotonirina. 2022. Tidy: Symbolic Verification of Timed Cryptographic Protocols. In ACM Conference on Computer and Communications Security (CCS).","DOI":"10.1145\/3548606.3559343"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535847"},{"key":"e_1_3_1_14_1","unstructured":"David Basin Cas Cremers Jannik Dreier Simon Meier Ralf Sasse and Benedikt Schmidt. 2019. Tamarin prover manual. https:\/\/tamarin-prover.github.io\/."},{"key":"e_1_3_1_15_1","volume-title":"S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires","author":"Baudet Mathieu","year":"2007","unstructured":"Mathieu Baudet. 2007. S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires. Ph.D. Dissertation. \u00c9cole normale sup\u00e9rieure de Cachan."},{"key":"e_1_3_1_16_1","unstructured":"Mario RF Benevides and Luiz CF Fernandez. 2021. Tableaux Calculus for Dolev-Yao Multi-Agent Epistemic Logic. Logical and Semantic Frameworks with Applications (LSFA) (2021)."},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Raven Beutner and Bernd Finkbeiner. 2022. A Logic for Hyperproperties in Multi-Agent Systems. arXiv preprint arXiv:2203.07283 (2022).","DOI":"10.46298\/lmcs-19(2:13)2023"},{"key":"e_1_3_1_18_1","doi-asserted-by":"crossref","unstructured":"Raven Beutner Bernd Finkbeiner Hadar Frenkel and Niklas Metzger. 2023. Second-order hyperproperties. arXiv preprint arXiv:2305.17935 (2023).","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"e_1_3_1_19_1","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan Abhishek Bichhawat Quoc Huy Do Pedram Hosseyni Ralf K\u00fcsters Guido Schmitz and Tim W\u00fcrtele. 2021. DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE 523\u2013542.","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_1_21_1","unstructured":"Bruno Blanchet Ben Smyth Vincent Cheval and Marc Sylvestre. 2020. Automatic Cryptographic Protocol Verifier User Manual and Tutorial. https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf."},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44598-6_15"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"Rohit Chadha Vincent Cheval Stefan Ciob\u00e2c\u00e0 and Steve Kremer. 2016. Automated verification of equivalence properties of cryptographic protocol. ACM Transactions on Computational Logic (2016).","DOI":"10.1145\/2926715"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"Vincent Cheval V\u00e9ronique Cortier and St\u00e9phanie Delaune. 2013. Deciding equivalence-based properties using constraint solving. Theoretical Computer Science (2013).","DOI":"10.1016\/j.tcs.2013.04.016"},{"key":"e_1_3_1_25_1","unstructured":"Vincent Cheval Charlie Jacomme Steve Kremer and Robert K\u00fcnnemann. 2022. Sapic+ : protocol verifiers of the world unite!. In USENIX Security Symposium."},{"key":"e_1_3_1_26_1","doi-asserted-by":"crossref","unstructured":"Vincent Cheval Steve Kremer and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding equivalence properties in security protocols theory and practice. In IEEE Symposium on Security and Privacy (S&P).","DOI":"10.1109\/SP.2018.00033"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Vincent Cheval Steve Kremer and Itsaka Rakotonirina. 2019. Exploiting symmetries when proving equivalence properties for security protocols. In ACM Conference on Computer and Communications Security (CCS).","DOI":"10.1145\/3319535.3354260"},{"key":"e_1_3_1_28_1","doi-asserted-by":"crossref","unstructured":"Vincent Cheval Steve Kremer and Itsaka Rakotonirina. 2020a. The hitchhiker\u2019s guide to decidability and complexity of equivalence properties in security protocols. In Logic Language and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday (ScedrovFest65).","DOI":"10.1007\/978-3-030-62077-6_10"},{"key":"e_1_3_1_29_1","unstructured":"Vincent Cheval Steve Kremer Itsaka Rakotonirina and Victor Yon. 2020b. DeepSec user manual. https:\/\/deepsec-prover.github.io\/."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"Norine Coenen Bernd Finkbeiner Christopher Hahn and Jana Hofmann. 2019. The hierarchy of hyperlogics. In ACM\/IEEE Symposium on Logic in Computer Science (LICS).","DOI":"10.1109\/LICS.2019.8785713"},{"key":"e_1_3_1_33_1","unstructured":"Norine Coenen Bernd Finkbeiner Jana Hofmann and Julia Tillman. 2022. Smart Contract Synthesis Modulo Hyperproperties. arXiv preprint arXiv:2208.07180 (2022)."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2004-12203"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","unstructured":"Stefan Dziembowski Lisa Eckey Sebastian Faust and Daniel Malinowski. 2019. Perun: Virtual payment hubs over cryptocurrencies. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE 106\u2013123.","DOI":"10.1109\/SP.2019.00020"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33170-1_22"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_3_1_41_1","doi-asserted-by":"crossref","unstructured":"Shelly Grossman Ittai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv and Yoni Zohar. 2017. Online detection of effectively callback free objects with applications to smart contracts. Proceedings of the ACM on Programming Languages (2017).","DOI":"10.1145\/3158136"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00023"},{"key":"e_1_3_1_43_1","unstructured":"Tzu-Han Hsu Borzoo Bonakdarpour Bernd Finkbeiner and C\u00e9sar S\u00e1nchez. 2023. Bounded Model Checking for Asynchronous Hyperproperties. arXiv preprint arXiv:2301.07208 (2023)."},{"key":"e_1_3_1_44_1","doi-asserted-by":"crossref","unstructured":"Max I. Kanovich Tajana Ban Kirigin Vivek Nigam and Andre Scedrov. 2014. Bounded memory protocols. Computer Languages Systems & Structures (2014).","DOI":"10.1016\/j.cl.2014.05.003"},{"key":"e_1_3_1_45_1","doi-asserted-by":"crossref","unstructured":"Steve Kremer and Robert K\u00fcnnemann. 2016. Automated analysis of security protocols with global state. Journal of Computer Security (JCS) (2016).","DOI":"10.3233\/JCS-160556"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/2846460.2846535"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_12"},{"key":"e_1_3_1_48_1","unstructured":"Corto Mascle and Martin Zimmermann. 2019. The keys to decidable hyperltl satisfiability: Small models or very simple formulas. arXiv preprint arXiv:1907.05070."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Anton Permenev Dimitar K. Dimitrov Petar Tsankov Dana Drachsler-Cohen and Martin T. Vechev. 2020. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy SP 2020 San Francisco CA USA May 18-21 2020. IEEE 1661\u20131677. https:\/\/doi.org\/10.1109\/SP40000.2020.00024 10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_3_1_50_1","unstructured":"Joseph Poon and Thaddeus Dryja. 2016. The bitcoin lightning network: Scalable off-chain instant payments. (2016)."},{"key":"e_1_3_1_51_1","volume-title":"Efficient verification of observational equivalences of cryptographic processes: theory and practice.","author":"Rakotonirina Itsaka","year":"2021","unstructured":"Itsaka Rakotonirina. 2021. Efficient verification of observational equivalences of cryptographic processes: theory and practice. Ph. D. Dissertation. Universit\u00e9 de Lorraine."},{"key":"e_1_3_1_52_1","volume-title":"ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"Rakotonirina Itsaka","year":"2024","unstructured":"Itsaka Rakotonirina, Gilles Barthe, and Clara Schneidewind. 2024. Decision and Complexity of Dolev-Yao Hyperproperties (Technical Report). In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM (Ed.). Available at https:\/\/hal.science\/hal-04261390."},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00490-5"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Jon Stephens Kostas Ferles Benjamin Mariano Shuvendu K. Lahiri and Isil Dillig. 2021. SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. In 42nd IEEE Symposium on Security and Privacy SP 2021 San Francisco CA USA 24-27 May 2021. IEEE 555\u2013571. https:\/\/doi.org\/10.1109\/SP40001.2021.00085 10.1109\/SP40001.2021.00085","DOI":"10.1109\/SP40001.2021.00085"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632906","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632906","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:01:53Z","timestamp":1751659313000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632906"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632906"],"URL":"https:\/\/doi.org\/10.1145\/3632906","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}