{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:54Z","timestamp":1780994694617,"version":"3.54.1"},"reference-count":69,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,5]]},"DOI":"10.1109\/sp46215.2023.10179477","type":"proceedings-article","created":{"date-parts":[[2023,7,21]],"date-time":"2023-07-21T17:18:15Z","timestamp":1689959895000},"page":"1130-1147","source":"Crossref","is-referenced-by-count":9,"title":["Owl: Compositional Verification of Security Protocols via an Information-Flow Type System"],"prefix":"10.1109","author":[{"given":"Joshua","family":"Gancher","sequence":"first","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sydney","family":"Gibson","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pratap","family":"Singh","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samvid","family":"Dharanikota","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.5"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.15"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.42"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.028"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00078"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_11"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45682-1_33"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/996943.996945"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44448-3_41"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.39"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"ref20","article-title":"Implementing and proving the TLS 1.3 record layer","volume-title":"Proceedings of the IEEE S&P","author":"Bhargavan"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44381-1_14"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1561\/9781680832075"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00009"},{"key":"ref27","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-63697-9_22","article-title":"Prf-odh: Relations, instantiations, and impossibility results","volume-title":"Cryptology ePrint Archive","author":"Brendel","year":"2017"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.13"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/74851.74852"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44647-8_2"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00019"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.27"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9187-9"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.35"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00039"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/358722.358740"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1976.1055638"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28632-5_26"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046747"},{"key":"ref44","volume-title":"Owl code repository","author":"Gancher"},{"key":"ref45","doi-asserted-by":"crossref","DOI":"10.1109\/SP46215.2023.10179477","article-title":"Owl: Compositional verification of security protocols via an information-flow type system","volume-title":"Cryptology ePrint Archive","author":"Gancher","year":"2023"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-171070"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/1609956.1609963"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-005-0432-z"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.17487\/rfc1510"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44647-8_19"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328479"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2019.00026"},{"key":"ref57","article-title":"A tutorial introduction to CryptHOL","volume-title":"Cryptology ePrint Archive, Report 2018\/941","author":"Lochbihler"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30556-9_27"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/1030083.1030112"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25385-0_20"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"ref65","volume-title":"The joy of cryptography","author":"Rosulek"},{"key":"ref66","year":"2022","journal-title":"The Rust programming language"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.17487\/rfc4253"}],"event":{"name":"2023 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2023,5,21]]},"end":{"date-parts":[[2023,5,25]]}},"container-title":["2023 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10179215\/10179280\/10179477.pdf?arnumber=10179477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T05:13:58Z","timestamp":1721452438000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10179477\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5]]},"references-count":69,"URL":"https:\/\/doi.org\/10.1109\/sp46215.2023.10179477","relation":{},"subject":[],"published":{"date-parts":[[2023,5]]}}}