Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions
January 2007
Shaddin F. Doghmi, The MITRE Corporation
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
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.
Additional Search Keywords
N/A
|
