{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T23:21:37Z","timestamp":1777936897712,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:00:00Z","timestamp":1700006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Werner Siemens-Stiftung (WSS)"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,15]]},"DOI":"10.1145\/3576915.3623105","type":"proceedings-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T12:35:13Z","timestamp":1700570113000},"page":"1377-1391","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Generic Methodology for the Modular Verification of Security Protocol Implementations"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6230-8014","authenticated-orcid":false,"given":"Linard","family":"Arquint","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2569-9121","authenticated-orcid":false,"given":"Malte","family":"Schwerhoff","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2357-3023","authenticated-orcid":false,"given":"Vaibhav","family":"Mehta","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Next generation kernel network tunnel,\" in NDSS","author":"Donenfeld J. A.","year":"2017","unstructured":"J. A. Donenfeld, \"WireGuard: Next generation kernel network tunnel,\" in NDSS. The Internet Society, 2017."},{"key":"e_1_3_2_1_2_1","unstructured":"M. Marlinspike and T. Perrin. The X3DH key agreement protocol (revision 1). Available: https:\/\/www.signal.org\/docs\/specifications\/x3dh\/"},{"key":"e_1_3_2_1_3_1","first-page":"147","volume-title":"ser. LNCS","author":"Lowe G.","year":"1996","unstructured":"G. Lowe, \"Breaking and fixing the Needham-Schroeder public-key protocol using FDR,\" in TACAS, ser. LNCS, vol. 1055. Springer, 1996, pp. 147--166."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_3_2_1_5_1","unstructured":"CVE \"CVE-2014-0160 \" 2013. [Online]. Available: https:\/\/www.cve.org\/ CVERecord?id=CVE-2014-0160"},{"key":"e_1_3_2_1_6_1","unstructured":"-- \"CVE-2021-40823 \" 2021. [Online]. Available: https:\/\/www.cve.org\/ CVERecord?id=CVE-2021--40823"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/AINA.2004.1283943"},{"key":"e_1_3_2_1_8_1","first-page":"65","volume-title":"IEEE Computer Society","author":"Cad\u00e9 D.","year":"2012","unstructured":"D. Cad\u00e9 and B. Blanchet, \"From computationally-proved protocol specifications to implementations,\" in ARES. IEEE Computer Society, 2012, pp. 65--74."},{"key":"e_1_3_2_1_9_1","first-page":"523","article-title":"DY*: A modular symbolic verification framework for executable cryptographic protocol code","author":"Bhargavan K.","year":"2021","unstructured":"K. Bhargavan, A. Bichhawat, Q. H. Do, P. Hosseyni, R. K\u00fcsters, G. Schmitz, and T. W\u00fcrtele, \"DY*: A modular symbolic verification framework for executable cryptographic protocol code,\" in EuroS&P. IEEE, 2021, pp. 523--542.","journal-title":"EuroS&P. IEEE"},{"key":"e_1_3_2_1_10_1","first-page":"2601","volume-title":"ACM","author":"Bhargavan K.","year":"2021","unstructured":"--, \"An in-depth symbolic security analysis of the ACME standard,\" in CCS. ACM, 2021, pp. 2601--2617."},{"key":"e_1_3_2_1_11_1","first-page":"107","article-title":"Noise*: A library of verified high-performance secure channel protocol implementations","author":"Ho S.","year":"2022","unstructured":"S. Ho, J. Protzenko, A. Bichhawat, and K. Bhargavan, \"Noise*: A library of verified high-performance secure channel protocol implementations,\" in S&P. IEEE, 2022, pp. 107--124.","journal-title":"S&P. IEEE"},{"key":"e_1_3_2_1_12_1","first-page":"256","volume-title":"ACM","author":"Swamy N.","year":"2016","unstructured":"N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P. Strub, M. Kohlweiss, J. K. Zinzindohoue, and S. Z. B\u00e9guelin, \"Dependent types and multi-monadic effects in F*,\" in POPL. ACM, 2016, pp. 256--270."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_3_2_1_14_1","first-page":"2008","article-title":"Using Elyjah to analyse Java implementations of cryptographic protocols","author":"O'Shea N.","year":"2008","unstructured":"N. O'Shea, \"Using Elyjah to analyse Java implementations of cryptographic protocols,\" in FCS-ARSPA-WITS-2008, 2008.","journal-title":"FCS-ARSPA-WITS-"},{"key":"e_1_3_2_1_15_1","first-page":"712","volume-title":"ACM","author":"Aizatulin M.","year":"2012","unstructured":"M. Aizatulin, A. D. Gordon, and J. J\u00fcrjens, \"Computational verification of C protocol implementations by symbolic execution,\" in CCS. ACM, 2012, pp. 712--723."},{"key":"e_1_3_2_1_16_1","first-page":"435","article-title":"Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach","author":"Kobeissi N.","year":"2017","unstructured":"N. Kobeissi, K. Bhargavan, and B. Blanchet, \"Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach,\" in EuroS&P. IEEE, 2017, pp. 435--450.","journal-title":"EuroS&P. IEEE"},{"key":"e_1_3_2_1_17_1","first-page":"483","volume-title":"IEEE Computer Society","author":"Bhargavan K.","year":"2017","unstructured":"K. Bhargavan, B. Blanchet, and N. Kobeissi, \"Verified models and reference imple-mentations for the TLS 1.3 standard candidate,\" in S&P. IEEE Computer Society, 2017, pp. 483--502."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0449-8"},{"key":"e_1_3_2_1_19_1","first-page":"1256","article-title":"Formally verified cryptographic web applications in WebAssembly","author":"Protzenko J.","year":"2019","unstructured":"J. Protzenko, B. Beurdouche, D. Merigoux, and K. Bhargavan, \"Formally verified cryptographic web applications in WebAssembly,\" in S&P. IEEE, 2019, pp. 1256--1274.","journal-title":"S&P. IEEE"},{"key":"e_1_3_2_1_20_1","first-page":"1077","article-title":"Sound verification of security protocols: From design to interoperable implementations","author":"Arquint L.","year":"2023","unstructured":"L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. A. Basin, and P. M\u00fcller, \"Sound verification of security protocols: From design to interoperable implementations,\" in SP. IEEE, 2023, pp. 1077--1093.","journal-title":"SP. IEEE"},{"key":"e_1_3_2_1_21_1","first-page":"41","volume-title":"VeriFast: A powerful, sound, predictable, fast verifier for C and Java,\" in NASA Formal Methods, ser. LNCS","author":"Jacobs B.","year":"2011","unstructured":"B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens, \"VeriFast: A powerful, sound, predictable, fast verifier for C and Java,\" in NASA Formal Methods, ser. LNCS, vol. 6617. Springer, 2011, pp. 41--55."},{"key":"e_1_3_2_1_22_1","first-page":"367","volume-title":"Gobra: Modular specification and verification of Go programs,\" in CAV, ser. LNCS","author":"Wolf F. A.","year":"2021","unstructured":"F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira, and P. M\u00fcller, \"Gobra: Modular specification and verification of Go programs,\" in CAV, ser. LNCS, vol. 12759. Springer, 2021, pp. 367--379."},{"key":"e_1_3_2_1_23_1","first-page":"127","volume-title":"The VerCors tool for verification of concurrent programs,\" in FM, ser. LNCS","author":"Blom S.","year":"2014","unstructured":"S. Blom and M. Huisman, \"The VerCors tool for verification of concurrent programs,\" in FM, ser. LNCS, vol. 8442. Springer, 2014, pp. 127--131."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158138"},{"key":"e_1_3_2_1_25_1","first-page":"1","volume-title":"Leveraging Rust types for modular specification and verification,\" Proc. ACM Program. Lang","author":"Astrauskas V.","year":"2019","unstructured":"V. Astrauskas, P. M\u00fcller, F. Poli, and A. J. Summers, \"Leveraging Rust types for modular specification and verification,\" Proc. ACM Program. Lang., vol. 3, no. OOPSLA, pp. 147:1--147:30, 2019."},{"key":"e_1_3_2_1_26_1","first-page":"1","volume-title":"Local reasoning about programs that alter data structures,\" in CSL, ser. LNCS","author":"O'Hearn P. W.","year":"2001","unstructured":"P. W. O'Hearn, J. C. Reynolds, and H. Yang, \"Local reasoning about programs that alter data structures,\" in CSL, ser. LNCS, vol. 2142. Springer, 2001, pp. 1--19."},{"key":"e_1_3_2_1_27_1","first-page":"55","volume-title":"IEEE Computer Society","author":"Reynolds J. C.","year":"2002","unstructured":"J. C. Reynolds, \"Separation Logic: A logic for shared mutable data structures,\" in LICS. IEEE Computer Society, 2002, pp. 55--74."},{"key":"e_1_3_2_1_28_1","first-page":"1","volume-title":"The spirit of ghost code,\" in CAV, ser. LNCS","author":"Filli\u00e2tre J.","year":"2014","unstructured":"J. Filli\u00e2tre, L. Gondelman, and A. Paskevich, \"The spirit of ghost code,\" in CAV, ser. LNCS, vol. 8559. Springer, 2014, pp. 1--16."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1976.1055638"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8330913"},{"key":"e_1_3_2_1_32_1","first-page":"3","volume-title":"IEEE Computer Society","author":"Dupressoir F.","year":"2011","unstructured":"F. Dupressoir, A. D. Gordon, J. J\u00fcrjens, and D. A. Naumann, \"Guiding a general-purpose C verifier to prove cryptographic protocols,\" in CSF. IEEE Computer Society, 2011, pp. 3--17."},{"key":"e_1_3_2_1_33_1","first-page":"23","volume-title":"VCC: A practical system for verifying concurrent C,\" in TPHOLs, ser. LNCS","author":"Cohen E.","year":"2009","unstructured":"E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies, \"VCC: A practical system for verifying concurrent C,\" in TPHOLs, ser. LNCS, vol. 5674. Springer, 2009, pp. 23--42."},{"key":"e_1_3_2_1_34_1","first-page":"1","volume-title":"Igloo: soundly linking compositional refinement and separation logic for distributed system verification,\" Proc. ACM Program. Lang","author":"Sprenger C.","year":"2020","unstructured":"C. Sprenger, T. Klenze, M. Eilers, F. A. Wolf, P. M\u00fcller, M. Clochard, and D. A. Basin, \"Igloo: soundly linking compositional refinement and separation logic for distributed system verification,\" Proc. ACM Program. Lang., vol. 4, no. OOPSLA, pp. 152:1--152:31, 2020."},{"key":"e_1_3_2_1_35_1","first-page":"55","volume-title":"ser. LNCS","author":"Boyland J.","year":"2003","unstructured":"J. Boyland, \"Checking interference with fractional permissions,\" in SAS, ser. LNCS, vol. 2694. Springer, 2003, pp. 55--72."},{"key":"e_1_3_2_1_36_1","first-page":"31","volume-title":"IEEE Computer Society","author":"Lowe G.","year":"1997","unstructured":"G. Lowe, \"A hierarchy of authentication specification,\" in CSFW. IEEE Computer Society, 1997, pp. 31--44."},{"key":"e_1_3_2_1_37_1","first-page":"445","volume-title":"ACM","author":"Bhargavan K.","year":"2010","unstructured":"K. Bhargavan, C. Fournet, and A. D. Gordon, \"Modular verification of security protocol code by typing,\" in POPL. ACM, 2010, pp. 445--456."},{"key":"e_1_3_2_1_38_1","first-page":"247","volume-title":"ACM","author":"Parkinson M. J.","year":"2005","unstructured":"M. J. Parkinson and G. M. Bierman, \"Separation Logic and abstraction,\" in POPL. ACM, 2005, pp. 247--258."},{"key":"e_1_3_2_1_39_1","first-page":"3","volume-title":"A cryptographic analysis of the WireGuard protocol,\" in ACNS, ser. LNCS","author":"Dowling B.","year":"2018","unstructured":"B. Dowling and K. G. Paterson, \"A cryptographic analysis of the WireGuard protocol,\" in ACNS, ser. LNCS, vol. 10892. Springer, 2018, pp. 3--21."},{"key":"e_1_3_2_1_40_1","first-page":"231","article-title":"A mechanised cryptographic proof of the Wire Guard virtual private network protocol","author":"Lipp B.","year":"2019","unstructured":"B. Lipp, B. Blanchet, and K. Bhargavan, \"A mechanised cryptographic proof of the Wire Guard virtual private network protocol,\" in Euro S&P. IEEE, 2019, pp. 231--246.","journal-title":"Euro S&P. IEEE"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7409524"},{"key":"e_1_3_2_1_42_1","first-page":"1857","volume-title":"A spectral analysis of Noise: A comprehensive, automated, formal analysis of Diffie-Hellman protocols,\" in USENIX Security Symposium","author":"Girol G.","year":"2020","unstructured":"G. Girol, L. Hirschi, R. Sasse, D. Jackson, C. Cremers, and D. A. Basin, \"A spectral analysis of Noise: A comprehensive, automated, formal analysis of Diffie-Hellman protocols,\" in USENIX Security Symposium. USENIX Association, 2020, pp. 1857--1874."},{"key":"e_1_3_2_1_43_1","first-page":"1773","volume-title":"ACM","author":"Cremers C.","year":"2017","unstructured":"C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe, \"A compre-hensive symbolic analysis of TLS 1.3,\" in CCS. ACM, 2017, pp. 1773--1788."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.25"},{"issue":"1","key":"e_1_3_2_1_45_1","first-page":"4","article-title":"Vst-floyd: A separation logic tool to verify correctness of C programs","volume":"61","author":"Cao Q.","year":"2018","unstructured":"Q. Cao, L. Beringer, S. Gruetter, J. Dodds, and A. W. Appel, \"Vst-floyd: A separation logic tool to verify correctness of C programs,\" J. Autom. Reason., vol. 61, no. 1--4, pp. 367--422, 2018.","journal-title":"J. Autom. Reason."},{"key":"e_1_3_2_1_46_1","first-page":"983","article-title":"EverCrypt: A fast, verified, cross-platform cryptographic provider","author":"Protzenko J.","year":"2020","unstructured":"J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. Delignat-Lavaud, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Z. B\u00e9guelin, \"EverCrypt: A fast, verified, cross-platform cryptographic provider,\" in S&P. IEEE, 2020, pp. 983--1002.","journal-title":"S&P. IEEE"},{"key":"e_1_3_2_1_47_1","volume-title":"A generic methodology for the modular verification of security protocol implementations (extended version)","author":"Arquint L.","year":"2023","unstructured":"L. Arquint, M. Schwerhoff, V. Mehta, and P. M\u00fcller, \"A generic methodology for the modular verification of security protocol implementations (extended version),\" 2023. [Online]. Available: https:\/\/arxiv.org\/abs\/2212.02626"},{"key":"e_1_3_2_1_48_1","first-page":"777","article-title":"SoK: Computer-aided cryptography","author":"Barbosa M.","year":"2021","unstructured":"M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, and B. Parno, \"SoK: Computer-aided cryptography,\" in S&P. IEEE, 2021, pp. 777--795.","journal-title":"S&P. IEEE"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"e_1_3_2_1_50_1","first-page":"3","volume-title":"Symbolic and computational models,\" in POST, ser. LNCS","author":"Blanchet B.","year":"2012","unstructured":"B. Blanchet, \"Security protocol verification: Symbolic and computational models,\" in POST, ser. LNCS, vol. 7215. Springer, 2012, pp. 3--29."},{"key":"e_1_3_2_1_51_1","first-page":"50","volume-title":"Verifying implementations of security protocols by refinement,\" in VSTTE, ser. LNCS","author":"Polikarpova N.","year":"2012","unstructured":"N. Polikarpova and M. Moskal, \"Verifying implementations of security protocols by refinement,\" in VSTTE, ser. LNCS, vol. 7152. Springer, 2012, pp. 50--65."},{"key":"e_1_3_2_1_52_1","first-page":"53","volume-title":"Verifying protocol implementations by augmenting existing cryptographic libraries with specifications,\" in SEFM, ser. LNCS","author":"Vanspauwen G.","year":"2015","unstructured":"G. Vanspauwen and B. Jacobs, \"Verifying protocol implementations by augmenting existing cryptographic libraries with specifications,\" in SEFM, ser. LNCS, vol. 9276. Springer, 2015, pp. 53--68."},{"key":"e_1_3_2_1_53_1","first-page":"78","volume-title":"IEEE Computer Society","author":"Schmidt B.","year":"2012","unstructured":"B. Schmidt, S. Meier, C. Cremers, and D. A. Basin, \"Automated analysis of Diffie- Hellman protocols and advanced security properties,\" in CSF. IEEE Computer Society, 2012, pp. 78--94."},{"key":"e_1_3_2_1_54_1","first-page":"158","volume-title":"Sound, modular and compositional verification of the input\/output behavior of programs,\" in ESOP, ser. LNCS","author":"Penninckx W.","year":"2015","unstructured":"W. Penninckx, B. Jacobs, and F. Piessens, \"Sound, modular and compositional verification of the input\/output behavior of programs,\" in ESOP, ser. LNCS, vol. 9032. Springer, 2015, pp. 158--182."},{"key":"e_1_3_2_1_55_1","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, ser. LNCS","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, ser. LNCS. Springer, 2002, vol. 2283."},{"key":"e_1_3_2_1_56_1","first-page":"17","volume-title":"IEEE Computer Society","author":"Bengtson J.","year":"2008","unstructured":"J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, \"Refinement types for secure implementations,\" in CSF. IEEE Computer Society, 2008, pp. 17--32."},{"key":"e_1_3_2_1_57_1","first-page":"47","volume-title":"Typechecking higher-order security libraries,\" in APLAS, ser. LNCS","author":"Bhargavan K.","year":"2010","unstructured":"K. Bhargavan, C. Fournet, and N. Guts, \"Typechecking higher-order security libraries,\" in APLAS, ser. LNCS, vol. 6461. Springer, 2010, pp. 47--62."},{"key":"e_1_3_2_1_58_1","first-page":"198","volume-title":"IEEE Computer Society","author":"K\u00fcsters R.","year":"2012","unstructured":"R. K\u00fcsters, T. Truderung, and J. Graf, \"A framework for the cryptographic verifi-cation of Java-like programs,\" in CSF. IEEE Computer Society, 2012, pp. 198--212."},{"key":"e_1_3_2_1_59_1","first-page":"363","volume-title":"Cryptographic protocol analysis on real C code,\" in VMCAI, ser. LNCS","author":"Goubault-Larrecq J.","year":"2005","unstructured":"J. Goubault-Larrecq and F. Parrennes, \"Cryptographic protocol analysis on real C code,\" in VMCAI, ser. LNCS, vol. 3385. Springer, 2005, pp. 363--379."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_3_2_1_61_1","first-page":"167","volume-title":"IEEE Computer Society","author":"J\u00fcrjens J.","year":"2006","unstructured":"J. J\u00fcrjens, \"Security analysis of crypto-based Java programs using automated theorem provers,\" in ASE. IEEE Computer Society, 2006, pp. 167--176."},{"key":"e_1_3_2_1_62_1","unstructured":"J. A. Donenfeld and K. Milner. Formal verification of the WireGuard protocol. [Online]. Available: https:\/\/www.wireguard.com\/papers\/wireguard-formal-verification.pdf"},{"key":"e_1_3_2_1_63_1","first-page":"356","article-title":"Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols","author":"Kobeissi N.","year":"2019","unstructured":"N. Kobeissi, G. Nicolas, and K. Bhargavan, \"Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols,\" in EuroS&P. IEEE, 2019, pp. 356--370.","journal-title":"EuroS&P. IEEE"},{"key":"e_1_3_2_1_64_1","first-page":"1130","article-title":"Owl: Compositional verification of security protocols via an information-flow type system","author":"Gancher J.","year":"2023","unstructured":"J. Gancher, S. Gibson, P. Singh, S. Dharanikota, and B. Parno, \"Owl: Compositional verification of security protocols via an information-flow type system,\" in SP. IEEE, 2023, pp. 1130--1147.","journal-title":"SP. IEEE"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"}],"event":{"name":"CCS '23: ACM SIGSAC Conference on Computer and Communications Security","location":"Copenhagen Denmark","acronym":"CCS '23","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T01:43:06Z","timestamp":1755740586000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,15]]},"references-count":67,"alternative-id":["10.1145\/3576915.3623105","10.1145\/3576915"],"URL":"https:\/\/doi.org\/10.1145\/3576915.3623105","relation":{},"subject":[],"published":{"date-parts":[[2023,11,15]]},"assertion":[{"value":"2023-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}