34 Unique :: "[event, event list] => bool" ("Unique _ on _") |
34 Unique :: "[event, event list] => bool" ("Unique _ on _") |
35 "Unique ev on evs == |
35 "Unique ev on evs == |
36 ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
36 ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
37 |
37 |
38 |
38 |
39 consts sr :: "event list set" |
39 inductive_set sr :: "event list set" |
40 inductive "sr" |
40 where |
41 intros |
|
42 |
41 |
43 Nil: "[]\<in> sr" |
42 Nil: "[]\<in> sr" |
44 |
43 |
45 |
44 |
46 |
45 |
47 Fake: "\<lbrakk> evsF\<in> sr; X\<in> synth (analz (knows Spy evsF)); |
46 | Fake: "\<lbrakk> evsF\<in> sr; X\<in> synth (analz (knows Spy evsF)); |
48 illegalUse(Card B) \<rbrakk> |
47 illegalUse(Card B) \<rbrakk> |
49 \<Longrightarrow> Says Spy A X # |
48 \<Longrightarrow> Says Spy A X # |
50 Inputs Spy (Card B) X # evsF \<in> sr" |
49 Inputs Spy (Card B) X # evsF \<in> sr" |
51 |
50 |
52 (*In general this rule causes the assumption Card B \<notin> cloned |
51 (*In general this rule causes the assumption Card B \<notin> cloned |
53 in most guarantees for B - starting with confidentiality - |
52 in most guarantees for B - starting with confidentiality - |
54 otherwise pairK_confidential could not apply*) |
53 otherwise pairK_confidential could not apply*) |
55 Forge: |
54 | Forge: |
56 "\<lbrakk> evsFo \<in> sr; Nonce Nb \<in> analz (knows Spy evsFo); |
55 "\<lbrakk> evsFo \<in> sr; Nonce Nb \<in> analz (knows Spy evsFo); |
57 Key (pairK(A,B)) \<in> knows Spy evsFo \<rbrakk> |
56 Key (pairK(A,B)) \<in> knows Spy evsFo \<rbrakk> |
58 \<Longrightarrow> Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \<in> sr" |
57 \<Longrightarrow> Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \<in> sr" |
59 |
58 |
60 |
59 |
61 |
60 |
62 Reception: "\<lbrakk> evsR\<in> sr; Says A B X \<in> set evsR \<rbrakk> |
61 | Reception: "\<lbrakk> evsR\<in> sr; Says A B X \<in> set evsR \<rbrakk> |
63 \<Longrightarrow> Gets B X # evsR \<in> sr" |
62 \<Longrightarrow> Gets B X # evsR \<in> sr" |
64 |
63 |
65 |
64 |
66 |
65 |
67 (*A AND THE SERVER *) |
66 (*A AND THE SERVER *) |
68 SR1: "\<lbrakk> evs1\<in> sr; A \<noteq> Server\<rbrakk> |
67 | SR1: "\<lbrakk> evs1\<in> sr; A \<noteq> Server\<rbrakk> |
69 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> |
68 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> |
70 # evs1 \<in> sr" |
69 # evs1 \<in> sr" |
71 |
70 |
72 SR2: "\<lbrakk> evs2\<in> sr; |
71 | SR2: "\<lbrakk> evs2\<in> sr; |
73 Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
72 Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
74 \<Longrightarrow> Says Server A \<lbrace>Nonce (Pairkey(A,B)), |
73 \<Longrightarrow> Says Server A \<lbrace>Nonce (Pairkey(A,B)), |
75 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace> |
74 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace> |
76 \<rbrace> |
75 \<rbrace> |
77 # evs2 \<in> sr" |
76 # evs2 \<in> sr" |
80 |
79 |
81 |
80 |
82 (*A AND HER CARD*) |
81 (*A AND HER CARD*) |
83 (*A cannot decrypt the verifier for she dosn't know shrK A, |
82 (*A cannot decrypt the verifier for she dosn't know shrK A, |
84 but the pairkey is recognisable*) |
83 but the pairkey is recognisable*) |
85 SR3: "\<lbrakk> evs3\<in> sr; legalUse(Card A); |
84 | SR3: "\<lbrakk> evs3\<in> sr; legalUse(Card A); |
86 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
85 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
87 Gets A \<lbrace>Nonce Pk, Certificate\<rbrace> \<in> set evs3 \<rbrakk> |
86 Gets A \<lbrace>Nonce Pk, Certificate\<rbrace> \<in> set evs3 \<rbrakk> |
88 \<Longrightarrow> Inputs A (Card A) (Agent A) |
87 \<Longrightarrow> Inputs A (Card A) (Agent A) |
89 # evs3 \<in> sr" (*however A only queries her card |
88 # evs3 \<in> sr" (*however A only queries her card |
90 if she has previously contacted the server to initiate with some B. |
89 if she has previously contacted the server to initiate with some B. |
91 Otherwise she would do so even if the Server had not been active. |
90 Otherwise she would do so even if the Server had not been active. |
92 Still, this doesn't and can't mean that the pairkey originated with |
91 Still, this doesn't and can't mean that the pairkey originated with |
93 the server*) |
92 the server*) |
94 |
93 |
95 (*The card outputs the nonce Na to A*) |
94 (*The card outputs the nonce Na to A*) |
96 SR4: "\<lbrakk> evs4\<in> sr; A \<noteq> Server; |
95 | SR4: "\<lbrakk> evs4\<in> sr; A \<noteq> Server; |
97 Nonce Na \<notin> used evs4; legalUse(Card A); |
96 Nonce Na \<notin> used evs4; legalUse(Card A); |
98 Inputs A (Card A) (Agent A) \<in> set evs4 \<rbrakk> |
97 Inputs A (Card A) (Agent A) \<in> set evs4 \<rbrakk> |
99 \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
98 \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
100 # evs4 \<in> sr" |
99 # evs4 \<in> sr" |
101 |
100 |
102 (*The card can be exploited by the spy*) |
101 (*The card can be exploited by the spy*) |
103 (*because of the assumptions on the card, A is certainly not server nor spy*) |
102 (*because of the assumptions on the card, A is certainly not server nor spy*) |
104 SR4Fake: "\<lbrakk> evs4F\<in> sr; Nonce Na \<notin> used evs4F; |
103 | SR4Fake: "\<lbrakk> evs4F\<in> sr; Nonce Na \<notin> used evs4F; |
105 illegalUse(Card A); |
104 illegalUse(Card A); |
106 Inputs Spy (Card A) (Agent A) \<in> set evs4F \<rbrakk> |
105 Inputs Spy (Card A) (Agent A) \<in> set evs4F \<rbrakk> |
107 \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
106 \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
108 # evs4F \<in> sr" |
107 # evs4F \<in> sr" |
109 |
108 |
110 |
109 |
111 |
110 |
112 |
111 |
113 (*A TOWARDS B*) |
112 (*A TOWARDS B*) |
114 SR5: "\<lbrakk> evs5\<in> sr; |
113 | SR5: "\<lbrakk> evs5\<in> sr; |
115 Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs5; |
114 Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs5; |
116 \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk> |
115 \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk> |
117 \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> # evs5 \<in> sr" |
116 \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> # evs5 \<in> sr" |
118 (*A must check that the verifier is not a compound message, |
117 (*A must check that the verifier is not a compound message, |
119 otherwise this would also fire after SR7 *) |
118 otherwise this would also fire after SR7 *) |
120 |
119 |
121 |
120 |
122 |
121 |
123 |
122 |
124 (*B AND HIS CARD*) |
123 (*B AND HIS CARD*) |
125 SR6: "\<lbrakk> evs6\<in> sr; legalUse(Card B); |
124 | SR6: "\<lbrakk> evs6\<in> sr; legalUse(Card B); |
126 Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs6 \<rbrakk> |
125 Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs6 \<rbrakk> |
127 \<Longrightarrow> Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> |
126 \<Longrightarrow> Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> |
128 # evs6 \<in> sr" |
127 # evs6 \<in> sr" |
129 |
128 |
130 (*B gets back from the card the session key and various verifiers*) |
129 (*B gets back from the card the session key and various verifiers*) |
131 SR7: "\<lbrakk> evs7\<in> sr; |
130 | SR7: "\<lbrakk> evs7\<in> sr; |
132 Nonce Nb \<notin> used evs7; legalUse(Card B); B \<noteq> Server; |
131 Nonce Nb \<notin> used evs7; legalUse(Card B); B \<noteq> Server; |
133 K = sesK(Nb,pairK(A,B)); |
132 K = sesK(Nb,pairK(A,B)); |
134 Key K \<notin> used evs7; |
133 Key K \<notin> used evs7; |
135 Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7\<rbrakk> |
134 Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7\<rbrakk> |
136 \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, |
135 \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, |
138 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
137 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
139 # evs7 \<in> sr" |
138 # evs7 \<in> sr" |
140 |
139 |
141 (*The card can be exploited by the spy*) |
140 (*The card can be exploited by the spy*) |
142 (*because of the assumptions on the card, A is certainly not server nor spy*) |
141 (*because of the assumptions on the card, A is certainly not server nor spy*) |
143 SR7Fake: "\<lbrakk> evs7F\<in> sr; Nonce Nb \<notin> used evs7F; |
142 | SR7Fake: "\<lbrakk> evs7F\<in> sr; Nonce Nb \<notin> used evs7F; |
144 illegalUse(Card B); |
143 illegalUse(Card B); |
145 K = sesK(Nb,pairK(A,B)); |
144 K = sesK(Nb,pairK(A,B)); |
146 Key K \<notin> used evs7F; |
145 Key K \<notin> used evs7F; |
147 Inputs Spy (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7F \<rbrakk> |
146 Inputs Spy (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7F \<rbrakk> |
148 \<Longrightarrow> Outpts (Card B) Spy \<lbrace>Nonce Nb, Key K, |
147 \<Longrightarrow> Outpts (Card B) Spy \<lbrace>Nonce Nb, Key K, |
149 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, |
148 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, |
150 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
149 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
151 # evs7F \<in> sr" |
150 # evs7F \<in> sr" |
152 |
151 |
154 |
153 |
155 |
154 |
156 (*B TOWARDS A*) |
155 (*B TOWARDS A*) |
157 (*having sent an input that mentions A is the only memory B relies on, |
156 (*having sent an input that mentions A is the only memory B relies on, |
158 since the output doesn't mention A - lack of explicitness*) |
157 since the output doesn't mention A - lack of explicitness*) |
159 SR8: "\<lbrakk> evs8\<in> sr; |
158 | SR8: "\<lbrakk> evs8\<in> sr; |
160 Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs8; |
159 Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs8; |
161 Outpts (Card B) B \<lbrace>Nonce Nb, Key K, |
160 Outpts (Card B) B \<lbrace>Nonce Nb, Key K, |
162 Cert1, Cert2\<rbrace> \<in> set evs8 \<rbrakk> |
161 Cert1, Cert2\<rbrace> \<in> set evs8 \<rbrakk> |
163 \<Longrightarrow> Says B A \<lbrace>Nonce Nb, Cert1\<rbrace> # evs8 \<in> sr" |
162 \<Longrightarrow> Says B A \<lbrace>Nonce Nb, Cert1\<rbrace> # evs8 \<in> sr" |
164 |
163 |
166 |
165 |
167 |
166 |
168 (*A AND HER CARD*) |
167 (*A AND HER CARD*) |
169 (*A cannot check the form of the verifiers - although I can prove the form of |
168 (*A cannot check the form of the verifiers - although I can prove the form of |
170 Cert2 - and just feeds her card with what she's got*) |
169 Cert2 - and just feeds her card with what she's got*) |
171 SR9: "\<lbrakk> evs9\<in> sr; legalUse(Card A); |
170 | SR9: "\<lbrakk> evs9\<in> sr; legalUse(Card A); |
172 Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs9; |
171 Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs9; |
173 Outpts (Card A) A \<lbrace>Nonce Na, Cert2\<rbrace> \<in> set evs9; |
172 Outpts (Card A) A \<lbrace>Nonce Na, Cert2\<rbrace> \<in> set evs9; |
174 Gets A \<lbrace>Nonce Nb, Cert3\<rbrace> \<in> set evs9; |
173 Gets A \<lbrace>Nonce Nb, Cert3\<rbrace> \<in> set evs9; |
175 \<forall> p q. Cert2 \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk> |
174 \<forall> p q. Cert2 \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk> |
176 \<Longrightarrow> Inputs A (Card A) |
175 \<Longrightarrow> Inputs A (Card A) |
177 \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, |
176 \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, |
178 Cert1, Cert3, Cert2\<rbrace> |
177 Cert1, Cert3, Cert2\<rbrace> |
179 # evs9 \<in> sr" |
178 # evs9 \<in> sr" |
180 |
179 |
181 (*But the card will only give outputs to the inputs of the correct form*) |
180 (*But the card will only give outputs to the inputs of the correct form*) |
182 SR10: "\<lbrakk> evs10\<in> sr; legalUse(Card A); A \<noteq> Server; |
181 | SR10: "\<lbrakk> evs10\<in> sr; legalUse(Card A); A \<noteq> Server; |
183 K = sesK(Nb,pairK(A,B)); |
182 K = sesK(Nb,pairK(A,B)); |
184 Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, |
183 Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, |
185 Nonce (Pairkey(A,B)), |
184 Nonce (Pairkey(A,B)), |
186 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), |
185 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), |
187 Agent B\<rbrace>, |
186 Agent B\<rbrace>, |
191 \<Longrightarrow> Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
190 \<Longrightarrow> Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
192 # evs10 \<in> sr" |
191 # evs10 \<in> sr" |
193 |
192 |
194 (*The card can be exploited by the spy*) |
193 (*The card can be exploited by the spy*) |
195 (*because of the assumptions on the card, A is certainly not server nor spy*) |
194 (*because of the assumptions on the card, A is certainly not server nor spy*) |
196 SR10Fake: "\<lbrakk> evs10F\<in> sr; |
195 | SR10Fake: "\<lbrakk> evs10F\<in> sr; |
197 illegalUse(Card A); |
196 illegalUse(Card A); |
198 K = sesK(Nb,pairK(A,B)); |
197 K = sesK(Nb,pairK(A,B)); |
199 Inputs Spy (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, |
198 Inputs Spy (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, |
200 Nonce (Pairkey(A,B)), |
199 Nonce (Pairkey(A,B)), |
201 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), |
200 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), |
202 Agent B\<rbrace>, |
201 Agent B\<rbrace>, |
203 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, |
202 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, |
204 Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
203 Crypt (crdK (Card A)) (Nonce Na)\<rbrace> |
205 \<in> set evs10F \<rbrakk> |
204 \<in> set evs10F \<rbrakk> |
206 \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
205 \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
207 # evs10F \<in> sr" |
206 # evs10F \<in> sr" |
208 |
207 |
209 |
208 |
210 |
209 |
211 |
210 |
212 (*A TOWARDS B*) |
211 (*A TOWARDS B*) |
213 (*having initiated with B is the only memory A relies on, |
212 (*having initiated with B is the only memory A relies on, |
214 since the output doesn't mention B - lack of explicitness*) |
213 since the output doesn't mention B - lack of explicitness*) |
215 SR11: "\<lbrakk> evs11\<in> sr; |
214 | SR11: "\<lbrakk> evs11\<in> sr; |
216 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs11; |
215 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs11; |
217 Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs11 \<rbrakk> |
216 Outpts (Card A) A \<lbrace>Key K, Certificate\<rbrace> \<in> set evs11 \<rbrakk> |
218 \<Longrightarrow> Says A B (Certificate) |
217 \<Longrightarrow> Says A B (Certificate) |
219 # evs11 \<in> sr" |
218 # evs11 \<in> sr" |
220 |
219 |
221 |
220 |
222 |
221 |
223 (*Both peers may leak by accident the session keys obtained from their |
222 (*Both peers may leak by accident the session keys obtained from their |
224 cards*) |
223 cards*) |
225 Oops1: |
224 | Oops1: |
226 "\<lbrakk> evsO1 \<in> sr; |
225 "\<lbrakk> evsO1 \<in> sr; |
227 Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, |
226 Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, |
228 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evsO1 \<rbrakk> |
227 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evsO1 \<rbrakk> |
229 \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO1 \<in> sr" |
228 \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO1 \<in> sr" |
230 |
229 |
231 Oops2: |
230 | Oops2: |
232 "\<lbrakk> evsO2 \<in> sr; |
231 "\<lbrakk> evsO2 \<in> sr; |
233 Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
232 Outpts (Card A) A \<lbrace>Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> |
234 \<in> set evsO2 \<rbrakk> |
233 \<in> set evsO2 \<rbrakk> |
235 \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO2 \<in> sr" |
234 \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO2 \<in> sr" |
236 |
235 |