Date of Award

Summer 7-15-2022

Document Type


Degree Name

Master of Arts (MA)


Computer Science

First Advisor

Subash Shankar

Second Advisor

Sven Dietrich

Academic Program Adviser

Subash Shankar


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.



To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.