{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T14:15:18Z","timestamp":1730211318639,"version":"3.28.0"},"reference-count":38,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"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":[[2022,8]]},"DOI":"10.1109\/csf54842.2022.9919638","type":"proceedings-article","created":{"date-parts":[[2022,11,4]],"date-time":"2022-11-04T01:29:20Z","timestamp":1667525360000},"page":"412-427","source":"Crossref","is-referenced-by-count":1,"title":["Adversary Safety by Construction in a Language of Cryptographic Protocols"],"prefix":"10.1109","author":[{"given":"Timothy M.","family":"Braje","sequence":"first","affiliation":[{"name":"MIT Lincoln Laboratory,Lexington,MA,USA"}]},{"given":"Alice R.","family":"Lee","sequence":"additional","affiliation":[{"name":"Technische Universität Wien,Vienna,Austria"}]},{"given":"Andrew","family":"Wagner","sequence":"additional","affiliation":[{"name":"Northeastern University,Boston,MA,USA"}]},{"given":"Benjamin","family":"Kaiser","sequence":"additional","affiliation":[{"name":"Princeton University,Princeton,NJ,USA"}]},{"given":"Daniel","family":"Park","sequence":"additional","affiliation":[{"name":"Rensselaer Polytechnic Institute,Troy,NY,USA"}]},{"given":"Martine","family":"Kalke","sequence":"additional","affiliation":[{"name":"MIT Lincoln Laboratory,Lexington,MA,USA"}]},{"given":"Robert K.","family":"Cunningham","sequence":"additional","affiliation":[{"name":"University of Pittsburgh,Pittsburgh,PA,USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL,Cambridge,MA,USA"}]}],"member":"263","reference":[{"key":"ref13","article-title":"Verified Cryptography for Firefox 57","author":"beurdouche","year":"0","journal-title":"The Mozilla Blog"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85174-5_32"},{"key":"ref15","first-page":"71","article-title":"Computer-Aided Security Proofs for the Working Cryptographer","author":"barthe","year":"0","journal-title":"Proceedings of the 31st Annual Cryptology Conference (CRYPTO)"},{"key":"ref37","first-page":"53","article-title":"The Foundational Cryptography Frame-work","author":"petcher","year":"0","journal-title":"Proceedings of the 4th International Conference on Principles of Security and Trust - Volume 9036"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"ref36","first-page":"494","volume":"33","author":"basin","year":"0","journal-title":"CryptHOL Game-Based Proofs in Higher-Order Logic"},{"key":"ref31","first-page":"152","article-title":"Verified Inter-operable Implementations of Security Protocols","author":"bhargavan","year":"0","journal-title":"Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW) Institute of Electrical and Electronics Engineers (IEEE)"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.23"},{"journal-title":"The Transport Layer Security (TLS) Protocol version 1 3 RFC 8446","year":"0","author":"rescorla","key":"ref11"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694385"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3371118","article-title":"A language for prob-abilistically oblivious computation","volume":"4","author":"darais","year":"0","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"ref2","first-page":"526","article-title":"Lucky Thirteen: Breaking the TLS and DTLS Record Protocols","author":"alfardan","year":"0","journal-title":"Proceedings of the 2013 IEEE Symposium on Security & Privacy (S&P) Institute of Electrical and Electronics Engineers (IEEE)"},{"key":"ref1","first-page":"305","article-title":"On the Security of RC4 in TLS","author":"alfardan","year":"0","journal-title":"Proceedings of the 22nd USENIX Security Symposium (SEC)"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"ref16","volume":"29","author":"dolev","year":"0","journal-title":"On the security of public key protocols"},{"key":"ref38","first-page":"207","article-title":"Verified Cor-rectness and Security of OpenSSL HMAC","author":"beringer","year":"0","journal-title":"Proceedings of the 24th USENIX Security Symposium (SEC)"},{"journal-title":"RFC 1991 PGP Message Exchange Formats","year":"0","author":"atkins","key":"ref19"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3473599"},{"key":"ref24","first-page":"406","article-title":"Synthesizing secure proto-cols","author":"cortier","year":"0","journal-title":"Computer Security - ESORICS 2007"},{"journal-title":"Sloc Cloc and Code (sec)","year":"0","author":"boyter","key":"ref23"},{"key":"ref26","first-page":"1","author":"escobar","year":"0","journal-title":"Foundations of Security Analysis and Design V"},{"key":"ref25","first-page":"361","article-title":"Developing security protocols by refine-ment","author":"sprenger","year":"0","journal-title":"7th ACM Conference on Computer and Communications Security (CCS 2010)"},{"key":"ref20","article-title":"DNSCurve: Usable Security for DNS","author":"bernstein","year":"0","journal-title":"DNSCurve Protocol Website"},{"key":"ref22","first-page":"696","article-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"meier","year":"0","journal-title":"Proceedings of the 25th International Conference on Computer Aided Verification (CAV)"},{"key":"ref21","first-page":"1","volume":"1","author":"blanchet","year":"0","journal-title":"Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.27"},{"key":"ref27","first-page":"163","article-title":"Automated Analysis of Security Proto-cols with Global State","author":"kremer","year":"0","journal-title":"Proceedings of the 2014 IEEE Symposium on Security & Privacy (S&P) Institute of Electrical and Electronics Engineers (IEEE)"},{"key":"ref29","first-page":"301","volume":"22","author":"backes","year":"0","journal-title":"Union Intersection and Refine-ment Types and Reasoning About Type Disjointness for Secure Protocol Implementations"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27954-6_11"},{"key":"ref7","first-page":"37","volume":"23","author":"tromer","year":"0","journal-title":"Efficient Cache Attacks on AES and Countermeasures"},{"journal-title":"The Coq Proof Assistant","year":"0","author":"team","key":"ref9"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"ref3","first-page":"689","article-title":"DROWN: Breaking TLS Using SSLv2","author":"aviram","year":"0","journal-title":"Proceedings of the 25th USENIX Security Symposium (SEC)"},{"key":"ref6","first-page":"1","article-title":"Cache Attacks and Counter-measures: The Case of AES","author":"osvik","year":"0","journal-title":"Proceedings of the 2006 Cryptogra-phers' Track at the RSA Conference on Topics in Cryptology (CT-RSA)"},{"journal-title":"Secure Domain Name System (DNS) Deployment Guide","year":"0","author":"chandramouli","key":"ref5"}],"event":{"name":"2022 IEEE 35th Computer Security Foundations Symposium (CSF)","start":{"date-parts":[[2022,8,7]]},"location":"Haifa, Israel","end":{"date-parts":[[2022,8,10]]}},"container-title":["2022 IEEE 35th Computer Security Foundations Symposium (CSF)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9919409\/9919636\/09919638.pdf?arnumber=9919638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:19:30Z","timestamp":1699485570000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9919638\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":38,"URL":"https:\/\/doi.org\/10.1109\/csf54842.2022.9919638","relation":{},"subject":[],"published":{"date-parts":[[2022,8]]}}}