Secure Messaging

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

Blueprint Status and Progress

5 atoms510 atoms1015 atoms1520 atoms2025 atoms2530 atoms3035 atoms3540 atoms4045 atoms4550 atoms5055 atoms5560 atoms6065 atoms6570 atoms7075 atoms7580 atoms8085 atoms8590 atoms9095 atoms95100 atoms100105 atoms105110 atoms110115 atoms115120 atoms120125 atoms125 Specified: 41Verified: 41 May 7May 14May 21May 28Jun 4Jun 11Jun 18Jun 25Jul 2Jul 9Jul 16Jul 23Jul 30Aug 6Aug 13Aug 20Aug 27Sep 3Sep 10Sep 17Sep 24Oct 1Oct 8Oct 15Oct 22Oct 29Nov 5Nov 12Nov 19Nov 26Dec 3Dec 10Dec 17Dec 24Dec 31Jan 7Jan 14Jan 21Jan 28
Total 122Specified 41Verified 41Data timeframe: 7 May - 25 Aug
ChapterDefinitionsTheorems
TotalSpecifiedVerifiedReady nextTotalSpecifiedVerifiedReady next
ALL622929116012123
Authenticated Encryption with Associated Data5550
  • No atoms
4331
Continuous Key Agreement65516440
  • No atoms
Erasure Codes5550
  • No atoms
1110
  • No atoms
Forward-Secure Authenticated Encryption with Associated Data30
  • No atoms
0
  • No atoms
120
  • No atoms
0
  • No atoms
0
  • No atoms
Key Encapsulation Mechanism87716331
Pseudorandom Function and Generator30
  • No atoms
0
  • No atoms
110
  • No atoms
0
  • No atoms
0
  • No atoms
Ratcheting Key Encapsulation Mechanism90
  • No atoms
0
  • No atoms
1140
  • No atoms
0
  • No atoms
0
  • No atoms
Sparse Continuous Key Agreement1277310111
Secure Messaging110
  • No atoms
0
  • No atoms
3160
  • No atoms
0
  • No atoms
0
  • No atoms

References