Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions
Abstract
Most protocol analysis tools and techniques operate by proving/disproving security properties of a protocol formulated as predicates in a specific logic. Starting from some initial assumptions, theorem proving or model checking (such as in[8]) techniques can be used to check if a certain security property follows. In this paper, we take a different approach to this problem. Instead of checking each security property individually, our approach is to characterize all protocol executions compatible with the initial assumptions. The resulting characterization is a set of protocol runs that is representative of all possible protocol runs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2005
- Accession Number
- AD1137513
Entities
People
- F. J. Thayer
- Joshua D. Guttman
- Shaddin F Doghm
Organizations
- MITRE Corporation