theory Needham_Schroeder_No_Attacker_Example imports Needham_Schroeder_Base begin inductive_set ns_public :: "event list set" where (*Initial trace is empty*) Nil: "[] \ ns_public" (*Alice initiates a protocol run, sending a nonce to Bob*) | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) # evs1 \ ns_public" (*Bob responds to Alice's message with a further nonce*) | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) # evs2 \ ns_public" (*Alice proves her existence by sending NB back to Bob.*) | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" code_pred [skip_proof] ns_publicp . thm ns_publicp.equation code_pred [generator_cps] ns_publicp . thm ns_publicp.generator_cps_equation lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" (*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] quickcheck[exhaustive, size = 8, timeout = 3600, verbose] quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] oops lemma "\ns_publicp evs\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs \ A \ Spy \ B \ Spy \ A \ B \ Nonce NB \ analz (spies evs)" quickcheck[smart_exhaustive, depth = 6, timeout = 30] quickcheck[narrowing, size = 6, timeout = 30, verbose] oops end