Secure Messaging

Formal verification of cryptographic primitives and protocols for secure messaging in Lean

Blueprint Status and Progress

Total 125Specified 64Verified 64Data timeframe: 7 May - 19 Oct

Chapter	Definitions				Theorems
Chapter	Total	Specified	Verified	Ready next	Total	Specified	Verified	Ready next
ALL	65	44	44	9	60	20	20	10
Authenticated Encryption with Associated Data	5	5	5	0	4	4	4	0
Continuous Key Agreement	6	6	6	0	6	4	4	2
Erasure Codes	5	5	5	0	1	1	1	0
Forward-Secure Authenticated Encryption with Associated Data	3	0	0	1	2	0	0	0
Key Encapsulation Mechanism	8	8	8	0	6	3	3	3
Pseudorandom Function and Generator	4	1	1	1	1	0	0	0
Ratcheting Key Encapsulation Mechanism	9	6	6	3	14	5	5	0
Sparse Continuous Key Agreement	14	13	13	1	10	3	3	5
Secure Messaging	11	0	0	3	16	0	0	0

The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal ProtocolJoel Alwen, Sandro Coretti, Yevgeniy DodisEUROCRYPT 2019
Triple Ratchet: A Bandwidth-Efficient Hybrid-Secure Signal ProtocolYevgeniy Dodis, Daniel Jost, Shuichi Katsumata, Thomas Prest, Rolfe SchmidtEUROCRYPT 2025
How to Compare Bandwidth-Constrained Two-Party Secure Messaging Protocols: A Quest for a More Efficient and Secure Post-Quantum ProtocolBenedikt Auerbach, Yevgeniy Dodis, Daniel Jost, Shuichi Katsumata, Rolfe SchmidtUSENIX Security 2025
VCV-ioFormalized Cryptography Proofs in Lean 4GitHub Repository
secure-messaging (project source)Lean/VCVio specifications and proofs for secure messaging protocolsGitHub Repository