R. Grosu/Huang/Smolka/Yang: Monte Carlo Analysis of Security Protocols: Needham Schroeder Revisited

Monte Carlo Analysis of Security Protocols: Needham Schroeder Revisited*

R. Grosu, X. Huang, S.A. Smolka and P. Yang

We apply Monte Carlo model checking to the Needham-Schroeder public key authentication protocol. The Monte Carlo approach uses random sampling of ``lassos'' (reachable cycles) to compute an estimate of the weighted expectation that a system $ S$ satisfies an LTL formula $ \varphi$ within a factor of $ 1 \pm \epsilon$ with probability at least $ 1 - \delta$. It does so using a number of samples $ N$ that is optimal to within a constant factor, and in expected time $ O(N \cdot D)$ and expected space $ O(D)$, where $ D$ is the recurrence diameter of the directed graph representing the product of $ S$'s state transition graph and the Büchi automaton for $ \neg\varphi$. Our results indicate that Monte Carlo model checking can find attacks in security protocols like Needham-Schroeder when traditional model checkers fail due to state explosion; and that the weighted expectation that Needham-Schroder is attack-free increases linearly with the nonce range (number of rounds).

In Proc. of the DIMACS Workshop on Security Analysis of Protocols, Rutgers University, June 2004, USA.

*R. Grosu and X. Huang were partially supported by the NSF Faculty Early Career Development Award CCR01-33583.