src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy
equal
deleted
inserted
replaced
49 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
49 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
50 quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] |
50 quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] |
51 (*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) |
51 (*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) |
52 oops |
52 oops |
53 |
53 |
54 section {* Proving the counterexample trace for validation *} |
54 section \<open>Proving the counterexample trace for validation\<close> |
55 |
55 |
56 lemma |
56 lemma |
57 assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" |
57 assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" |
58 assumes "evs = |
58 assumes "evs = |
59 [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), |
59 [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), |