A Hybrid Analysis for Security Protocols with State

July 2014
Topics: Network Protocols, Cybersecurity, Network Security, Computer Security, Data Encryption
Dr. John D. Ramsdell, The MITRE Corporation
Daniel J. Dougherty, Worcester Polytechnic Institute
Joshua D. Guttman, The MITRE Corporation
Paul D. Rowe, The MITRE Corporation
Download PDF (342.52 KB)

Cryptographic protocols rely on message-passing to coordinate activity among principals. Many richly developed tools, based on well-understood foundations, are available for the design and analysis of pure message-passing protocols. However, in many protocols, a principal uses non-local, mutable state to coordinate its local sessions. Cross-session state poses difficulties for protocol analysis tools. We provide a framework for modeling stateful protocols, and a hybrid analysis method. We leverage theorem-proving—specifically, PVS—for reasoning about computations over state. An "enrich-by-need" approach—embodied by CPSA—focuses on the message-passing part. The Envelope Protocol, due to Mark Ryan furnishes a case study.

Publications

Interested in MITRE's Work?

MITRE provides affordable, effective solutions that help the government meet its most complex challenges.
Explore Job Openings

Publication Search