Approved for public release; distribution is unlimited. / This thesis presents a formal analysis process and the results of applying that process to the MLS LAN: TCB-to- TCBE, Session Status, and TCBE-to-Session Server Protocols. The formal analysis process consists of several distinct stages: the creation of a detailed informal protocol description, analyzing that description to reveal assumptions and areas of interest not directly addressed in the protocol description, the transformation of that description and the related assumptions into a formal Strand Space representation, analyzing that representation to reveal assumptions and areas of interest, and concluding with an application of John Millen's automated Constraint Checker analysis tool to the Strand Space representations under an extremely limited set of conditions to prove certain protocol secrecy properties.
| Identifer | oai:union.ndltd.org:nps.edu/oai:calhoun.nps.edu:10945/1448 |
| Date | 09 1900 |
| Creators | Craven, Daniel Shawn |
| Contributors | Dinolt, George W., Pinsky, Sylvan S., Naval Postgraduate School (U.S.)., Information Sciences |
| Publisher | Monterey, California. Naval Postgraduate School |
| Source Sets | Naval Postgraduate School |
| Detected Language | English |
| Type | Thesis |
| Format | xvi, 137 p. ;, application/pdf |
| Rights | This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States. |
Page generated in 0.0025 seconds