---
# System prepended metadata

title: SOTA_signal_verif

---

### 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)

