{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T15:41:31Z","timestamp":1783438891113,"version":"3.54.6"},"reference-count":39,"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"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,5]]},"DOI":"10.1109\/sp46215.2023.10179325","type":"proceedings-article","created":{"date-parts":[[2023,7,21]],"date-time":"2023-07-21T17:18:15Z","timestamp":1689959895000},"page":"1077-1093","source":"Crossref","is-referenced-by-count":10,"title":["Sound Verification of Security Protocols: From Design to Interoperable Implementations"],"prefix":"10.1109","author":[{"given":"Linard","family":"Arquint","sequence":"first","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felix A.","family":"Wolf","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Lallemand","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA,France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Sasse","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sven N.","family":"Wiesner","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH,Department of Computer Science,Zurich,Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2012.25"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/csfw.2001.930138"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/sp.2017.26"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/sp40001.2021.00037"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30303-1_10"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25527-9_7"},{"issue":"2","key":"ref9","first-page":"279","article-title":"Formally sound implementations of security protocols with JavaSPI","volume-title":"Formal Asp. Comput.","volume":"30","author":"Sisto","year":"2018"},{"issue":"1","key":"ref10","first-page":"5:1","article-title":"Verified interoperable implementations of security protocols","volume-title":"ACM Trans. Program. Lang. Syst.","volume":"31","author":"Bhargavan","year":"2008"},{"key":"ref11","first-page":"523","article-title":"DY*: A modular symbolic verification framework for executable cryptographic protocol code","volume-title":"IEEE European Symposium on Security and Privacy, EuroS&P 2021","author":"Bhargavan"},{"key":"ref12","first-page":"63","article-title":"Proved generation of implementations from computationally secure protocol specifications","volume-title":"Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013","volume":"7796","author":"Cad\u00e9"},{"key":"ref13","first-page":"463","article-title":"Implementing and proving the TLS 1.3 record layer","volume-title":"2017 IEEE Symposium on Security and Privacy, SP 2017","author":"Delignat-Lavaud"},{"key":"ref14","first-page":"1162","article-title":"A security model and fully verified implementation for the IETF QUIC record layer","volume-title":"42nd IEEE Symposium on Security and Privacy, SP 2021","author":"Delignat-Lavaud"},{"key":"ref15","first-page":"55","article-title":"Separation Logic: A logic for shared mutable data structures","volume-title":"17th IEEE Symposium on Logic in Computer Science (LICS 2002)","author":"Reynolds"},{"key":"ref16","first-page":"367","article-title":"Gobra: Modular specification and verification of Go programs","volume-title":"Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event","volume":"12759","author":"Wolf"},{"key":"ref17","first-page":"41","article-title":"VeriFast: A powerful, sound, predictable, fast verifier for C and Java","volume-title":"NASA Formal Methods - Third International Symposium, NFM 2011","volume":"6617","author":"Jacobs"},{"key":"ref18","first-page":"596","article-title":"Nagini: A static verifier for Python","volume-title":"Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018","volume":"10981","author":"Eilers"},{"issue":"OOPSLA","key":"ref19","first-page":"152:1","article-title":"Igloo: Soundly linking compositional refinement and separation logic for distributed system verification","volume-title":"Proc. ACM Program. Lang","volume":"4","author":"Sprenger"},{"key":"ref20","article-title":"Sound verification of security protocols: From design to interoperable implementations (extended version)","author":"Arquint","year":"2022"},{"key":"ref21","article-title":"Sound verification of security protocols: From design to interoperable implementations","author":"Arquint","year":"2022"},{"key":"ref22","doi-asserted-by":"crossref","DOI":"10.14722\/ndss.2019.23394","article-title":"Component-based formal analysis of 5G-AKA: Channel assumptions and session confusion","volume-title":"26th Annual Network and Distributed System Security Symposium, NDSS 2019","author":"Cremers"},{"key":"ref23","first-page":"1773","article-title":"A comprehensive symbolic analysis of TLS 1.3","volume-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017","author":"Cremers"},{"key":"ref24","article-title":"A spectral analysis of Noise: A comprehensive, automated, formal analysis of Diffie-Hellman protocols","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Girol"},{"key":"ref25","article-title":"Card brand mixup attack: Bypassing the PIN in non-Visa cards by using them for Visa transactions","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Basin"},{"issue":"2","key":"ref26","first-page":"198","article-title":"On the security of public key protocols","volume-title":"IEEE Trans. Information Theory","volume":"29","author":"Dolev","year":"1983"},{"key":"ref27","first-page":"31","article-title":"A hierarchy of authentication specification","volume-title":"10th Computer Security Foundations Workshop (CSFW \u201997)","author":"Lowe"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_7"},{"key":"ref29","first-page":"259","article-title":"A sound abstraction of the parsing problem","volume-title":"IEEE 27th Computer Security Foundations Symposium, CSF 2014","author":"M\u00f6dersheim"},{"key":"ref30","first-page":"1465","article-title":"EverParse: Verified secure zero-copy parsers for authenticated message formats","volume-title":"28th USENIX Security Symposium, USENIX Security 2019","author":"Ramananandro"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2011.8"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.3233\/jcs-140508"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_4"},{"key":"ref34","article-title":"Verifying cryptographic protocol implementations that use industrial cryptographic APIs","volume-title":"Tech. Rep.","author":"Vanspauwen","year":"2017"},{"key":"ref35","article-title":"Go implementation of WireGuard","author":"Donenfeld"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2133375.2133378"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2008.27"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813662"}],"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\/10179325.pdf?arnumber=10179325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T05:19:07Z","timestamp":1721452747000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10179325\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/sp46215.2023.10179325","relation":{},"subject":[],"published":{"date-parts":[[2023,5]]}}}