|
1 (* Title: HOL/Auth/Event |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Theory of events for security protocols |
|
7 |
|
8 Datatype of events; function "sees"; freshness |
|
9 *) |
|
10 |
|
11 open Event; |
|
12 |
|
13 (*** Function "sees" ***) |
|
14 |
|
15 (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) |
|
16 |
|
17 goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)"; |
|
18 by (Simp_tac 1); |
|
19 qed "sees_own"; |
|
20 |
|
21 goal thy "sees lost B (Notes A X # evs) = \ |
|
22 \ (if A=B then insert X (sees lost B evs) else sees lost B evs)"; |
|
23 by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
24 qed "sees_Notes"; |
|
25 |
|
26 (** Three special-case rules for rewriting of sees lost A **) |
|
27 |
|
28 goal thy "!!A. Server ~= B ==> \ |
|
29 \ sees lost Server (Says A B X # evs) = sees lost Server evs"; |
|
30 by (Asm_simp_tac 1); |
|
31 qed "sees_Server"; |
|
32 |
|
33 goal thy "!!A. Friend i ~= B ==> \ |
|
34 \ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs"; |
|
35 by (Asm_simp_tac 1); |
|
36 qed "sees_Friend"; |
|
37 |
|
38 goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)"; |
|
39 by (Simp_tac 1); |
|
40 qed "sees_Spy"; |
|
41 |
|
42 goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)"; |
|
43 by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
44 by (Fast_tac 1); |
|
45 qed "sees_Says_subset_insert"; |
|
46 |
|
47 goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)"; |
|
48 by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
49 by (Fast_tac 1); |
|
50 qed "sees_subset_sees_Says"; |
|
51 |
|
52 goal thy "sees lost A evs <= sees lost A (Notes A' X # evs)"; |
|
53 by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
54 by (Fast_tac 1); |
|
55 qed "sees_subset_sees_Notes"; |
|
56 |
|
57 (*Pushing Unions into parts. One of the agents A is B, and thus sees Y.*) |
|
58 goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \ |
|
59 \ parts {Y} Un (UN A. parts (sees lost A evs))"; |
|
60 by (Step_tac 1); |
|
61 by (etac rev_mp 1); (*split_tac does not work on assumptions*) |
|
62 by (ALLGOALS |
|
63 (fast_tac (!claset addss (!simpset addsimps [parts_Un] |
|
64 setloop split_tac [expand_if])))); |
|
65 qed "UN_parts_sees_Says"; |
|
66 |
|
67 goal thy "(UN A. parts (sees lost A (Notes B Y # evs))) = \ |
|
68 \ parts {Y} Un (UN A. parts (sees lost A evs))"; |
|
69 by (Step_tac 1); |
|
70 by (etac rev_mp 1); (*split_tac does not work on assumptions*) |
|
71 by (ALLGOALS |
|
72 (fast_tac (!claset addss (!simpset addsimps [parts_Un] |
|
73 setloop split_tac [expand_if])))); |
|
74 qed "UN_parts_sees_Notes"; |
|
75 |
|
76 goal thy "Says A B X : set evs --> X : sees lost Spy evs"; |
|
77 by (list.induct_tac "evs" 1); |
|
78 by (Auto_tac ()); |
|
79 qed_spec_mp "Says_imp_sees_Spy"; |
|
80 |
|
81 (*Use with addSEs to derive contradictions from old Says events containing |
|
82 items known to be fresh*) |
|
83 val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; |
|
84 |
|
85 Addsimps [sees_own, sees_Notes, sees_Server, sees_Friend, sees_Spy]; |
|
86 |
|
87 (**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****) |
|
88 Delsimps [sees_Cons]; |
|
89 |
|
90 |
|
91 (*** Fresh nonces ***) |
|
92 |
|
93 goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs"; |
|
94 by (etac (impOfSubs parts_mono) 1); |
|
95 by (Fast_tac 1); |
|
96 qed "usedI"; |
|
97 AddIs [usedI]; |
|
98 |
|
99 goal thy "used (Says A B X # evs) = parts{X} Un used evs"; |
|
100 by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1); |
|
101 qed "used_Says"; |
|
102 Addsimps [used_Says]; |
|
103 |
|
104 goal thy "used (Notes A X # evs) = parts{X} Un used evs"; |
|
105 by (simp_tac (!simpset delsimps [sees_Notes] |
|
106 addsimps [used_def, UN_parts_sees_Notes]) 1); |
|
107 qed "used_Notes"; |
|
108 Addsimps [used_Notes]; |
|
109 |
|
110 (*These two facts about "used" are unused.*) |
|
111 goal thy "used [] <= used l"; |
|
112 by (list.induct_tac "l" 1); |
|
113 by (event.induct_tac "a" 2); |
|
114 by (ALLGOALS Asm_simp_tac); |
|
115 by (ALLGOALS Blast_tac); |
|
116 qed "used_nil_subset"; |
|
117 |
|
118 goal thy "used l <= used (l@l')"; |
|
119 by (list.induct_tac "l" 1); |
|
120 by (simp_tac (!simpset addsimps [used_nil_subset]) 1); |
|
121 by (event.induct_tac "a" 1); |
|
122 by (ALLGOALS Asm_simp_tac); |
|
123 by (ALLGOALS Blast_tac); |
|
124 qed "used_subset_append"; |
|
125 |
|
126 |
|
127 (** Simplifying parts (insert X (sees lost A evs)) |
|
128 = parts {X} Un parts (sees lost A evs) -- since general case loops*) |
|
129 |
|
130 val parts_insert_sees = |
|
131 parts_insert |> read_instantiate_sg (sign_of thy) |
|
132 [("H", "sees lost A evs")] |
|
133 |> standard; |
|
134 |
|
135 |
|
136 |
|
137 (*For proving theorems of the form X ~: analz (sees Spy evs) --> P |
|
138 New events added by induction to "evs" are discarded. Provided |
|
139 this information isn't needed, the proof will be much shorter, since |
|
140 it will omit complicated reasoning about analz.*) |
|
141 val analz_mono_contra_tac = |
|
142 let val impI' = read_instantiate_sg (sign_of thy) |
|
143 [("P", "?Y ~: analz (sees lost ?A ?evs)")] impI; |
|
144 in |
|
145 rtac impI THEN' |
|
146 REPEAT1 o |
|
147 (dresolve_tac |
|
148 [sees_subset_sees_Says RS analz_mono RS contra_subsetD, |
|
149 sees_subset_sees_Notes RS analz_mono RS contra_subsetD]) |
|
150 THEN' |
|
151 mp_tac |
|
152 end; |