author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 30549 | d2d7874648bd |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
1 |
(* Title: HOL/SET-Protocol/EventSET.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
2 |
Author: Giampaolo Bella |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
3 |
Author: Fabio Massacci |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
4 |
Author: Lawrence C Paulson |
14199 | 5 |
*) |
6 |
||
7 |
header{*Theory of Events for SET*} |
|
8 |
||
16417 | 9 |
theory EventSET imports MessageSET begin |
14199 | 10 |
|
11 |
text{*The Root Certification Authority*} |
|
12 |
syntax RCA :: agent |
|
13 |
translations "RCA" == "CA 0" |
|
14 |
||
15 |
||
16 |
text{*Message events*} |
|
17 |
datatype |
|
18 |
event = Says agent agent msg |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
19 |
| Gets agent msg |
14199 | 20 |
| Notes agent msg |
21 |
||
22 |
||
23 |
text{*compromised agents: keys known, Notes visible*} |
|
24 |
consts bad :: "agent set" |
|
25 |
||
26 |
text{*Spy has access to his own key for spoof messages, but RCA is secure*} |
|
27 |
specification (bad) |
|
28 |
Spy_in_bad [iff]: "Spy \<in> bad" |
|
29 |
RCA_not_bad [iff]: "RCA \<notin> bad" |
|
30 |
by (rule exI [of _ "{Spy}"], simp) |
|
31 |
||
32 |
||
33 |
subsection{*Agents' Knowledge*} |
|
34 |
||
35 |
consts (*Initial states of agents -- parameter of the construction*) |
|
36 |
initState :: "agent => msg set" |
|
37 |
knows :: "[agent, event list] => msg set" |
|
38 |
||
39 |
(* Message reception does not extend spy's knowledge because of |
|
40 |
reception invariant enforced by Reception rule in protocol definition*) |
|
41 |
primrec |
|
42 |
||
43 |
knows_Nil: |
|
44 |
"knows A [] = initState A" |
|
45 |
knows_Cons: |
|
46 |
"knows A (ev # evs) = |
|
47 |
(if A = Spy then |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
48 |
(case ev of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
49 |
Says A' B X => insert X (knows Spy evs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
50 |
| Gets A' X => knows Spy evs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
51 |
| Notes A' X => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
52 |
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
53 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
54 |
(case ev of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
55 |
Says A' B X => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
56 |
if A'=A then insert X (knows A evs) else knows A evs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
57 |
| Gets A' X => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
58 |
if A'=A then insert X (knows A evs) else knows A evs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
59 |
| Notes A' X => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
60 |
if A'=A then insert X (knows A evs) else knows A evs))" |
14199 | 61 |
|
62 |
||
63 |
subsection{*Used Messages*} |
|
64 |
||
65 |
consts |
|
66 |
(*Set of items that might be visible to somebody: |
|
67 |
complement of the set of fresh items*) |
|
68 |
used :: "event list => msg set" |
|
69 |
||
70 |
(* As above, message reception does extend used items *) |
|
71 |
primrec |
|
72 |
used_Nil: "used [] = (UN B. parts (initState B))" |
|
73 |
used_Cons: "used (ev # evs) = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
74 |
(case ev of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
75 |
Says A B X => parts {X} Un (used evs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
76 |
| Gets A X => used evs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30549
diff
changeset
|
77 |
| Notes A X => parts {X} Un (used evs))" |
14199 | 78 |
|
79 |
||
80 |
||
81 |
(* Inserted by default but later removed. This declaration lets the file |
|
82 |
be re-loaded. Addsimps [knows_Cons, used_Nil, *) |
|
83 |
||
84 |
(** Simplifying parts (insert X (knows Spy evs)) |
|
85 |
= parts {X} Un parts (knows Spy evs) -- since general case loops*) |
|
86 |
||
87 |
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard] |
|
88 |
||
89 |
lemma knows_Spy_Says [simp]: |
|
90 |
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)" |
|
91 |
by auto |
|
92 |
||
93 |
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits |
|
94 |
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*} |
|
95 |
lemma knows_Spy_Notes [simp]: |
|
96 |
"knows Spy (Notes A X # evs) = |
|
97 |
(if A:bad then insert X (knows Spy evs) else knows Spy evs)" |
|
98 |
apply auto |
|
99 |
done |
|
100 |
||
101 |
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" |
|
102 |
by auto |
|
103 |
||
104 |
lemma initState_subset_knows: "initState A <= knows A evs" |
|
105 |
apply (induct_tac "evs") |
|
106 |
apply (auto split: event.split) |
|
107 |
done |
|
108 |
||
109 |
lemma knows_Spy_subset_knows_Spy_Says: |
|
110 |
"knows Spy evs <= knows Spy (Says A B X # evs)" |
|
111 |
by auto |
|
112 |
||
113 |
lemma knows_Spy_subset_knows_Spy_Notes: |
|
114 |
"knows Spy evs <= knows Spy (Notes A X # evs)" |
|
115 |
by auto |
|
116 |
||
117 |
lemma knows_Spy_subset_knows_Spy_Gets: |
|
118 |
"knows Spy evs <= knows Spy (Gets A X # evs)" |
|
119 |
by auto |
|
120 |
||
121 |
(*Spy sees what is sent on the traffic*) |
|
122 |
lemma Says_imp_knows_Spy [rule_format]: |
|
123 |
"Says A B X \<in> set evs --> X \<in> knows Spy evs" |
|
124 |
apply (induct_tac "evs") |
|
125 |
apply (auto split: event.split) |
|
126 |
done |
|
127 |
||
128 |
(*Use with addSEs to derive contradictions from old Says events containing |
|
129 |
items known to be fresh*) |
|
130 |
lemmas knows_Spy_partsEs = |
|
131 |
Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] |
|
132 |
parts.Body [THEN revcut_rl, standard] |
|
133 |
||
134 |
||
135 |
subsection{*The Function @{term used}*} |
|
136 |
||
137 |
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs" |
|
138 |
apply (induct_tac "evs") |
|
139 |
apply (auto simp add: parts_insert_knows_A split: event.split) |
|
140 |
done |
|
141 |
||
142 |
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
|
143 |
||
144 |
lemma initState_subset_used: "parts (initState B) <= used evs" |
|
145 |
apply (induct_tac "evs") |
|
146 |
apply (auto split: event.split) |
|
147 |
done |
|
148 |
||
149 |
lemmas initState_into_used = initState_subset_used [THEN subsetD] |
|
150 |
||
151 |
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} Un used evs" |
|
152 |
by auto |
|
153 |
||
154 |
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} Un used evs" |
|
155 |
by auto |
|
156 |
||
157 |
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" |
|
158 |
by auto |
|
159 |
||
160 |
||
161 |
lemma Notes_imp_parts_subset_used [rule_format]: |
|
162 |
"Notes A X \<in> set evs --> parts {X} <= used evs" |
|
163 |
apply (induct_tac "evs") |
|
164 |
apply (induct_tac [2] "a", auto) |
|
165 |
done |
|
166 |
||
167 |
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
168 |
declare knows_Cons [simp del] |
|
169 |
used_Nil [simp del] used_Cons [simp del] |
|
170 |
||
171 |
||
172 |
text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"} |
|
173 |
New events added by induction to "evs" are discarded. Provided |
|
174 |
this information isn't needed, the proof will be much shorter, since |
|
175 |
it will omit complicated reasoning about @{term analz}.*} |
|
176 |
||
177 |
lemmas analz_mono_contra = |
|
178 |
knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] |
|
179 |
knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] |
|
180 |
knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] |
|
27225 | 181 |
|
182 |
lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard] |
|
183 |
||
14199 | 184 |
ML |
185 |
{* |
|
186 |
val analz_mono_contra_tac = |
|
27225 | 187 |
rtac @{thm analz_impI} THEN' |
188 |
REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) |
|
189 |
THEN' mp_tac |
|
14199 | 190 |
*} |
191 |
||
192 |
method_setup analz_mono_contra = {* |
|
30549 | 193 |
Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} |
14199 | 194 |
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" |
195 |
||
196 |
end |