71 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
69 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
72 sends messages containing X! **) |
70 sends messages containing X! **) |
73 |
71 |
74 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
72 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
75 goal thy |
73 goal thy |
76 "!!evs. evs : woolam lost \ |
74 "!!evs. evs : woolam \ |
77 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
75 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
78 by (parts_induct_tac 1); |
76 by (parts_induct_tac 1); |
79 by (Auto_tac()); |
77 by (Auto_tac()); |
80 qed "Spy_see_shrK"; |
78 qed "Spy_see_shrK"; |
81 Addsimps [Spy_see_shrK]; |
79 Addsimps [Spy_see_shrK]; |
82 |
80 |
83 goal thy |
81 goal thy |
84 "!!evs. evs : woolam lost \ |
82 "!!evs. evs : woolam \ |
85 \ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
83 \ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
86 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
84 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
87 qed "Spy_analz_shrK"; |
85 qed "Spy_analz_shrK"; |
88 Addsimps [Spy_analz_shrK]; |
86 Addsimps [Spy_analz_shrK]; |
89 |
87 |
90 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
88 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
91 \ evs : woolam lost |] ==> A:lost"; |
89 \ evs : woolam |] ==> A:lost"; |
92 by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
90 by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
93 qed "Spy_see_shrK_D"; |
91 qed "Spy_see_shrK_D"; |
94 |
92 |
95 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
93 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]; |
94 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
97 |
95 |
98 |
96 |
99 (*** Future nonces can't be seen or used! ***) |
97 (*** Future nonces can't be seen or used! ***) |
100 |
98 |
101 goal thy "!!evs. evs : woolam lost ==> \ |
99 goal thy "!!evs. evs : woolam ==> \ |
102 \ length evs <= length evt --> \ |
100 \ length evs <= length evt --> \ |
103 \ Nonce (newN evt) ~: parts (sees lost Spy evs)"; |
101 \ Nonce (newN evt) ~: parts (sees lost Spy evs)"; |
104 by (parts_induct_tac 1); |
102 by (parts_induct_tac 1); |
105 by (REPEAT_FIRST (fast_tac (!claset |
103 by (REPEAT_FIRST (fast_tac (!claset |
106 addSEs partsEs |
104 addSEs partsEs |
119 |
117 |
120 (*** WL4 ***) |
118 (*** WL4 ***) |
121 |
119 |
122 (*If the encrypted message appears then it originated with Alice*) |
120 (*If the encrypted message appears then it originated with Alice*) |
123 goal thy |
121 goal thy |
124 "!!evs. [| A ~: lost; evs : woolam lost |] \ |
122 "!!evs. [| A ~: lost; evs : woolam |] \ |
125 \ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) \ |
123 \ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \ |
126 \ --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)"; |
124 \ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)"; |
127 by (parts_induct_tac 1); |
125 by (parts_induct_tac 1); |
128 by (Fast_tac 1); |
126 by (Fast_tac 1); |
129 qed_spec_mp "NB_Crypt_imp_Alice_msg"; |
127 qed_spec_mp "NB_Crypt_imp_Alice_msg"; |
130 |
128 |
131 (*Guarantee for Server: if it gets a message containing a certificate from |
129 (*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 |
130 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.*) |
131 ever saw it: the Spy may have rerouted the message to the Server.*) |
134 goal thy |
132 goal thy |
135 "!!evs. [| A ~: lost; evs : woolam lost; \ |
133 "!!evs. [| A ~: lost; evs : woolam; \ |
136 \ Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \ |
134 \ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ |
137 \ : set_of_list evs |] \ |
135 \ : set_of_list evs |] \ |
138 \ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; |
136 \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
139 by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] |
137 by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] |
140 addSEs [MPair_parts] |
138 addSEs [MPair_parts] |
141 addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
139 addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
142 qed "Server_trust_WL4"; |
140 qed "Server_trust_WL4"; |
143 |
141 |
144 |
142 |
145 (*** WL5 ***) |
143 (*** WL5 ***) |
146 |
144 |
147 (*Server sent WL5 only if it received the right sort of message*) |
145 (*Server sent WL5 only if it received the right sort of message*) |
148 goal thy |
146 goal thy |
149 "!!evs. evs : woolam lost ==> \ |
147 "!!evs. evs : woolam ==> \ |
150 \ Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs \ |
148 \ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \ |
151 \ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \ |
149 \ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ |
152 \ : set_of_list evs)"; |
150 \ : set_of_list evs)"; |
153 by (parts_induct_tac 1); |
151 by (parts_induct_tac 1); |
154 by (ALLGOALS Fast_tac); |
152 by (ALLGOALS Fast_tac); |
155 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); |
153 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); |
156 |
154 |
157 |
155 |
158 (*If the encrypted message appears then it originated with the Server!*) |
156 (*If the encrypted message appears then it originated with the Server!*) |
159 goal thy |
157 goal thy |
160 "!!evs. [| B ~: lost; evs : woolam lost |] \ |
158 "!!evs. [| B ~: lost; evs : woolam |] \ |
161 \ ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs) \ |
159 \ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \ |
162 \ --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs"; |
160 \ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; |
163 by (parts_induct_tac 1); |
161 by (parts_induct_tac 1); |
164 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
162 qed_spec_mp "NB_Crypt_imp_Server_msg"; |
165 |
163 |
166 (*Partial guarantee for B: if it gets a message of correct form then the Server |
164 (*Partial guarantee for B: if it gets a message of correct form then the Server |
167 sent the same message.*) |
165 sent the same message.*) |
168 goal thy |
166 goal thy |
169 "!!evs. [| Says S B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs; \ |
167 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \ |
170 \ B ~: lost; evs : woolam lost |] \ |
168 \ B ~: lost; evs : woolam |] \ |
171 \ ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs"; |
169 \ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; |
172 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
170 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
173 addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
171 addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
174 qed "B_got_WL5"; |
172 qed "B_got_WL5"; |
175 |
173 |
176 (*Guarantee for B. If B gets the Server's certificate then A has encrypted |
174 (*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. |
175 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 |
176 But A may have sent the nonce to some other agent and it could have reached |
179 the Server via the Spy.*) |
177 the Server via the Spy.*) |
180 goal thy |
178 goal thy |
181 "!!evs. [| Says S B (Crypt {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \ |
179 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \ |
182 \ A ~: lost; B ~: lost; evs : woolam lost |] \ |
180 \ A ~: lost; B ~: lost; evs : woolam |] \ |
183 \ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; |
181 \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
184 by (fast_tac (!claset addIs [Server_trust_WL4] |
182 by (fast_tac (!claset addIs [Server_trust_WL4] |
185 addSDs [B_got_WL5 RS Server_sent_WL5]) 1); |
183 addSDs [B_got_WL5 RS Server_sent_WL5]) 1); |
186 qed "B_trust_WL5"; |
184 qed "B_trust_WL5"; |
187 |
185 |
188 |
186 |
189 (*B only issues challenges in response to WL1. Useful??*) |
187 (*B only issues challenges in response to WL1. Useful??*) |
190 goal thy |
188 goal thy |
191 "!!evs. [| B ~= Spy; evs : woolam lost |] \ |
189 "!!evs. [| B ~= Spy; evs : woolam |] \ |
192 \ ==> Says B A (Nonce NB) : set_of_list evs \ |
190 \ ==> Says B A (Nonce NB) : set_of_list evs \ |
193 \ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; |
191 \ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; |
194 by (parts_induct_tac 1); |
192 by (parts_induct_tac 1); |
195 by (ALLGOALS Fast_tac); |
193 by (ALLGOALS Fast_tac); |
196 bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); |
194 bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); |
197 |
195 |
198 |
196 |
199 (**CANNOT be proved because A doesn't know where challenges come from... |
197 (**CANNOT be proved because A doesn't know where challenges come from... |
200 goal thy |
198 goal thy |
201 "!!evs. [| A ~: lost; B ~= Spy; evs : woolam lost |] \ |
199 "!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \ |
202 \ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) & \ |
200 \ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \ |
203 \ Says B A (Nonce NB) : set_of_list evs \ |
201 \ Says B A (Nonce NB) : set_of_list evs \ |
204 \ --> Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; |
202 \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
205 by (parts_induct_tac 1); |
203 by (parts_induct_tac 1); |
206 by (Step_tac 1); |
204 by (Step_tac 1); |
207 by (best_tac (!claset addSEs partsEs |
205 by (best_tac (!claset addSEs partsEs |
208 addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); |
206 addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); |
209 **) |
207 **) |