# dimacs04

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 satisfies an LTL formula within a factor of with probability at least . It does so using a number of samples that is optimal to within a constant factor, and in expected time and expected space , where is the recurrence diameter of the directed graph representing the product of 's state transition graph and the Büchi automaton for . 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.