2274
|
1 |
(* Title: HOL/Auth/WooLam
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1996 University of Cambridge
|
|
5 |
|
|
6 |
Inductive relation "woolam" for the Woo-Lam protocol.
|
|
7 |
|
|
8 |
Simplified version from page 11 of
|
|
9 |
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
|
|
10 |
IEEE Trans. S.E. 22(1), 1996, pages 6-15.
|
|
11 |
*)
|
|
12 |
|
|
13 |
open WooLam;
|
|
14 |
|
|
15 |
proof_timing:=true;
|
|
16 |
HOL_quantifiers := false;
|
|
17 |
Pretty.setdepth 20;
|
|
18 |
|
|
19 |
|
|
20 |
(*Weak liveness: there are traces that reach the end*)
|
|
21 |
goal thy
|
|
22 |
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
|
|
23 |
\ ==> EX NB. EX evs: woolam lost. \
|
|
24 |
\ Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) \
|
|
25 |
\ : set_of_list evs";
|
|
26 |
by (REPEAT (resolve_tac [exI,bexI] 1));
|
|
27 |
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
|
|
28 |
woolam.WL4 RS woolam.WL5) 2);
|
|
29 |
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
|
|
30 |
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
|
|
31 |
by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
|
|
32 |
result();
|
|
33 |
|
|
34 |
|
|
35 |
(**** Inductive proofs about woolam ****)
|
|
36 |
|
|
37 |
(*Nobody sends themselves messages*)
|
|
38 |
goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs";
|
|
39 |
by (etac woolam.induct 1);
|
|
40 |
by (Auto_tac());
|
|
41 |
qed_spec_mp "not_Says_to_self";
|
|
42 |
Addsimps [not_Says_to_self];
|
|
43 |
AddSEs [not_Says_to_self RSN (2, rev_notE)];
|
|
44 |
|
|
45 |
|
|
46 |
(** For reasoning about the encrypted portion of messages **)
|
|
47 |
|
|
48 |
goal thy "!!evs. Says A' B X : set_of_list evs \
|
|
49 |
\ ==> X : analz (sees lost Spy evs)";
|
|
50 |
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
|
|
51 |
qed "WL4_analz_sees_Spy";
|
|
52 |
|
|
53 |
bind_thm ("WL4_parts_sees_Spy",
|
|
54 |
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
|
|
55 |
|
|
56 |
(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
|
|
57 |
harder to complete, since simplification does less for us.*)
|
|
58 |
val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6;
|
|
59 |
|
|
60 |
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
|
|
61 |
fun parts_induct_tac i = SELECT_GOAL
|
|
62 |
(DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
|
|
63 |
(*Fake message*)
|
|
64 |
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
|
|
65 |
impOfSubs Fake_parts_insert]
|
|
66 |
addss (!simpset)) 2)) THEN
|
|
67 |
(*Base case*)
|
|
68 |
fast_tac (!claset addss (!simpset)) 1 THEN
|
|
69 |
ALLGOALS Asm_simp_tac) i;
|
|
70 |
|
|
71 |
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
|
|
72 |
sends messages containing X! **)
|
|
73 |
|
|
74 |
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
|
|
75 |
goal thy
|
|
76 |
"!!evs. evs : woolam lost \
|
|
77 |
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
|
|
78 |
by (parts_induct_tac 1);
|
|
79 |
by (Auto_tac());
|
|
80 |
qed "Spy_see_shrK";
|
|
81 |
Addsimps [Spy_see_shrK];
|
|
82 |
|
|
83 |
goal thy
|
|
84 |
"!!evs. evs : woolam lost \
|
|
85 |
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
|
|
86 |
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
|
|
87 |
qed "Spy_analz_shrK";
|
|
88 |
Addsimps [Spy_analz_shrK];
|
|
89 |
|
|
90 |
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
|
|
91 |
\ evs : woolam lost |] ==> A:lost";
|
|
92 |
by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
|
|
93 |
qed "Spy_see_shrK_D";
|
|
94 |
|
|
95 |
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
|
|
96 |
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
|
|
97 |
|
|
98 |
|
|
99 |
(*** Future nonces can't be seen or used! ***)
|
|
100 |
|
|
101 |
goal thy "!!evs. evs : woolam lost ==> \
|
|
102 |
\ length evs <= length evt --> \
|
|
103 |
\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
|
|
104 |
by (parts_induct_tac 1);
|
|
105 |
by (REPEAT_FIRST (fast_tac (!claset
|
|
106 |
addSEs partsEs
|
|
107 |
addSDs [Says_imp_sees_Spy RS parts.Inj]
|
|
108 |
addEs [leD RS notE]
|
|
109 |
addDs [impOfSubs analz_subset_parts,
|
|
110 |
impOfSubs parts_insert_subset_Un,
|
|
111 |
Suc_leD]
|
|
112 |
addss (!simpset))));
|
|
113 |
qed_spec_mp "new_nonces_not_seen";
|
|
114 |
Addsimps [new_nonces_not_seen];
|
|
115 |
|
|
116 |
|
|
117 |
(**** Autheticity properties for Woo-Lam ****)
|
|
118 |
|
|
119 |
|
|
120 |
(*** WL4 ***)
|
|
121 |
|
|
122 |
(*If the encrypted message appears then it originated with Alice*)
|
|
123 |
goal thy
|
|
124 |
"!!evs. [| A ~: lost; evs : woolam lost |] \
|
|
125 |
\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) \
|
|
126 |
\ --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)";
|
|
127 |
by (parts_induct_tac 1);
|
|
128 |
by (Fast_tac 1);
|
|
129 |
qed_spec_mp "NB_Crypt_imp_Alice_msg";
|
|
130 |
|
|
131 |
(*Guarantee for Server: if it gets a message containing a certificate from
|
|
132 |
Alice, then she originated that certificate. But we DO NOT know that B
|
|
133 |
ever saw it: the Spy may have rerouted the message to the Server.*)
|
|
134 |
goal thy
|
|
135 |
"!!evs. [| A ~: lost; evs : woolam lost; \
|
|
136 |
\ Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \
|
|
137 |
\ : set_of_list evs |] \
|
|
138 |
\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
|
|
139 |
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
|
|
140 |
addSEs [MPair_parts]
|
|
141 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
|
|
142 |
qed "Server_trust_WL4";
|
|
143 |
|
|
144 |
|
|
145 |
(*** WL5 ***)
|
|
146 |
|
|
147 |
(*Server sent WL5 only if it received the right sort of message*)
|
|
148 |
goal thy
|
|
149 |
"!!evs. evs : woolam lost ==> \
|
|
150 |
\ Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs \
|
|
151 |
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \
|
|
152 |
\ : set_of_list evs)";
|
|
153 |
by (parts_induct_tac 1);
|
|
154 |
by (ALLGOALS Fast_tac);
|
|
155 |
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
|
|
156 |
|
|
157 |
|
|
158 |
(*If the encrypted message appears then it originated with the Server!*)
|
|
159 |
goal thy
|
|
160 |
"!!evs. [| B ~: lost; evs : woolam lost |] \
|
|
161 |
\ ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs) \
|
|
162 |
\ --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
|
|
163 |
by (parts_induct_tac 1);
|
|
164 |
qed_spec_mp "NB_Crypt_imp_Server_msg";
|
|
165 |
|
|
166 |
(*Partial guarantee for B: if it gets a message of correct form then the Server
|
|
167 |
sent the same message.*)
|
|
168 |
goal thy
|
|
169 |
"!!evs. [| Says S B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs; \
|
|
170 |
\ B ~: lost; evs : woolam lost |] \
|
|
171 |
\ ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
|
|
172 |
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
|
|
173 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
|
|
174 |
qed "B_got_WL5";
|
|
175 |
|
|
176 |
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
|
|
177 |
the nonce using her key. This event can be no older than the nonce itself.
|
|
178 |
But A may have sent the nonce to some other agent and it could have reached
|
|
179 |
the Server via the Spy.*)
|
|
180 |
goal thy
|
|
181 |
"!!evs. [| Says S B (Crypt {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \
|
|
182 |
\ A ~: lost; B ~: lost; evs : woolam lost |] \
|
|
183 |
\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
|
|
184 |
by (fast_tac (!claset addIs [Server_trust_WL4]
|
|
185 |
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
|
|
186 |
qed "B_trust_WL5";
|
|
187 |
|
|
188 |
|
|
189 |
(*B only issues challenges in response to WL1. Useful??*)
|
|
190 |
goal thy
|
|
191 |
"!!evs. [| B ~= Spy; evs : woolam lost |] \
|
|
192 |
\ ==> Says B A (Nonce NB) : set_of_list evs \
|
|
193 |
\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
|
|
194 |
by (parts_induct_tac 1);
|
|
195 |
by (ALLGOALS Fast_tac);
|
|
196 |
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
|
|
197 |
|
|
198 |
|
|
199 |
(**CANNOT be proved because A doesn't know where challenges come from...
|
|
200 |
goal thy
|
|
201 |
"!!evs. [| A ~: lost; B ~= Spy; evs : woolam lost |] \
|
|
202 |
\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) & \
|
|
203 |
\ Says B A (Nonce NB) : set_of_list evs \
|
|
204 |
\ --> Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
|
|
205 |
by (parts_induct_tac 1);
|
|
206 |
by (Step_tac 1);
|
|
207 |
by (best_tac (!claset addSEs partsEs
|
|
208 |
addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);
|
|
209 |
**)
|