SecureMessaging

Formal verification of protocols for secure messaging in Lean 4, built on top of VCVio. Currently targeting cryptographic primitives and protocols from:

• Alwen, Coretti, Dodis. The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal Protocol. EUROCRYPT 2019, https://eprint.iacr.org/2018/1037.pdf

• Dodis, Jost, Katsumata, Prest, Schmidt. Triple Ratchet: A Bandwidth Efficient Hybrid-Secure Signal Protocol. EUROCRYPT 2025, https://eprint.iacr.org/2025/078.pdf

• Auerbach, Dodis, Jost, Katsumata, Schmidt. How to Compare Bandwidth Constrained Two-Party Secure Messaging Protocols: A Quest for A More Efficient and Secure Post-Quantum Protocol. USENIX Security 2025, https://eprint.iacr.org/2025/2267.pdf

License

Apache-2.0.