Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions

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.