author | bulwahn |
Tue, 10 Jul 2012 18:41:34 +0200 | |
changeset 48224 | f2dd90cc724b |
child 48243 | b149de01d669 |
permissions | -rw-r--r-- |
48224
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
1 |
theory Needham_Schroeder_No_Attacker_Example |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
2 |
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
3 |
begin |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
4 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
5 |
datatype agent = Alice | Bob | Spy |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
6 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
7 |
definition agents :: "agent set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
8 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
9 |
"agents = {Spy, Alice, Bob}" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
10 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
11 |
definition bad :: "agent set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
12 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
13 |
"bad = {Spy}" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
14 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
15 |
datatype key = pubEK agent | priEK agent |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
16 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
17 |
fun invKey |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
18 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
19 |
"invKey (pubEK A) = priEK A" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
20 |
| "invKey (priEK A) = pubEK A" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
21 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
22 |
datatype |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
23 |
msg = Agent agent --{*Agent names*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
24 |
| Key key |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
25 |
| Nonce nat --{*Unguessable nonces*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
26 |
| MPair msg msg --{*Compound messages*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
27 |
| Crypt key msg --{*Encryption, public- or shared-key*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
28 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
29 |
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
30 |
syntax |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
31 |
"_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
32 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
33 |
syntax (xsymbols) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
34 |
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
35 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
36 |
translations |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
37 |
"{|x, y, z|}" == "{|x, {|y, z|}|}" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
38 |
"{|x, y|}" == "CONST MPair x y" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
39 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
40 |
inductive_set |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
41 |
parts :: "msg set => msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
42 |
for H :: "msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
43 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
44 |
Inj [intro]: "X \<in> H ==> X \<in> parts H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
45 |
| Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
46 |
| Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
47 |
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
48 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
49 |
inductive_set |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
50 |
analz :: "msg set => msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
51 |
for H :: "msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
52 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
53 |
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
54 |
| Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
55 |
| Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
56 |
| Decrypt [dest]: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
57 |
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
58 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
59 |
inductive_set |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
60 |
synth :: "msg set => msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
61 |
for H :: "msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
62 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
63 |
Inj [intro]: "X \<in> H ==> X \<in> synth H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
64 |
| Agent [intro]: "Agent agt \<in> synth H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
65 |
| MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
66 |
| Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
67 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
68 |
primrec initState |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
69 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
70 |
initState_Alice: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
71 |
"initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
72 |
| initState_Bob: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
73 |
"initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
74 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
75 |
| initState_Spy: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
76 |
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
77 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
78 |
datatype |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
79 |
event = Says agent agent msg |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
80 |
| Gets agent msg |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
81 |
| Notes agent msg |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
82 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
83 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
84 |
primrec knows :: "agent => event list => msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
85 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
86 |
knows_Nil: "knows A [] = initState A" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
87 |
| knows_Cons: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
88 |
"knows A (ev # evs) = |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
89 |
(if A = Spy then |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
90 |
(case ev of |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
91 |
Says A' B X => insert X (knows Spy evs) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
92 |
| Gets A' X => knows Spy evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
93 |
| Notes A' X => |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
94 |
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
95 |
else |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
96 |
(case ev of |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
97 |
Says A' B X => |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
98 |
if A'=A then insert X (knows A evs) else knows A evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
99 |
| Gets A' X => |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
100 |
if A'=A then insert X (knows A evs) else knows A evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
101 |
| Notes A' X => |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
102 |
if A'=A then insert X (knows A evs) else knows A evs))" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
103 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
104 |
abbreviation (input) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
105 |
spies :: "event list => msg set" where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
106 |
"spies == knows Spy" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
107 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
108 |
primrec used :: "event list => msg set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
109 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
110 |
used_Nil: "used [] = Union (parts ` initState ` agents)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
111 |
| used_Cons: "used (ev # evs) = |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
112 |
(case ev of |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
113 |
Says A B X => parts {X} \<union> used evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
114 |
| Gets A X => used evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
115 |
| Notes A X => parts {X} \<union> used evs)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
116 |
(* --{*The case for @{term Gets} seems anomalous, but @{term Gets} always |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
117 |
follows @{term Says} in real protocols. Seems difficult to change. |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
118 |
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
119 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
120 |
inductive_set ns_public :: "event list set" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
121 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
122 |
(*Initial trace is empty*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
123 |
Nil: "[] \<in> ns_public" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
124 |
(*Alice initiates a protocol run, sending a nonce to Bob*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
125 |
| NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
126 |
\<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
127 |
# evs1 \<in> ns_public" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
128 |
(*Bob responds to Alice's message with a further nonce*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
129 |
| NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
130 |
Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
131 |
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
132 |
# evs2 \<in> ns_public" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
133 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
134 |
(*Alice proves her existence by sending NB back to Bob.*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
135 |
| NS3: "\<lbrakk>evs3 \<in> ns_public; |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
136 |
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
137 |
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
138 |
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
139 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
140 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
141 |
subsection {* Preparations for sets *} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
142 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
143 |
fun find_first :: "('a => 'b option) => 'a list => 'b option" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
144 |
where |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
145 |
"find_first f [] = None" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
146 |
| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
147 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
148 |
consts cps_of_set :: "'a set => ('a => term list option) => term list option" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
149 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
150 |
lemma |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
151 |
[code]: "cps_of_set (set xs) f = find_first f xs" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
152 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
153 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
154 |
consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
155 |
consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
156 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
157 |
lemma |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
158 |
[code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
159 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
160 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
161 |
consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
162 |
=> 'b list => 'a Quickcheck_Exhaustive.three_valued" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
163 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
164 |
lemma [code]: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
165 |
"find_first' f [] = Quickcheck_Exhaustive.No_value" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
166 |
"find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
167 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
168 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
169 |
lemma |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
170 |
[code]: "neg_cps_of_set (set xs) f i = find_first' f xs" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
171 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
172 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
173 |
setup {* |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
174 |
let |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
175 |
val Fun = Predicate_Compile_Aux.Fun |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
176 |
val Input = Predicate_Compile_Aux.Input |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
177 |
val Output = Predicate_Compile_Aux.Output |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
178 |
val Bool = Predicate_Compile_Aux.Bool |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
179 |
val oi = Fun (Output, Fun (Input, Bool)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
180 |
val ii = Fun (Input, Fun (Input, Bool)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
181 |
fun of_set compfuns (Type ("fun", [T, _])) = |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
182 |
case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
183 |
Type ("Quickcheck_Exhaustive.three_valued", _) => |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
184 |
Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
185 |
| Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
186 |
| _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
187 |
fun member compfuns (U as Type ("fun", [T, _])) = |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
188 |
(absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
189 |
(Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0)))) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
190 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
191 |
in |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
192 |
Core_Data.force_modes_and_compilations @{const_name Set.member} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
193 |
[(oi, (of_set, false)), (ii, (member, false))] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
194 |
end |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
195 |
*} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
196 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
197 |
subsection {* Derived equations for analz, parts and synth *} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
198 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
199 |
lemma [code]: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
200 |
"analz H = (let |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
201 |
H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
202 |
in if H' = H then H else analz H')" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
203 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
204 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
205 |
lemma [code]: |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
206 |
"parts H = (let |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
207 |
H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H)) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
208 |
in if H' = H then H else parts H')" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
209 |
sorry |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
210 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
211 |
code_pred [skip_proof] ns_publicp . |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
212 |
thm ns_publicp.equation |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
213 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
214 |
code_pred [generator_cps] ns_publicp . |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
215 |
thm ns_publicp.generator_cps_equation |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
216 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
217 |
setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
218 |
declare ListMem_iff[symmetric, code_pred_inline] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
219 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
220 |
declare [[quickcheck_timing]] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
221 |
setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
222 |
declare [[quickcheck_full_support = false]] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
223 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
224 |
lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
225 |
(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
226 |
quickcheck[exhaustive, size = 8, timeout = 3600, verbose] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
227 |
quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
228 |
quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
229 |
oops |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
230 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
231 |
lemma |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
232 |
"\<lbrakk>ns_publicp evs\<rbrakk> |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
233 |
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
234 |
\<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
235 |
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
236 |
quickcheck[smart_exhaustive, depth = 6, timeout = 30] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
237 |
quickcheck[narrowing, size = 6, timeout = 30, verbose] |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
238 |
oops |
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
239 |
|
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset
|
240 |
end |