Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM

• Alex J. Washburn Hunter College
• Subash Shankar Hunter College

Resumo

The TreeKEM protocol is the preeminent implementation candidate for the Message Layer Security standard. Prior work analyzed TreeKEM by defining the Continuous Group Key Agreement security game, which facilitated proof of some security guarantees and also identified protocol deficiencies which were subsequently remedied. This work extends such applications by formalizing the Continuous Group Key Agreement security game through multiple soundness preserving abstractions. The model is parameterized by N, representing an unbounded protocol duration among N distinct participants. Once formalized, the game is encoded within Promela and essential security guarantees are verified for N ≤ 16 via the model checker Spin. This represents a notable achievement, both in practical security terms for the TreeKEM protocol, as well as demonstrating scalability techniques for non-trivial parameter bounds when modeling a complex, concurrent protocol.