Completeness of CPSA

Abstract

The Cryptographic Protocol Shapes Analyzer (cpsa) is a program for automatically characterizing the possible executions of a protocol compatible with a specified partial execution. This paper presents a mathematically rigorous theory that backs up the implementation of cpsa in Haskell, and proves the algorithm produces characterizations that are complete, and that the algorithm enumerates these characterizations.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2011
Accession Number
ADA562264

Entities

People

  • F. J. Thayer
  • Moses D. Liskov
  • Paul D. Rowe

Organizations

  • MITRE Corporation

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Analyzers
  • Boundaries
  • Composite Structures
  • Compression
  • Computer Science
  • Coverings
  • Cryptography
  • Equations
  • Guarantees
  • Identities
  • Language
  • Notation
  • Security
  • Security Protocols
  • Specifications

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Computational Linguistics
  • Computer Networking