A Formal Analysis of the MLS LAN: TCB-to-TCBE, Session Status, and TCBE-to-Session Server Protocols

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2004
Accession Number
ADA427307

Entities

People

  • Daniel S. Craven

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Application Protocols
  • Authentication
  • Communications Protocols
  • Computer Communications
  • Computer Networks
  • Computer Science
  • Computers
  • Cryptography
  • Cybersecurity
  • Formal Languages
  • Local Area Networks
  • Materials
  • Network Science
  • Notation
  • Numbering Systems
  • Operating Systems
  • Security Protocols

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computer Networking
  • Systems Analysis and Design

Technology Areas

  • Space