135 |
132 |
136 lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'" |
133 lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'" |
137 apply (cut_tac evs = evs in Nonce_supply_lemma) |
134 apply (cut_tac evs = evs in Nonce_supply_lemma) |
138 apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) |
135 apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) |
139 apply (rule_tac x = N in exI) |
136 apply (rule_tac x = N in exI) |
140 apply (rule_tac x = "Suc (N+Na) " in exI) |
137 apply (rule_tac x = "Suc (N+Na)" in exI) |
141 apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
138 apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
142 done |
139 done |
143 |
140 |
144 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & |
141 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & |
145 Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''" |
142 Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''" |
146 apply (cut_tac evs = evs in Nonce_supply_lemma) |
143 apply (cut_tac evs = evs in Nonce_supply_lemma) |
147 apply (cut_tac evs = "evs'" in Nonce_supply_lemma) |
144 apply (cut_tac evs = "evs'" in Nonce_supply_lemma) |
148 apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) |
145 apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) |
149 apply (rule_tac x = N in exI) |
146 apply (rule_tac x = N in exI) |
150 apply (rule_tac x = "Suc (N+Na) " in exI) |
147 apply (rule_tac x = "Suc (N+Na)" in exI) |
151 apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) |
148 apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) |
152 apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
149 apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
153 done |
150 done |
154 |
151 |
155 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
152 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
156 apply (rule Nonce_supply_lemma [THEN exE]) |
153 apply (rule Nonce_supply_lemma [THEN exE]) |
157 apply (rule someI, blast) |
154 apply (rule someI, blast) |
158 done |
155 done |
159 |
156 |
160 subsection{*Supply fresh keys for possibility theorems.*} |
157 text{*Unlike the corresponding property of nonces, we cannot prove |
161 |
158 @{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}. |
162 axioms |
|
163 Key_supply_ax: "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs" |
|
164 --{*Unlike the corresponding property of nonces, this cannot be proved. |
|
165 We have infinitely many agents and there is nothing to stop their |
159 We have infinitely many agents and there is nothing to stop their |
166 long-term keys from exhausting all the natural numbers. The axiom |
160 long-term keys from exhausting all the natural numbers. Instead, |
167 assumes that their keys are dispersed so as to leave room for infinitely |
161 possibility theorems must assume the existence of a few keys.*} |
168 many fresh session keys. We could, alternatively, restrict agents to |
162 |
169 an unspecified finite number. We could however replace @{term"used evs"} |
|
170 by @{term "used []"}.*} |
|
171 |
|
172 lemma Key_supply1: "\<exists>K. Key K \<notin> used evs" |
|
173 by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast) |
|
174 |
|
175 lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'" |
|
176 apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) |
|
177 apply (erule exE) |
|
178 apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) |
|
179 done |
|
180 |
|
181 lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' & |
|
182 Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''" |
|
183 apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) |
|
184 apply (erule exE) |
|
185 (*Blast_tac requires instantiation of the keys for some reason*) |
|
186 apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax]) |
|
187 apply (erule exE) |
|
188 apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K |
|
189 in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast) |
|
190 done |
|
191 |
|
192 lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs" |
|
193 apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE]) |
|
194 apply (rule someI, blast) |
|
195 done |
|
196 |
163 |
197 subsection{*Tactics for possibility theorems*} |
164 subsection{*Tactics for possibility theorems*} |
198 |
165 |
199 ML |
166 ML |
200 {* |
167 {* |
201 val inj_shrK = thm "inj_shrK"; |
168 val inj_shrK = thm "inj_shrK"; |
202 val isSym_keys = thm "isSym_keys"; |
169 val isSym_keys = thm "isSym_keys"; |
203 val Key_supply_ax = thm "Key_supply_ax"; |
|
204 val Key_supply = thm "Key_supply"; |
|
205 val Nonce_supply = thm "Nonce_supply"; |
170 val Nonce_supply = thm "Nonce_supply"; |
206 val invKey_K = thm "invKey_K"; |
171 val invKey_K = thm "invKey_K"; |
207 val analz_Decrypt' = thm "analz_Decrypt'"; |
172 val analz_Decrypt' = thm "analz_Decrypt'"; |
208 val keysFor_parts_initState = thm "keysFor_parts_initState"; |
173 val keysFor_parts_initState = thm "keysFor_parts_initState"; |
209 val keysFor_parts_insert = thm "keysFor_parts_insert"; |
174 val keysFor_parts_insert = thm "keysFor_parts_insert"; |