1.1 --- a/src/HOL/Auth/CertifiedEmail.thy Fri Aug 08 15:05:11 2003 +0200
1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy Tue Aug 12 13:35:03 2003 +0200
1.3 @@ -39,12 +39,12 @@
1.4
1.5 Fake: --{*The Spy may say anything he can say. The sender field is correct,
1.6 but agents don't use that information.*}
1.7 - "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|]
1.8 + "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|]
1.9 ==> Says Spy B X # evsf \<in> certified_mail"
1.10
1.11 FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
1.12 equipped with the necessary credentials to serve as an SSL server.*}
1.13 - "[| evsfssl \<in> certified_mail; X \<in> synth(analz(knows Spy evsfssl))|]
1.14 + "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
1.15 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
1.16
1.17 CM1: --{*The sender approaches the recipient. The message is a number.*}
1.18 @@ -89,6 +89,9 @@
1.19 ==> Gets B X#evsr \<in> certified_mail"
1.20
1.21
1.22 +declare Says_imp_knows_Spy [THEN analz.Inj, dest]
1.23 +declare analz_into_parts [dest]
1.24 +
1.25 (*A "possibility property": there are traces that reach the end*)
1.26 lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
1.27 Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
1.28 @@ -118,7 +121,7 @@
1.29 "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext,
1.30 Nonce q, S2TTP|} \<in> set evs;
1.31 evs \<in> certified_mail|]
1.32 - ==> S2TTP \<in> analz(knows Spy evs)"
1.33 + ==> S2TTP \<in> analz(spies evs)"
1.34 apply (drule Gets_imp_Says, simp)
1.35 apply (blast dest: Says_imp_knows_Spy analz.Inj)
1.36 done
1.37 @@ -128,7 +131,7 @@
1.38
1.39 lemma hr_form_lemma [rule_format]:
1.40 "evs \<in> certified_mail
1.41 - ==> hr \<notin> synth (analz (knows Spy evs)) -->
1.42 + ==> hr \<notin> synth (analz (spies evs)) -->
1.43 (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
1.44 \<in> set evs -->
1.45 (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
1.46 @@ -142,39 +145,39 @@
1.47 lemma hr_form:
1.48 "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
1.49 evs \<in> certified_mail|]
1.50 - ==> hr \<in> synth (analz (knows Spy evs)) |
1.51 + ==> hr \<in> synth (analz (spies evs)) |
1.52 (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
1.53 by (blast intro: hr_form_lemma)
1.54
1.55 -lemma Spy_dont_know_private_keys [rule_format]:
1.56 - "evs \<in> certified_mail
1.57 - ==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad"
1.58 +lemma Spy_dont_know_private_keys [dest!]:
1.59 + "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
1.60 + ==> A \<in> bad"
1.61 +apply (erule rev_mp)
1.62 apply (erule certified_mail.induct, simp_all)
1.63 txt{*Fake*}
1.64 -apply (blast dest: Fake_parts_insert[THEN subsetD]
1.65 - analz_subset_parts[THEN subsetD])
1.66 +apply (blast dest: Fake_parts_insert_in_Un);
1.67 txt{*Message 1*}
1.68 apply blast
1.69 txt{*Message 3*}
1.70 apply (frule_tac hr_form, assumption)
1.71 apply (elim disjE exE)
1.72 apply (simp_all add: parts_insert2)
1.73 - apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
1.74 - analz_subset_parts[THEN subsetD], blast)
1.75 + apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
1.76 + analz_subset_parts [THEN subsetD], blast)
1.77 done
1.78
1.79 lemma Spy_know_private_keys_iff [simp]:
1.80 "evs \<in> certified_mail
1.81 ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
1.82 -by (blast intro: Spy_dont_know_private_keys parts.Inj)
1.83 +by (blast intro: elim:);
1.84
1.85 lemma Spy_dont_know_TTPKey_parts [simp]:
1.86 - "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)"
1.87 + "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)"
1.88 by simp
1.89
1.90 lemma Spy_dont_know_TTPKey_analz [simp]:
1.91 - "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)"
1.92 -by (force dest!: analz_subset_parts[THEN subsetD])
1.93 + "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
1.94 +by auto
1.95
1.96 text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
1.97 belonging to @{term TTP}*}
1.98 @@ -192,10 +195,9 @@
1.99 apply (erule certified_mail.induct, simp_all)
1.100 apply (blast intro:parts_insertI)
1.101 txt{*Fake SSL*}
1.102 -apply (blast dest: analz_subset_parts[THEN subsetD] parts.Body)
1.103 +apply (blast dest: parts.Body)
1.104 txt{*Message 2*}
1.105 -apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says
1.106 - elim!: knows_Spy_partsEs)
1.107 +apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
1.108 txt{*Message 3*}
1.109 apply (frule_tac hr_form, assumption)
1.110 apply (elim disjE exE)
1.111 @@ -207,8 +209,7 @@
1.112 "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
1.113 apply (erule certified_mail.induct, simp_all)
1.114 txt{*Fake*}
1.115 -apply (blast dest: Fake_parts_insert[THEN subsetD]
1.116 - analz_subset_parts[THEN subsetD])
1.117 +apply (blast dest: Fake_parts_insert_in_Un);
1.118 txt{*Message 1*}
1.119 apply blast
1.120 txt{*Message 3*}
1.121 @@ -216,18 +217,18 @@
1.122 apply (frule_tac hr_form, assumption)
1.123 apply (elim disjE exE)
1.124 apply (simp_all add: parts_insert2)
1.125 -apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
1.126 - analz_subset_parts[THEN subsetD])
1.127 +apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
1.128 + analz_subset_parts [THEN subsetD])
1.129 done
1.130
1.131
1.132 lemma Spy_know_RPwd_iff [simp]:
1.133 - "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)"
1.134 + "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)"
1.135 by (auto simp add: Spy_dont_know_RPwd)
1.136
1.137 lemma Spy_analz_RPwd_iff [simp]:
1.138 - "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>bad)"
1.139 -by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts[THEN subsetD]])
1.140 + "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
1.141 +by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
1.142
1.143
1.144 text{*Unused, but a guarantee of sorts*}
1.145 @@ -237,16 +238,15 @@
1.146 apply (erule rev_mp)
1.147 apply (erule certified_mail.induct, simp_all)
1.148 txt{*Fake*}
1.149 -apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert[THEN subsetD]
1.150 - analz_subset_parts[THEN subsetD])
1.151 +apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
1.152 txt{*Message 1*}
1.153 apply blast
1.154 txt{*Message 3*}
1.155 apply (frule_tac hr_form, assumption)
1.156 apply (elim disjE exE)
1.157 -apply (simp_all add: parts_insert2)
1.158 -apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
1.159 - analz_subset_parts[THEN subsetD], blast)
1.160 +apply (simp_all add: parts_insert2 parts_insert_knows_A)
1.161 + apply (blast dest!: Fake_parts_sing_imp_Un)
1.162 +apply (blast intro: elim:);
1.163 done
1.164
1.165
1.166 @@ -255,8 +255,8 @@
1.167 lemma analz_image_freshK [rule_format]:
1.168 "evs \<in> certified_mail ==>
1.169 \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
1.170 - (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
1.171 - (K \<in> KK | Key K \<in> analz (knows Spy evs))"
1.172 + (Key K \<in> analz (Key`KK Un (spies evs))) =
1.173 + (K \<in> KK | Key K \<in> analz (spies evs))"
1.174 apply (erule certified_mail.induct)
1.175 apply (drule_tac [6] A=TTP in symKey_neq_priEK)
1.176 apply (erule_tac [6] disjE [OF hr_form])
1.177 @@ -272,8 +272,8 @@
1.178
1.179 lemma analz_insert_freshK:
1.180 "[| evs \<in> certified_mail; KAB \<noteq> invKey (pubEK TTP) |] ==>
1.181 - (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
1.182 - (K = KAB | Key K \<in> analz (knows Spy evs))"
1.183 + (Key K \<in> analz (insert (Key KAB) (spies evs))) =
1.184 + (K = KAB | Key K \<in> analz (spies evs))"
1.185 by (simp only: analz_image_freshK analz_image_freshK_simps)
1.186
1.187 text{*@{term S2TTP} must have originated from a valid sender
1.188 @@ -284,11 +284,11 @@
1.189 by (blast dest!: Notes_imp_used)
1.190
1.191
1.192 -(*The weaker version, replacing "used evs" by "parts (knows Spy evs)",
1.193 +(*The weaker version, replacing "used evs" by "parts (spies evs)",
1.194 isn't inductive: message 3 case can't be proved *)
1.195 lemma S2TTP_sender_lemma [rule_format]:
1.196 "evs \<in> certified_mail ==>
1.197 - Key K \<notin> analz (knows Spy evs) -->
1.198 + Key K \<notin> analz (spies evs) -->
1.199 (\<forall>AO. Crypt (pubEK TTP)
1.200 {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
1.201 (\<exists>m ctxt q.
1.202 @@ -302,11 +302,11 @@
1.203 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
1.204 apply (simp add: used_Nil Crypt_notin_initState, simp_all)
1.205 txt{*Fake*}
1.206 -apply (blast dest: Fake_parts_sing[THEN subsetD]
1.207 - dest!: analz_subset_parts[THEN subsetD])
1.208 +apply (blast dest: Fake_parts_sing [THEN subsetD]
1.209 + dest!: analz_subset_parts [THEN subsetD])
1.210 txt{*Fake SSL*}
1.211 -apply (blast dest: Fake_parts_sing[THEN subsetD]
1.212 - dest: analz_subset_parts[THEN subsetD])
1.213 +apply (blast dest: Fake_parts_sing [THEN subsetD]
1.214 + dest: analz_subset_parts [THEN subsetD])
1.215 txt{*Message 1*}
1.216 apply (clarsimp, blast)
1.217 txt{*Message 2*}
1.218 @@ -319,7 +319,7 @@
1.219
1.220 lemma S2TTP_sender:
1.221 "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
1.222 - Key K \<notin> analz (knows Spy evs);
1.223 + Key K \<notin> analz (spies evs);
1.224 evs \<in> certified_mail|]
1.225 ==> \<exists>m ctxt q.
1.226 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
1.227 @@ -353,7 +353,7 @@
1.228 where @{term K} is secure.*}
1.229 lemma Key_unique_lemma [rule_format]:
1.230 "evs \<in> certified_mail ==>
1.231 - Key K \<notin> analz (knows Spy evs) -->
1.232 + Key K \<notin> analz (spies evs) -->
1.233 (\<forall>m cleartext q hs.
1.234 Says S R
1.235 {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
1.236 @@ -367,10 +367,11 @@
1.237 Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
1.238 \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))"
1.239 apply (erule certified_mail.induct, analz_mono_contra, simp_all)
1.240 -txt{*Fake*}
1.241 -apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD])
1.242 -txt{*Message 1*}
1.243 -apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
1.244 + prefer 2
1.245 + txt{*Message 1*}
1.246 + apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
1.247 +txt{*Fake*}
1.248 +apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD])
1.249 done
1.250
1.251 text{*The key determines the sender, recipient and protocol options.*}
1.252 @@ -385,7 +386,7 @@
1.253 Number cleartext', Nonce q',
1.254 Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
1.255 \<in> set evs;
1.256 - Key K \<notin> analz (knows Spy evs);
1.257 + Key K \<notin> analz (spies evs);
1.258 evs \<in> certified_mail|]
1.259 ==> R' = R & S' = S & AO' = AO & hs' = hs"
1.260 by (rule Key_unique_lemma, assumption+)
1.261 @@ -400,7 +401,7 @@
1.262 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
1.263 Number cleartext, Nonce q, S2TTP|} \<in> set evs;
1.264 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
1.265 - Key K \<in> analz(knows Spy evs);
1.266 + Key K \<in> analz(spies evs);
1.267 evs \<in> certified_mail;
1.268 S\<noteq>Spy|]
1.269 ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
1.270 @@ -430,7 +431,7 @@
1.271 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
1.272 evs \<in> certified_mail;
1.273 S\<noteq>Spy; R \<notin> bad|]
1.274 - ==> Key K \<notin> analz(knows Spy evs)"
1.275 + ==> Key K \<notin> analz(spies evs)"
1.276 by (blast dest: Spy_see_encrypted_key_imp)
1.277
1.278
1.279 @@ -471,19 +472,19 @@
1.280 apply (erule ssubst)
1.281 apply (erule certified_mail.induct, simp_all)
1.282 txt{*Fake*}
1.283 -apply (blast dest: Fake_parts_sing[THEN subsetD]
1.284 - dest!: analz_subset_parts[THEN subsetD])
1.285 +apply (blast dest: Fake_parts_sing [THEN subsetD]
1.286 + dest!: analz_subset_parts [THEN subsetD])
1.287 txt{*Fake SSL*}
1.288 -apply (blast dest: Fake_parts_sing[THEN subsetD]
1.289 - dest!: analz_subset_parts[THEN subsetD])
1.290 +apply (blast dest: Fake_parts_sing [THEN subsetD]
1.291 + dest!: analz_subset_parts [THEN subsetD])
1.292 txt{*Message 2*}
1.293 apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
1.294 apply (force dest: parts_cut)
1.295 txt{*Message 3*}
1.296 apply (frule_tac hr_form, assumption)
1.297 apply (elim disjE exE, simp_all)
1.298 -apply (blast dest: Fake_parts_sing[THEN subsetD]
1.299 - dest!: analz_subset_parts[THEN subsetD])
1.300 +apply (blast dest: Fake_parts_sing [THEN subsetD]
1.301 + dest!: analz_subset_parts [THEN subsetD])
1.302 done
1.303
1.304 end
2.1 --- a/src/HOL/Auth/Message.thy Fri Aug 08 15:05:11 2003 +0200
2.2 +++ b/src/HOL/Auth/Message.thy Tue Aug 12 13:35:03 2003 +0200
2.3 @@ -683,10 +683,10 @@
2.4 done
2.5
2.6 lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
2.7 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
2.8 +by (blast intro: analz_subset_parts [THEN subsetD])
2.9
2.10 lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
2.11 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
2.12 +by (blast intro: analz_subset_parts [THEN subsetD])
2.13
2.14 (*Without this equation, other rules for synth and analz would yield
2.15 redundant cases*)
2.16 @@ -994,6 +994,8 @@
2.17 apply (simp add: parts_mono)
2.18 done
2.19
2.20 +lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
2.21 +
2.22 method_setup spy_analz = {*
2.23 Method.ctxt_args (fn ctxt =>
2.24 Method.METHOD (fn facts =>
3.1 --- a/src/HOL/Auth/ROOT.ML Fri Aug 08 15:05:11 2003 +0200
3.2 +++ b/src/HOL/Auth/ROOT.ML Tue Aug 12 13:35:03 2003 +0200
3.3 @@ -21,6 +21,8 @@
3.4 time_use_thy "Yahalom";
3.5 time_use_thy "Yahalom2";
3.6 time_use_thy "Yahalom_Bad";
3.7 +time_use_thy "ZhouGollmann";
3.8 +
3.9
3.10 (*Public-key protocols*)
3.11 time_use_thy "NS_Public_Bad";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Auth/ZhouGollmann.thy Tue Aug 12 13:35:03 2003 +0200
4.3 @@ -0,0 +1,463 @@
4.4 +(* Title: HOL/Auth/ZhouGollmann
4.5 + ID: $Id$
4.6 + Author: Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
4.7 + Copyright 2003 University of Cambridge
4.8 +
4.9 +The protocol of
4.10 + Jianying Zhou and Dieter Gollmann,
4.11 + A Fair Non-Repudiation Protocol,
4.12 + Security and Privacy 1996 (Oakland)
4.13 + 55-61
4.14 +*)
4.15 +
4.16 +theory ZhouGollmann = Public:
4.17 +
4.18 +syntax
4.19 + TTP :: agent
4.20 +
4.21 +translations
4.22 + "TTP" == "Server"
4.23 +
4.24 +syntax
4.25 + f_sub :: nat
4.26 + f_nro :: nat
4.27 + f_nrr :: nat
4.28 + f_con :: nat
4.29 +
4.30 +translations
4.31 + "f_sub" == "5"
4.32 + "f_nro" == "2"
4.33 + "f_nrr" == "3"
4.34 + "f_con" == "4"
4.35 +
4.36 +
4.37 +constdefs
4.38 + broken :: "agent set"
4.39 + --{*the compromised honest agents; TTP is included as it's not allowed to
4.40 + use the protocol*}
4.41 + "broken == insert TTP (bad - {Spy})"
4.42 +
4.43 +declare broken_def [simp]
4.44 +
4.45 +consts zg :: "event list set"
4.46 +
4.47 +inductive zg
4.48 + intros
4.49 +
4.50 + Nil: "[] \<in> zg"
4.51 +
4.52 + Fake: "[| evsf \<in> zg; X \<in> synth (analz (spies evsf)) |]
4.53 + ==> Says Spy B X # evsf \<in> zg"
4.54 +
4.55 +Reception: "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |]
4.56 + ==> Gets B X # evsr \<in> zg"
4.57 +
4.58 + (*L is fresh for honest agents.
4.59 + We don't require K to be fresh because we don't bother to prove secrecy!
4.60 + We just assume that the protocol's objective is to deliver K fairly,
4.61 + rather than to keep M secret.*)
4.62 + ZG1: "[| evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m);
4.63 + K \<in> symKeys;
4.64 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
4.65 + ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
4.66 +
4.67 + (*B must check that NRO is A's signature to learn the sender's name*)
4.68 + ZG2: "[| evs2 \<in> zg;
4.69 + Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
4.70 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
4.71 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
4.72 + ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2 \<in> zg"
4.73 +
4.74 + (*K is symmetric must be repeated IF there's spy*)
4.75 + (*A must check that NRR is B's signature to learn the sender's name*)
4.76 + (*without spy, the matching label would be enough*)
4.77 + ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
4.78 + Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
4.79 + Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
4.80 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
4.81 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
4.82 + ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
4.83 + # evs3 \<in> zg"
4.84 +
4.85 + (*TTP checks that sub_K is A's signature to learn who issued K, then
4.86 + gives credentials to A and B. The Notes event models the availability of
4.87 + the credentials, but the act of fetching them is not modelled.*)
4.88 + (*Also said TTP_prepare_ftp*)
4.89 + ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
4.90 + Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
4.91 + \<in> set evs4;
4.92 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.93 + con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
4.94 + Nonce L, Key K|}|]
4.95 + ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
4.96 + # evs4 \<in> zg"
4.97 +
4.98 +
4.99 +declare Says_imp_knows_Spy [THEN analz.Inj, dest]
4.100 +declare Fake_parts_insert_in_Un [dest]
4.101 +declare analz_into_parts [dest]
4.102 +
4.103 +declare symKey_neq_priEK [simp]
4.104 +declare symKey_neq_priEK [THEN not_sym, simp]
4.105 +
4.106 +
4.107 +subsection {*Basic Lemmas*}
4.108 +
4.109 +lemma Gets_imp_Says:
4.110 + "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
4.111 +apply (erule rev_mp)
4.112 +apply (erule zg.induct, auto)
4.113 +done
4.114 +
4.115 +lemma Gets_imp_knows_Spy:
4.116 + "[| Gets B X \<in> set evs; evs \<in> zg |] ==> X \<in> spies evs"
4.117 +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
4.118 +
4.119 +
4.120 +text{*Lets us replace proofs about @{term "used evs"} by simpler proofs
4.121 +about @{term "parts (spies evs)"}.*}
4.122 +lemma Crypt_used_imp_spies:
4.123 + "[| Crypt K X \<in> used evs; K \<noteq> priK TTP; evs \<in> zg |]
4.124 + ==> Crypt K X \<in> parts (spies evs)"
4.125 +apply (erule rev_mp)
4.126 +apply (erule zg.induct)
4.127 +apply (simp_all add: parts_insert_knows_A)
4.128 +done
4.129 +
4.130 +lemma Notes_TTP_imp_Gets:
4.131 + "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
4.132 + \<in> set evs;
4.133 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.134 + evs \<in> zg|]
4.135 + ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
4.136 +apply (erule rev_mp)
4.137 +apply (erule zg.induct, auto)
4.138 +done
4.139 +
4.140 +text{*For reasoning about C, which is encrypted in message ZG2*}
4.141 +lemma ZG2_msg_in_parts_spies:
4.142 + "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
4.143 + ==> C \<in> parts (spies evs)"
4.144 +by (blast dest: Gets_imp_Says)
4.145 +
4.146 +(*classical regularity lemma on priK*)
4.147 +lemma Spy_see_priK [simp]:
4.148 + "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
4.149 +apply (erule zg.induct)
4.150 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
4.151 +done
4.152 +
4.153 +text{*So that blast can use it too*}
4.154 +declare Spy_see_priK [THEN [2] rev_iffD1, dest!]
4.155 +
4.156 +lemma Spy_analz_priK [simp]:
4.157 + "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
4.158 +by auto
4.159 +
4.160 +
4.161 +subsection{*About NRO*}
4.162 +
4.163 +text{*Below we prove that if @{term NRO} exists then @{term A} definitely
4.164 +sent it, provided @{term A} is not broken. *}
4.165 +
4.166 +text{*Strong conclusion for a good agent*}
4.167 +lemma NRO_authenticity_good:
4.168 + "[| NRO \<in> parts (spies evs);
4.169 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
4.170 + A \<notin> bad; evs \<in> zg |]
4.171 + ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
4.172 +apply clarify
4.173 +apply (erule rev_mp)
4.174 +apply (erule zg.induct)
4.175 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
4.176 +done
4.177 +
4.178 +text{*A compromised agent: we can't be sure whether A or the Spy sends the
4.179 +message or of the precise form of the message*}
4.180 +lemma NRO_authenticity_bad:
4.181 + "[| NRO \<in> parts (spies evs);
4.182 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
4.183 + A \<in> bad; evs \<in> zg |]
4.184 + ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
4.185 +apply clarify
4.186 +apply (erule rev_mp)
4.187 +apply (erule zg.induct)
4.188 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.189 +txt{*ZG3*}
4.190 + prefer 4 apply blast
4.191 +txt{*ZG2*}
4.192 + prefer 3 apply blast
4.193 +txt{*Fake*}
4.194 +apply (simp add: parts_insert_knows_A, blast)
4.195 +txt{*ZG1*}
4.196 +apply (auto intro!: exI)
4.197 +done
4.198 +
4.199 +theorem NRO_authenticity:
4.200 + "[| NRO \<in> used evs;
4.201 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
4.202 + A \<notin> broken; evs \<in> zg |]
4.203 + ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
4.204 +apply auto
4.205 + apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
4.206 +apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
4.207 +done
4.208 +
4.209 +
4.210 +subsection{*About NRR*}
4.211 +
4.212 +text{*Below we prove that if @{term NRR} exists then @{term B} definitely
4.213 +sent it, provided @{term B} is not broken.*}
4.214 +
4.215 +text{*Strong conclusion for a good agent*}
4.216 +lemma NRR_authenticity_good:
4.217 + "[| NRR \<in> parts (spies evs);
4.218 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
4.219 + B \<notin> bad; evs \<in> zg |]
4.220 + ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
4.221 +apply clarify
4.222 +apply (erule rev_mp)
4.223 +apply (erule zg.induct)
4.224 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
4.225 +done
4.226 +
4.227 +lemma NRR_authenticity_bad:
4.228 + "[| NRR \<in> parts (spies evs);
4.229 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
4.230 + B \<in> bad; evs \<in> zg |]
4.231 + ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
4.232 +apply clarify
4.233 +apply (erule rev_mp)
4.234 +apply (erule zg.induct)
4.235 +apply (frule_tac [5] ZG2_msg_in_parts_spies)
4.236 +apply (simp_all del: bex_simps)
4.237 +txt{*ZG3*}
4.238 + prefer 4 apply blast
4.239 +txt{*Fake*}
4.240 +apply (simp add: parts_insert_knows_A, blast)
4.241 +txt{*ZG1*}
4.242 +apply (auto simp del: bex_simps)
4.243 +txt{*ZG2*}
4.244 +apply (force intro!: exI)
4.245 +done
4.246 +
4.247 +theorem NRR_authenticity:
4.248 + "[| NRR \<in> used evs;
4.249 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
4.250 + B \<notin> broken; evs \<in> zg |]
4.251 + ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
4.252 +apply auto
4.253 + apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
4.254 +apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
4.255 +done
4.256 +
4.257 +
4.258 +subsection{*Proofs About @{term sub_K}*}
4.259 +
4.260 +text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
4.261 +sent it, provided @{term A} is not broken. *}
4.262 +
4.263 +text{*Strong conclusion for a good agent*}
4.264 +lemma sub_K_authenticity_good:
4.265 + "[| sub_K \<in> parts (spies evs);
4.266 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.267 + A \<notin> bad; evs \<in> zg |]
4.268 + ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
4.269 +apply (erule rev_mp)
4.270 +apply (erule zg.induct)
4.271 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.272 +txt{*Fake*}
4.273 +apply (blast dest!: Fake_parts_sing_imp_Un)
4.274 +done
4.275 +
4.276 +text{*A compromised agent: we can't be sure whether A or the Spy sends the
4.277 +message or of the precise form of the message*}
4.278 +lemma sub_K_authenticity_bad:
4.279 + "[| sub_K \<in> parts (spies evs);
4.280 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.281 + A \<in> bad; evs \<in> zg |]
4.282 + ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
4.283 +apply clarify
4.284 +apply (erule rev_mp)
4.285 +apply (erule zg.induct)
4.286 +apply (frule_tac [5] ZG2_msg_in_parts_spies)
4.287 +apply (simp_all del: bex_simps)
4.288 +txt{*Fake*}
4.289 +apply (simp add: parts_insert_knows_A, blast)
4.290 +txt{*ZG1*}
4.291 +apply (auto simp del: bex_simps)
4.292 +txt{*ZG3*}
4.293 +apply (force intro!: exI)
4.294 +done
4.295 +
4.296 +theorem sub_K_authenticity:
4.297 + "[| sub_K \<in> used evs;
4.298 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.299 + A \<notin> broken; evs \<in> zg |]
4.300 + ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
4.301 +apply auto
4.302 + apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
4.303 +apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
4.304 +done
4.305 +
4.306 +
4.307 +subsection{*Proofs About @{term con_K}*}
4.308 +
4.309 +text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
4.310 +and therefore @{term A} and @{term B}) can get it too. Moreover, we know
4.311 +that @{term A} sent @{term sub_K}*}
4.312 +
4.313 +lemma con_K_authenticity:
4.314 + "[|con_K \<in> used evs;
4.315 + con_K = Crypt (priK TTP)
4.316 + {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
4.317 + evs \<in> zg |]
4.318 + ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
4.319 + \<in> set evs"
4.320 +apply clarify
4.321 +apply (erule rev_mp)
4.322 +apply (erule zg.induct)
4.323 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.324 +txt{*Fake*}
4.325 +apply (blast dest!: Fake_parts_sing_imp_Un)
4.326 +txt{*ZG2*}
4.327 +apply (blast dest: parts_cut)
4.328 +done
4.329 +
4.330 +text{*If @{term TTP} holds @{term con_K} then @{term A} sent
4.331 + @{term sub_K}. We assume that @{term A} is not broken. Nothing needs to
4.332 + be assumed about the form of @{term con_K}!*}
4.333 +lemma Notes_TTP_imp_Says_A:
4.334 + "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
4.335 + \<in> set evs;
4.336 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.337 + A \<notin> broken; evs \<in> zg|]
4.338 + ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
4.339 +by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
4.340 +
4.341 +text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
4.342 +theorem B_sub_K_authenticity:
4.343 + "[|con_K \<in> used evs;
4.344 + con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
4.345 + Nonce L, Key K|};
4.346 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.347 + A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
4.348 + ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
4.349 +by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
4.350 +
4.351 +
4.352 +subsection{*Proving fairness*}
4.353 +
4.354 +text{*Cannot prove that, if @{term B} has NRO, then @{term A} has her NRR.
4.355 +It would appear that @{term B} has a small advantage, though it is
4.356 +useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
4.357 +
4.358 +text{*Strange: unicity of the label protects @{term A}?*}
4.359 +lemma A_unicity:
4.360 + "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
4.361 + NRO \<in> parts (spies evs);
4.362 + Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
4.363 + \<in> set evs;
4.364 + A \<notin> bad; evs \<in> zg |]
4.365 + ==> M'=M"
4.366 +apply clarify
4.367 +apply (erule rev_mp)
4.368 +apply (erule rev_mp)
4.369 +apply (erule zg.induct)
4.370 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
4.371 +txt{*ZG1: freshness*}
4.372 +apply (blast dest: parts.Body)
4.373 +done
4.374 +
4.375 +
4.376 +text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds
4.377 +NRR. Relies on unicity of labels.*}
4.378 +lemma sub_K_implies_NRR:
4.379 + "[| sub_K \<in> parts (spies evs);
4.380 + NRO \<in> parts (spies evs);
4.381 + sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
4.382 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
4.383 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
4.384 + A \<notin> bad; evs \<in> zg |]
4.385 + ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
4.386 +apply clarify
4.387 +apply (erule rev_mp)
4.388 +apply (erule rev_mp)
4.389 +apply (erule zg.induct)
4.390 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.391 +txt{*Fake*}
4.392 +apply blast
4.393 +txt{*ZG1: freshness*}
4.394 +apply (blast dest: parts.Body)
4.395 +txt{*ZG3*}
4.396 +apply (blast dest: A_unicity [OF refl])
4.397 +done
4.398 +
4.399 +
4.400 +lemma Crypt_used_imp_L_used:
4.401 + "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
4.402 + ==> L \<in> used evs"
4.403 +apply (erule rev_mp)
4.404 +apply (erule zg.induct, auto)
4.405 +txt{*Fake*}
4.406 +apply (blast dest!: Fake_parts_sing_imp_Un)
4.407 +txt{*ZG2: freshness*}
4.408 +apply (blast dest: parts.Body)
4.409 +done
4.410 +
4.411 +
4.412 +text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist,
4.413 +then @{term A} holds NRR. @{term A} must be uncompromised, but there is no
4.414 +assumption about @{term B}.*}
4.415 +theorem A_fairness_NRO:
4.416 + "[|con_K \<in> used evs;
4.417 + NRO \<in> parts (spies evs);
4.418 + con_K = Crypt (priK TTP)
4.419 + {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
4.420 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
4.421 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
4.422 + A \<notin> bad; evs \<in> zg |]
4.423 + ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
4.424 +apply clarify
4.425 +apply (erule rev_mp)
4.426 +apply (erule rev_mp)
4.427 +apply (erule zg.induct)
4.428 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.429 + txt{*Fake*}
4.430 + apply (simp add: parts_insert_knows_A)
4.431 + apply (blast dest: Fake_parts_sing_imp_Un)
4.432 + txt{*ZG1*}
4.433 + apply (blast dest: Crypt_used_imp_L_used)
4.434 + txt{*ZG2*}
4.435 + apply (blast dest: parts_cut)
4.436 +txt{*ZG4*}
4.437 +apply (blast intro: sub_K_implies_NRR [OF _ _ refl]
4.438 + dest: Gets_imp_knows_Spy [THEN parts.Inj])
4.439 +done
4.440 +
4.441 +text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
4.442 +@{term B} must be uncompromised, but there is no assumption about @{term
4.443 +A}. *}
4.444 +theorem B_fairness_NRR:
4.445 + "[|NRR \<in> used evs;
4.446 + NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
4.447 + NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
4.448 + B \<notin> bad; evs \<in> zg |]
4.449 + ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
4.450 +apply clarify
4.451 +apply (erule rev_mp)
4.452 +apply (erule zg.induct)
4.453 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
4.454 +txt{*Fake*}
4.455 +apply (blast dest!: Fake_parts_sing_imp_Un)
4.456 +txt{*ZG2*}
4.457 +apply (blast dest: parts_cut)
4.458 +done
4.459 +
4.460 +
4.461 +text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
4.462 +con_K_authenticity}. Cannot conclude that also NRO is available to @{term B},
4.463 +because if @{term A} were unfair, @{term A} could build message 3 without
4.464 +building message 1, which contains NRO. *}
4.465 +
4.466 +end
5.1 --- a/src/HOL/IsaMakefile Fri Aug 08 15:05:11 2003 +0200
5.2 +++ b/src/HOL/IsaMakefile Tue Aug 12 13:35:03 2003 +0200
5.3 @@ -361,9 +361,9 @@
5.4 Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
5.5 Auth/Recur.thy Auth/Shared.thy \
5.6 Auth/TLS.thy Auth/WooLam.thy \
5.7 - Auth/Kerberos_BAN.thy \
5.8 - Auth/KerberosIV.ML Auth/KerberosIV.thy \
5.9 + Auth/Kerberos_BAN.thy Auth/KerberosIV.ML Auth/KerberosIV.thy \
5.10 Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
5.11 + Auth/ZhouGollmann.thy \
5.12 Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
5.13 Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
5.14 Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \