{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:19Z","timestamp":1750220659902,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,9]],"date-time":"2020-11-09T00:00:00Z","timestamp":1604880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,13]]},"DOI":"10.1145\/3411506.3417596","type":"proceedings-article","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T21:13:27Z","timestamp":1604351607000},"page":"19-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Short Paper: Modular Black-box Runtime Verification of Security Protocols"],"prefix":"10.1145","author":[{"given":"Kevin","family":"Morio","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]},{"given":"Dennis","family":"Jackson","sequence":"additional","affiliation":[{"name":"ETH Z\u00fcrich, Z\u00fcrich, Switzerland"}]},{"given":"Marco","family":"Vassena","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]},{"given":"Robert","family":"K\u00fcnnemann","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,11,9]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_3_2_2_2_1","volume-title":"TLS 1.3 session resumption works without master key, allowing MITM. https:\/\/gitlab.com\/gnutls\/gnutls\/-\/issues\/1011 (Accessed June 26th","author":"Airtower TLS","year":"2020","unstructured":"Gnu TLS Airtower . 2020. CVE-2020--13777 : TLS 1.3 session resumption works without master key, allowing MITM. https:\/\/gitlab.com\/gnutls\/gnutls\/-\/issues\/1011 (Accessed June 26th , 2020 ). GnuTLS Airtower. 2020. CVE-2020--13777: TLS 1.3 session resumption works without master key, allowing MITM. https:\/\/gitlab.com\/gnutls\/gnutls\/-\/issues\/1011 (Accessed June 26th, 2020)."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241094.3241100"},{"key":"e_1_3_2_2_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"FM 2012: Formal Methods, , Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.)","author":"Barringer Howard","unstructured":"Howard Barringer , Yli\u00e8s Falcone , Klaus Havelund , Giles Reger , and David Rydeheard . 2012. Quantified Event Automata : Towards Expressive and Efficient Runtime Monitors . In FM 2012: Formal Methods, , Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) . Lecture Notes in Computer Science , Vol. 7436 . Springer Berlin Heidelberg , 68--84. https:\/\/doi.org\/10.1007\/978--3--642--32759--9_9 10.1007\/978--3--642--32759--9_9 Howard Barringer, Yli\u00e8s Falcone, Klaus Havelund, Giles Reger, and David Rydeheard. 2012. Quantified Event Automata : Towards Expressive and Efficient Runtime Monitors. In FM 2012: Formal Methods, , Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.). Lecture Notes in Computer Science, Vol. 7436. Springer Berlin Heidelberg, 68--84. https:\/\/doi.org\/10.1007\/978--3--642--32759--9_9"},{"key":"e_1_3_2_2_5_1","first-page":"996","article-title":"Multi-user Schnorr security, revisited","volume":"2015","author":"Bernstein Daniel J.","year":"2015","unstructured":"Daniel J. Bernstein . 2015 . Multi-user Schnorr security, revisited . IACR Cryptology ePrint Archive , Vol. 2015 (2015), 996 . Daniel J. Bernstein. 2015. Multi-user Schnorr security, revisited. IACR Cryptology ePrint Archive, Vol. 2015 (2015), 996.","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_6_1","volume-title":"A Verified Modern Cryptographic Library. ACM CCS (September","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan , Benjamin Beurdouche , Jean-Karim Zinzindohou\u00e9 , and Jonathan Protzenko . 2017. HACL* : A Verified Modern Cryptographic Library. ACM CCS (September 2017 ). https:\/\/www.microsoft.com\/en-us\/research\/publication\/hacl-a-verified-modern-cryptographic-library\/ Karthikeyan Bhargavan, Benjamin Beurdouche, Jean-Karim Zinzindohou\u00e9, and Jonathan Protzenko. 2017. HACL*: A Verified Modern Cryptographic Library. ACM CCS (September 2017). https:\/\/www.microsoft.com\/en-us\/research\/publication\/hacl-a-verified-modern-cryptographic-library\/"},{"key":"e_1_3_2_2_7_1","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th Computer Security Foundations Workshop (CSFW'01)","author":"Blanchet Bruno","year":"2001","unstructured":"Bruno Blanchet . 2001 . An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th Computer Security Foundations Workshop (CSFW'01) . IEEE Comp. Soc., 82--96. Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th Computer Security Foundations Workshop (CSFW'01). IEEE Comp. Soc., 82--96."},{"volume-title":"Automatic verification of security protocols in the symbolic model: The verifier proverif","author":"Blanchet Bruno","key":"e_1_3_2_2_8_1","unstructured":"Bruno Blanchet . 2013. Automatic verification of security protocols in the symbolic model: The verifier proverif . In Foundations of Security Analysis and Design VII. Springer , 54--87. Bruno Blanchet. 2013. Automatic verification of security protocols in the symbolic model: The verifier proverif. In Foundations of Security Analysis and Design VII. Springer, 54--87."},{"key":"e_1_3_2_2_9_1","volume-title":"Proceedings of the USENIX Security Symposium. USENIX. https:\/\/www.microsoft.com\/en-us\/research\/publication\/vale-verifying-high-performance-cryptographic-assembly-code\/ Distinguished Paper Award.","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , Rustan Leino , Jay Lorch , Bryan Parno , Ashay Rane , Srinath Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code . In Proceedings of the USENIX Security Symposium. USENIX. https:\/\/www.microsoft.com\/en-us\/research\/publication\/vale-verifying-high-performance-cryptographic-assembly-code\/ Distinguished Paper Award. Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the USENIX Security Symposium. USENIX. https:\/\/www.microsoft.com\/en-us\/research\/publication\/vale-verifying-high-performance-cryptographic-assembly-code\/ Distinguished Paper Award."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00019"},{"key":"e_1_3_2_2_11_1","volume-title":"Advances in Cryptology - ASIACRYPT","author":"Raymond Choo Kim-Kwang","year":"2005","unstructured":"Kim-Kwang Raymond Choo , Colin Boyd , and Yvonne Hitchcock . 2005. Errors in Computational Complexity Proofs for Protocols . In Advances in Cryptology - ASIACRYPT 2005 , 11th International Conference on the Theory and Application of Cryptology and Information Security, Chennai, India, December 4--8, 2005, Proceedings (Lecture Notes in Computer Science),, Bimal K. Roy (Ed.), Vol. 3788 . Springer , 624--643. https:\/\/doi.org\/10.1007\/11593447_34 10.1007\/11593447_34 Kim-Kwang Raymond Choo, Colin Boyd, and Yvonne Hitchcock. 2005. Errors in Computational Complexity Proofs for Protocols. In Advances in Cryptology - ASIACRYPT 2005, 11th International Conference on the Theory and Application of Cryptology and Information Security, Chennai, India, December 4--8, 2005, Proceedings (Lecture Notes in Computer Science),, Bimal K. Roy (Ed.), Vol. 3788. Springer, 624--643. https:\/\/doi.org\/10.1007\/11593447_34"},{"key":"e_1_3_2_2_12_1","volume-title":"WireGuard: Next Generation Kernel Network Tunnel. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017","author":"Donenfeld Jason A.","year":"2017","unstructured":"Jason A. Donenfeld . 2017 . WireGuard: Next Generation Kernel Network Tunnel. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017 , San Diego, California, USA, February 26 - March 1, 2017. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2017\/ndss-2017-programme\/wireguard-next-generation-kernel-network-tunnel\/ Jason A. Donenfeld. 2017. WireGuard: Next Generation Kernel Network Tunnel. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26 - March 1, 2017. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2017\/ndss-2017-programme\/wireguard-next-generation-kernel-network-tunnel\/"},{"volume-title":"Runtime Verification, , Christian Colombo and Martin Leucker (Eds.).","author":"Falcone Yli\u00e8s","key":"e_1_3_2_2_13_1","unstructured":"Yli\u00e8s Falcone , Giles Reger , and Dmitriy Traytel . 2018. A Taxonomy for Classifying Runtime Verification Tools . In Runtime Verification, , Christian Colombo and Martin Leucker (Eds.). Vol. 11237 . Springer International Publishing , Cham , 241--262. https:\/\/doi.org\/10.1007\/978--3-030-03769--7_14 10.1007\/978--3-030-03769--7_14 Yli\u00e8s Falcone, Giles Reger, and Dmitriy Traytel. 2018. A Taxonomy for Classifying Runtime Verification Tools. In Runtime Verification, , Christian Colombo and Martin Leucker (Eds.). Vol. 11237. Springer International Publishing, Cham, 241--262. https:\/\/doi.org\/10.1007\/978--3-030-03769--7_14"},{"key":"e_1_3_2_2_14_1","volume-title":"International Journal on Software Tools for Technology Transfer (02","author":"Finkbeiner Bernd","year":"2020","unstructured":"Bernd Finkbeiner , Christopher Hahn , Marvin Stenger , and Leander Tentrup . 2020. Efficient monitoring of hyperproperties using prefix trees . International Journal on Software Tools for Technology Transfer (02 2020 ). https:\/\/doi.org\/10.1007\/s10009-020-00552--5 10.1007\/s10009-020-00552--5 Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. 2020. Efficient monitoring of hyperproperties using prefix trees. International Journal on Software Tools for Technology Transfer (02 2020). https:\/\/doi.org\/10.1007\/s10009-020-00552--5"},{"volume-title":"Runtime Verification","author":"Hahn Christopher","key":"e_1_3_2_2_15_1","unstructured":"Christopher Hahn . 2019. Algorithms for Monitoring Hyperproperties . In Runtime Verification , , Bernd Finkbeiner and Leonardo Mariani (Eds.). Springer International Publishing , Cham, 70--90. Christopher Hahn. 2019. Algorithms for Monitoring Hyperproperties. In Runtime Verification, , Bernd Finkbeiner and Leonardo Mariani (Eds.). Springer International Publishing, Cham, 70--90."},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1vs Vojnar and Lijun Zhang (Eds.)","author":"Hahn Christopher","key":"e_1_3_2_2_16_1","unstructured":"Christopher Hahn , Marvin Stenger , and Leander Tentrup . 2019. Constraint-Based Monitoring of Hyperproperties . In Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1vs Vojnar and Lijun Zhang (Eds.) . Springer International Publishing , Cham , 115--131. Christopher Hahn, Marvin Stenger, and Leander Tentrup. 2019. Constraint-Based Monitoring of Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1vs Vojnar and Lijun Zhang (Eds.). Springer International Publishing, Cham, 115--131."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795075"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1515\/JMC.2007.004"},{"key":"e_1_3_2_2_21_1","volume-title":"Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI) (LNCS)","author":"M\u00fcller P.","year":"2016","unstructured":"P. M\u00fcller , M. Schwerhoff , and A. J. Summers . 2016 . Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI) (LNCS) ,, B. Jobstmann and K. R. M. Leino (Eds.), Vol. 9583 . Springer-Verlag , 41--62. P. M\u00fcller, M. Schwerhoff, and A. J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI) (LNCS),, B. Jobstmann and K. R. M. Leino (Eds.), Vol. 9583. Springer-Verlag, 41--62."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_3_2_2_23_1","volume-title":"RFC 8446: The Transport Layer Security (TLS) Protocol Version 1.3. https:\/\/tools.ietf.org\/html\/rfc8446 (Accessed May 29th","author":"Rescorla E.","year":"2020","unstructured":"E. Rescorla . 2018. RFC 8446: The Transport Layer Security (TLS) Protocol Version 1.3. https:\/\/tools.ietf.org\/html\/rfc8446 (Accessed May 29th , 2020 ). E. Rescorla. 2018. RFC 8446: The Transport Layer Security (TLS) Protocol Version 1.3. https:\/\/tools.ietf.org\/html\/rfc8446 (Accessed May 29th, 2020)."},{"volume-title":"Verification of Quantitative Hyperproperties Using Trace Enumeration Relations","author":"Sahai Shubham","key":"e_1_3_2_2_24_1","unstructured":"Shubham Sahai , Pramod Subramanyan , and Rohit Sinha . 2020. Verification of Quantitative Hyperproperties Using Trace Enumeration Relations . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing , Cham , 201--224. Shubham Sahai, Pramod Subramanyan, and Rohit Sinha. 2020. Verification of Quantitative Hyperproperties Using Trace Enumeration Relations. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 201--224."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-16814"},{"key":"e_1_3_2_2_26_1","volume-title":"The Signal Protocol. https:\/\/signal.org\/ (Accessed May 29th","author":"Perrin M. Marlinspike T.","year":"2020","unstructured":"M. Marlinspike T. Perrin . 2016. The Signal Protocol. https:\/\/signal.org\/ (Accessed May 29th , 2020 ). M. Marlinspike T. Perrin. 2016. The Signal Protocol. https:\/\/signal.org\/ (Accessed May 29th, 2020)."},{"volume-title":"Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy. 178--194","author":"Woo T. Y. C.","key":"e_1_3_2_2_27_1","unstructured":"T. Y. C. Woo and S. S. Lam . 1993. A semantic model for authentication protocols . In Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy. 178--194 . T. Y. C. Woo and S. S. Lam. 1993. A semantic model for authentication protocols. In Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy. 178--194."}],"event":{"name":"CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Virtual Event USA","acronym":"CCS '20"},"container-title":["Proceedings of the 15th Workshop on Programming Languages and Analysis for Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3411506.3417596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3411506.3417596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:37Z","timestamp":1750197757000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3411506.3417596"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,9]]},"references-count":27,"alternative-id":["10.1145\/3411506.3417596","10.1145\/3411506"],"URL":"https:\/\/doi.org\/10.1145\/3411506.3417596","relation":{},"subject":[],"published":{"date-parts":[[2020,11,9]]},"assertion":[{"value":"2020-11-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}