An Analysis of the CAVES Attestation Protocol Using CPSA

Abstract

This paper describes the CAVES attestation protocol and presents a tool-supported analysis showing that the runs of the protocol achieve stated goals. The goals are stated formally by annotating the protocol with logical formulas using the rely-guarantee method. The protocol analysis tool used is the Cryptographic Protocol Shape Analyzer.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2009
Accession Number
AD1108359

Entities

People

  • Brian O'hanlon
  • John D. Ramsdell
  • Jonathan K. Millen
  • Joshua D. Guttman

Organizations

  • MITRE Corporation

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Acceptability
  • Analyzers
  • Authentication
  • Computer Programming
  • Computer Programs
  • Contracts
  • Corporations
  • Cryptography
  • Guarantees
  • Hypervisors
  • Identities
  • Language
  • Measurement
  • Notation
  • Security
  • Security Protocols
  • Sequences
  • Skeleton
  • Specifications
  • Transmitting
  • Verification
  • Virtual Machines

Fields of Study

  • Computer science

Readers

  • Computer Networking
  • Database Systems and Applications
  • Strategic Security Studies