{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T00:25:36Z","timestamp":1787012736573,"version":"3.56.0"},"reference-count":24,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"publisher","award":["ANR-22-PECY-0006"],"award-info":[{"award-number":["ANR-22-PECY-0006"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["101224640"],"award-info":[{"award-number":["101224640"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,18]]},"DOI":"10.1109\/sp63933.2026.00120","type":"proceedings-article","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T19:34:20Z","timestamp":1782934460000},"page":"1522-1538","source":"Crossref","is-referenced-by-count":1,"title":["Automated Formal Analysis of Signal's Double Ratchet: Attacks, Fixes and Security Proofs"],"prefix":"10.1109","author":[{"given":"Vincent","family":"Cheval","sequence":"first","affiliation":[{"name":"University of Oxford,United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charlie","family":"Jacomme","sequence":"additional","affiliation":[{"name":"Université de Lorraine, CNRS, Inria, LORIA,France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jessica","family":"Richards","sequence":"additional","affiliation":[{"name":"University of Oxford,United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-020-09360-1"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17653-2_5"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15802-5_27"},{"key":"ref4","first-page":"469","article-title":"Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging","volume-title":"33rd USENIX Security Symposium (USENIX Security 24)","author":"Bhargavan","year":"2024"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"ref7","first-page":"1235","article-title":"Formal analysis of SessionHandling in secure messaging: Lifting security from sessions to conversations","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Cremers","year":"2023"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2012.25"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"ref11","volume-title":"ProVerif models of the Double Ratchet","author":"Cheval","year":"2026"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690360"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15979-4_1"},{"key":"ref14","first-page":"5917","article-title":"How fast do you heal? a taxonomy for post-compromise security in secure-channel establishment","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Blazy","year":"2023"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3719027.3765131"},{"key":"ref16","first-page":"5015","article-title":"A formal analysis of apple\u2019s iMessage PQ3 protocol","volume-title":"34th USENIX Security Symposium (USENIX Security 25)","author":"Linker","year":"2025"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/SP61157.2025.00093"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3708821.3733910"},{"key":"ref19","volume-title":"The Double Ratchet Algorithm.","author":"Perrin","year":"2025"},{"key":"ref20","volume-title":"The PQXDH Key Agreement Protocol","author":"Kret","year":"2023"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00013"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833653"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/csf57540.2023.00032"}],"event":{"name":"2026 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2026,5,18]]},"end":{"date-parts":[[2026,5,21]]}},"container-title":["2026 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11573355\/11573356\/11573624.pdf?arnumber=11573624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T05:48:10Z","timestamp":1782971290000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11573624\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,18]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/sp63933.2026.00120","relation":{},"subject":[],"published":{"date-parts":[[2026,5,18]]}}}