Monte Carlo Analysis of Security Protocols: Needham-Schroeder Revisited

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 F within a factor of 1 +/- \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 . 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 Buchi automaton for \neg F. 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).