Combining Theory Generation and Model Checking for Security Protocol Analysis,

Abstract

This paper reviews two relatively new tools for automated formal analysis of security protocols. One applies the formal methods technique of model checking to the task of protocol analysis, while the other utilizes the method of theory generation. which borrows from both model checking and automated theorem proving. For purposes of comparison. the tools are both applied to a suite of sampIe protocols with known laws. including the protocol used in an earlier study to provide a baseline. We then suggest a heuristic for combining the two approaches to provide a more complete analysis than either approach can provide alone.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2000
Accession Number
ADA374554

Entities

People

  • Jeannette Wing
  • Nicholas J. Hopper
  • Sanjit A. Seshia

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Authentication
  • Communication Channels
  • Computer Science
  • Concrete
  • Construction
  • Cryptography
  • Demographic Cohorts
  • Electronic Commerce
  • Explosives Initiators
  • Notation
  • Push Buttons
  • Robotics
  • Security
  • Security Protocols
  • Specifications

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Computational Modeling and Simulation