{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,29]],"date-time":"2026-10-29T18:29:49Z","timestamp":1793298589213,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T00:00:00Z","timestamp":1667779200000},"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":[],"published-print":{"date-parts":[[2022,11,7]]},"DOI":"10.1145\/3548606.3559343","type":"proceedings-article","created":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T11:41:28Z","timestamp":1667821288000},"page":"263-276","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Tidy: Symbolic Verification of Timed Cryptographic Protocols"],"prefix":"10.1145","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI-SP & IMDEA Software Institute, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna & INRIA Sophia Antipolis, Bologna, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giulio","family":"Malavolta","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Itsaka","family":"Rakotonirina","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,11,7]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44929-9_1"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_3_2_2_5_1","volume-title":"Protocol Analysis with Time. In International Conference on Cryptology in India (INDOCRYPT)","author":"Aparicio-S\u00e1nchez Dami\u00e1n","year":"2020","unstructured":"Dami\u00e1n Aparicio-S\u00e1nchez , Santiago Escobar , Catherine Meadows , Jos\u00e9 Meseguer , and Julia Sapi na. 2020 . Protocol Analysis with Time. In International Conference on Cryptology in India (INDOCRYPT) . Springer, India, 128--150. Dami\u00e1n Aparicio-S\u00e1nchez, Santiago Escobar, Catherine Meadows, Jos\u00e9 Meseguer, and Julia Sapi na. 2020. Protocol Analysis with Time. In International Conference on Cryptology in India (INDOCRYPT). Springer, India, 128--150."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.19.403-429"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.12"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2012.27"},{"key":"e_1_3_2_2_9_1","volume-title":"SoK: Computer-Aided Cryptography. IEEE Symposium on Security and Privacy (S&P).","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa , Gilles Barthe , Karthik Bhargavan , Bruno Blanchet , Cas Cremers , Kevin Liao , and Bryan Parno . 2021 . SoK: Computer-Aided Cryptography. IEEE Symposium on Security and Privacy (S&P). Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. IEEE Symposium on Security and Privacy (S&P)."},{"key":"e_1_3_2_2_10_1","volume-title":"Giulio Malavolta, and Itsaka Rakotonirina.","author":"Barthe Gilles","year":"2022","unstructured":"Gilles Barthe , Ugo Dal Lago , Giulio Malavolta, and Itsaka Rakotonirina. 2022 . Tidy : Symbolic Verification of Timed Cryptographic Protocols (technical report). Technical Report. MPI-SP, University of Bologna, IMDEA Software Institute . Available at: https:\/\/gitlab.com\/irakoton\/20-timed-dy\/-\/releases\/tech-report. Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, and Itsaka Rakotonirina. 2022. Tidy: Symbolic Verification of Timed Cryptographic Protocols (technical report). Technical Report. MPI-SP, University of Bologna, IMDEA Software Institute. Available at: https:\/\/gitlab.com\/irakoton\/20-timed-dy\/-\/releases\/tech-report."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2019599.2019601"},{"key":"e_1_3_2_2_12_1","unstructured":"David Basin Cas Cremers Jannik Dreier Simon Meier Ralf Sasse and Benedikt Schmidt. 2019. Tamarin prover manual. https:\/\/tamarin-prover.github.io\/.  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_2_2_13_1","unstructured":"Mathieu Baudet. 2007. S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires. Ph. D. Dissertation. \u00c9cole normale sup\u00e9rieure de Cachan-ENS Cachan. In French.  Mathieu Baudet. 2007. S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires. Ph. D. Dissertation. \u00c9cole normale sup\u00e9rieure de Cachan-ENS Cachan. In French."},{"key":"e_1_3_2_2_14_1","volume-title":"Jesper Buus Nielsen, and Sabine Oechsner","author":"Baum Carsten","year":"2021","unstructured":"Carsten Baum , Bernardo David , Rafael Dowsley , Jesper Buus Nielsen, and Sabine Oechsner . 2021 . TARDIS : A Foundation of Time-Lock Puzzles in UC. In Advances in Cryptology (EUROCRYPT). Springer , Zagreb, Croatia, 429--459. Carsten Baum, Bernardo David, Rafael Dowsley, Jesper Buus Nielsen, and Sabine Oechsner. 2021. TARDIS: A Foundation of Time-Lock Puzzles in UC. In Advances in Cryptology (EUROCRYPT). Springer, Zagreb, Croatia, 429--459."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840745"},{"key":"e_1_3_2_2_16_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.  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_2_2_17_1","volume-title":"Annual international cryptology conference (CRYPTO)","author":"Boneh Dan","unstructured":"Dan Boneh , Joseph Bonneau , Benedikt B\u00fcnz , and Ben Fisch . 2018. Verifiable delay functions . In Annual international cryptology conference (CRYPTO) . Springer , Santa Barbara, CA, USA , 757--788. Dan Boneh, Joseph Bonneau, Benedikt B\u00fcnz, and Ben Fisch. 2018. Verifiable delay functions. In Annual international cryptology conference (CRYPTO). Springer, Santa Barbara, CA, USA, 757--788."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44598-6_15"},{"key":"e_1_3_2_2_19_1","unstructured":"Joseph Bonneau Jeremy Clark and Steven Goldfeder. 2015. On Bitcoin as a public randomness source. IACR Cryptol. ePrint Arch. Available at: https:\/\/eprint.iacr.org\/2015\/1015.pdf.  Joseph Bonneau Jeremy Clark and Steven Goldfeder. 2015. On Bitcoin as a public randomness source. IACR Cryptol. ePrint Arch. Available at: https:\/\/eprint.iacr.org\/2015\/1015.pdf."},{"key":"e_1_3_2_2_20_1","volume-title":"Advances in Cryptology (EUROCRYPT)","author":"Burdges Jeffrey","unstructured":"Jeffrey Burdges and Luca De Feo . 2021. Delay Encryption . In Advances in Cryptology (EUROCRYPT) . Springer , Zagreb, Croatia , 429--459. Jeffrey Burdges and Luca De Feo. 2021. Delay Encryption. In Advances in Cryptology (EUROCRYPT). Springer, Zagreb, Croatia, 429--459."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9019-5"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.04.016"},{"key":"e_1_3_2_2_24_1","volume-title":"Logic, Language, and Security","author":"Cheval Vincent","unstructured":"Vincent Cheval , Steve Kremer , and Itsaka Rakotonirina . 2020. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols . In Logic, Language, and Security . Springer , France , 127--145. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2020. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. In Logic, Language, and Security. Springer, France, 127--145."},{"key":"e_1_3_2_2_25_1","unstructured":"Jeremy Clark and Urs Hengartner. 2010. On the Use of Financial Data as a Random Beacon. Usenix EVT\/WOTE.  Jeremy Clark and Urs Hengartner. 2010. On the Use of Financial Data as a Random Beacon. Usenix EVT\/WOTE."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12168"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785713"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_7"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48000-7_29"},{"key":"e_1_3_2_2_34_1","unstructured":"Bernd Finkbeiner and Christopher Hahn. 2016. Deciding hyperproperties. arXiv preprint arXiv:1606.07047.  Bernd Finkbeiner and Christopher Hahn. 2016. Deciding hyperproperties. arXiv preprint arXiv:1606.07047."},{"key":"e_1_3_2_2_35_1","volume-title":"Computer Aided Verification (CAV)","author":"Finkbeiner Bernd","unstructured":"Bernd Finkbeiner , Markus N. Rabe , and C\u00e9sar S\u00e1nchez . 2015. Algorithms for Model Checking HyperLTL and HyperCTL* . In Computer Aided Verification (CAV) . Springer , San Fransisco, CA, USA , 30--48. Bernd Finkbeiner, Markus N. Rabe, and C\u00e9sar S\u00e1nchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL*. In Computer Aided Verification (CAV). Springer, San Fransisco, CA, USA, 30--48."},{"key":"e_1_3_2_2_36_1","volume-title":"Non-malleable Time-Lock Puzzles and Applications. In Theory of Cryptography Conference (TCC). Springer, Raleigh, United States, 447--479","author":"Freitag Cody","year":"2021","unstructured":"Cody Freitag , Ilan Komargodski , Rafael Pass , and Naomi Sirkin . 2021 . Non-malleable Time-Lock Puzzles and Applications. In Theory of Cryptography Conference (TCC). Springer, Raleigh, United States, 447--479 . Cody Freitag, Ilan Komargodski, Rafael Pass, and Naomi Sirkin. 2021. Non-malleable Time-Lock Puzzles and Applications. In Theory of Cryptography Conference (TCC). Springer, Raleigh, United States, 447--479."},{"key":"e_1_3_2_2_37_1","volume-title":"International Conference on Financial Cryptography (FC). Springer, Southampton, Bermuda, 168--182","author":"Garay Juan A","year":"2002","unstructured":"Juan A Garay and Markus Jakobsson . 2002 . Timed release of standard digital signatures . In International Conference on Financial Cryptography (FC). Springer, Southampton, Bermuda, 168--182 . Juan A Garay and Markus Jakobsson. 2002. Timed release of standard digital signatures. In International Conference on Financial Cryptography (FC). Springer, Southampton, Bermuda, 168--182."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0055-4"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104639"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214884"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64381-2_14"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64381-2_14"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160556"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74835-9_40"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_37"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2002.1021817"},{"key":"e_1_3_2_2_47_1","unstructured":"Arjen K Lenstra and Benjamin Wesolowski. 2015. A random zoo: sloth unicorn and trx. IACR Cryptol. ePrint Arch..  Arjen K Lenstra and Benjamin Wesolowski. 2015. A random zoo: sloth unicorn and trx. IACR Cryptol. ePrint Arch.."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_22"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-26948-7_22"},{"key":"e_1_3_2_2_50_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.  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_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00001"},{"key":"e_1_3_2_2_52_1","unstructured":"Vivek Nigam Carolyn Talcott and Abraao Aires Urquiza. 2018. Symbolic timed observational equivalence. arXiv preprint arXiv:1801.04066.  Vivek Nigam Carolyn Talcott and Abraao Aires Urquiza. 2018. Symbolic timed observational equivalence. arXiv preprint arXiv:1801.04066."},{"key":"e_1_3_2_2_53_1","volume-title":"Time-lock puzzles and timed-release crypto","author":"Rivest Ronald L","unstructured":"Ronald L Rivest , Adi Shamir , and David A Wagner . 1996. Time-lock puzzles and timed-release crypto . Massachusetts Institute of Technology . Laboratory for Computer Science. Ronald L Rivest, Adi Shamir, and David A Wagner. 1996. Time-lock puzzles and timed-release crypto. Massachusetts Institute of Technology. Laboratory for Computer Science."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00490-5"},{"key":"e_1_3_2_2_55_1","volume-title":"International Symposium on Trustworthy Global Computing (TGC). Springer","author":"Saeedloei Neda","year":"2013","unstructured":"Neda Saeedloei and Gopal Gupta . 2013 . Timed pi-Calculus . In International Symposium on Trustworthy Global Computing (TGC). Springer , Buenos Aires, Argentina, 119--135. Neda Saeedloei and Gopal Gupta. 2013. Timed pi-Calculus. In International Symposium on Trustworthy Global Computing (TGC). Springer, Buenos Aires, Argentina, 119--135."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00141-4"},{"key":"e_1_3_2_2_57_1","volume-title":"Verifiable Timed Signatures Made Practical. ACM Conference on Computer and Communications Security (CCS).","author":"Krishnan Thyagarajan Sri Aravinda","year":"2020","unstructured":"Sri Aravinda Krishnan Thyagarajan , Adithya Bhat , Giulio Malavolta , Nico D\u00f6ttling , Aniket Kate , and Dominique Schr\u00f6der . 2020 . Verifiable Timed Signatures Made Practical. ACM Conference on Computer and Communications Security (CCS). Sri Aravinda Krishnan Thyagarajan, Adithya Bhat, Giulio Malavolta, Nico D\u00f6ttling, Aniket Kate, and Dominique Schr\u00f6der. 2020. Verifiable Timed Signatures Made Practical. ACM Conference on Computer and Communications Security (CCS)."}],"event":{"name":"CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications Security","location":"Los Angeles CA USA","acronym":"CCS '22","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3548606.3559343","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3548606.3559343","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:50:56Z","timestamp":1750182656000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3548606.3559343"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,7]]},"references-count":55,"alternative-id":["10.1145\/3548606.3559343","10.1145\/3548606"],"URL":"https:\/\/doi.org\/10.1145\/3548606.3559343","relation":{},"subject":[],"published":{"date-parts":[[2022,11,7]]},"assertion":[{"value":"2022-11-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}