Date of Award
Summer 7-15-2022
Document Type
Thesis
Degree Name
Master of Arts (MA)
Department
Computer Science
First Advisor
Subash Shankar
Second Advisor
Sven Dietrich
Academic Program Adviser
Subash Shankar
Abstract
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.
Recommended Citation
Washburn, Alexander J., "Formal Verification Applications for the TreeKEM Continuous Group Key Agreement Protocol" (2022). CUNY Academic Works.
https://academicworks.cuny.edu/hc_sas_etds/931