Date of Award
Master of Arts (MA)
Academic Program Adviser
The features of Secure Group Messaging, the security guarantees of Message Layer Security, and the TreeKEM protocol designed to satisfy these guarantees and features are explored. A motivation and methodology for verification via explicit model checking is presented. Subsequently, a translation of the TreeKEM protocol into a Promela reference model is described, examining the nuances explicit model checking brings. Finally the results of the formal verification methods are discussed.
Washburn, Alexander J., "Formal Verification Applications for the TreeKEM Continuous Group Key Agreement Protocol" (2022). CUNY Academic Works.