### SOTA Signal verif Efforts led by [Karthikeyan Bhargavan](https://dblp.org/pid/80/3503.html): - [Signal post quantum key agreement verified in proverif/cryptoverif](https://www.usenix.org/conference/usenixsecurity24/presentation/bhargavan). The corresponding paper is [Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging](https://inria.hal.science/hal-04604518/document). - [Signal*](https://github.com/Inria-Prosecco/libsignal-protocol-wasm-fstar) was for the javascript implementation of `libsignal/protocol`; to be seen at what extent it can be reused for the rust implementation - [DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code](https://github.com/REPROSEC/dolev-yao-star) [Proverif](https://bblanche.gitlabpages.inria.fr/proverif) is symbolic while [Cryptoverif](https://bblanche.gitlabpages.inria.fr/cryptoverif) is computational. Other efforts come from [Cas Cremers](https://dblp.org/pid/17/2282.html), who worked on [Tamarin](https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples): - [Secure Messaging with Strong Compromise Resilience, Temporal Privacy, and Immediate Decryption](https://eprint.iacr.org/2022/1481.pdf) - [A Formal Security Analysis of the Signal Messaging Protocol](https://eprint.iacr.org/2016/1013.pdf) - [Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations](https://eprint.iacr.org/2022/1710.pdf) ### Misc - [Cryspen blogpost on pqxdh, '23](https://cryspen.com/post/pqxdh/) - [Signal's spec for PQXDH, authored by the above R. Schmidt](https://signal.org/docs/specifications/pqxdh) - [SOTA from Claude](https://hackmd.io/@0JyvKcitS628xqX2ApesTA/SyvNb-661l)