A formal analysis of the MLS LAN: TCB-to-TCBE, Session Status, and TCBE-to-Session Server Protocols
Loading...
Authors
Craven, Daniel Shawn
Subjects
Advisors
Dinolt, George W.
Date of Issue
2004-09
Date
Publisher
Monterey, CA; Naval Postgraduate School
Language
Abstract
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.
Type
Thesis
Description
Series/Report No
Department
Identifiers
NPS Report Number
Sponsors
Funder
Format
xvi, 137 p. ;
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
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.