Efficient finite-state analysis for large security protocols

Abstract

The authors describe two state reduction techniques for finite-state models of security protocols. The techniques exploit certain protocol properties that they have identified as characteristic of security protocols. They prove the soundness of the techniques by demonstrating that any violation of protocol invariants is preserved in the reduced state graph. In addition, they describe an optimization method for evaluating parameterized rule conditions, which are common in models of security protocols. All three techniques have been implemented in the Mur/spl phi/ verifier.