##
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).