1 theory Needham_Schroeder_No_Attacker_Example |
|
2 imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
|
3 begin |
|
4 |
|
5 inductive_set ns_public :: "event list set" |
|
6 where |
|
7 (*Initial trace is empty*) |
|
8 Nil: "[] \<in> ns_public" |
|
9 (*Alice initiates a protocol run, sending a nonce to Bob*) |
|
10 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
|
11 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
|
12 # evs1 \<in> ns_public" |
|
13 (*Bob responds to Alice's message with a further nonce*) |
|
14 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
|
15 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
|
16 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) |
|
17 # evs2 \<in> ns_public" |
|
18 |
|
19 (*Alice proves her existence by sending NB back to Bob.*) |
|
20 | NS3: "\<lbrakk>evs3 \<in> ns_public; |
|
21 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
|
22 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
|
23 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
24 |
|
25 code_pred [skip_proof] ns_publicp . |
|
26 thm ns_publicp.equation |
|
27 |
|
28 code_pred [generator_cps] ns_publicp . |
|
29 thm ns_publicp.generator_cps_equation |
|
30 |
|
31 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" |
|
32 (*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] |
|
33 quickcheck[exhaustive, size = 8, timeout = 3600, verbose] |
|
34 quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) |
|
35 quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] |
|
36 oops |
|
37 |
|
38 lemma |
|
39 "\<lbrakk>ns_publicp evs\<rbrakk> |
|
40 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs |
|
41 \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B |
|
42 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
|
43 quickcheck[smart_exhaustive, depth = 6, timeout = 30] |
|
44 quickcheck[narrowing, size = 6, timeout = 30, verbose] |
|
45 oops |
|
46 |
|
47 end |
|