1.1 --- a/src/HOL/Auth/KerberosIV.ML Tue Mar 13 18:35:48 2001 +0100
1.2 +++ b/src/HOL/Auth/KerberosIV.ML Wed Mar 14 08:50:55 2001 +0100
1.3 @@ -185,8 +185,8 @@
1.4 qed_spec_mp "new_keys_not_used";
1.5 Addsimps [new_keys_not_used];
1.6
1.7 -(*Earlier, \\<forall>protocol proofs declared this theorem.
1.8 - But Yahalom and Kerberos IV are the only ones that need it!*)
1.9 +(*Earlier, all protocol proofs declared this theorem.
1.10 + But few of them actually need it! (Another is Yahalom) *)
1.11 bind_thm ("new_keys_not_analzd",
1.12 [analz_subset_parts RS keysFor_mono,
1.13 new_keys_not_used] MRS contra_subsetD);
1.14 @@ -492,7 +492,7 @@
1.15 by (blast_tac (claset() addSEs spies_partsEs) 1);
1.16 qed "Serv_fresh_not_KeyCryptKey";
1.17
1.18 -Goalw [KeyCryptKey_def]
1.19 +Goal
1.20 "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
1.21 \ \\<in> parts (spies evs); evs \\<in> kerberos |] \
1.22 \ ==> ~ KeyCryptKey K AuthKey evs";
1.23 @@ -501,24 +501,23 @@
1.24 (*K4*)
1.25 by (blast_tac (claset() addEs spies_partsEs) 3);
1.26 (*K2: by freshness*)
1.27 +by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2);
1.28 by (blast_tac (claset() addEs spies_partsEs) 2);
1.29 by (Fake_parts_insert_tac 1);
1.30 qed "AuthKey_not_KeyCryptKey";
1.31
1.32 (*A secure serverkey cannot have been used to encrypt others*)
1.33 -Goalw [KeyCryptKey_def]
1.34 - "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} \
1.35 -\ \\<in> parts (spies evs); \
1.36 -\ Key ServKey \\<notin> analz (spies evs); \
1.37 -\ B \\<noteq> Tgs; evs \\<in> kerberos |] \
1.38 -\ ==> ~ KeyCryptKey ServKey K evs";
1.39 +Goal
1.40 + "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
1.41 +\ Key SK \\<notin> analz (spies evs); \
1.42 +\ B \\<noteq> Tgs; evs \\<in> kerberos |] \
1.43 +\ ==> ~ KeyCryptKey SK K evs";
1.44 by (etac rev_mp 1);
1.45 by (etac rev_mp 1);
1.46 by (parts_induct_tac 1);
1.47 by (Fake_parts_insert_tac 1);
1.48 (*K4 splits into distinct subcases*)
1.49 -by (Step_tac 1);
1.50 -by (ALLGOALS Asm_full_simp_tac);
1.51 +by Auto_tac;
1.52 (*ServKey can't have been enclosed in two certificates*)
1.53 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
1.54 addSEs [MPair_parts]
1.55 @@ -526,7 +525,7 @@
1.56 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
1.57 by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
1.58 Crypt_imp_invKey_keysFor],
1.59 - simpset()) 2);
1.60 + simpset() addsimps [KeyCryptKey_def]) 2);
1.61 (*Others by freshness*)
1.62 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
1.63 qed "ServKey_not_KeyCryptKey";
1.64 @@ -610,11 +609,6 @@
1.65 REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
1.66 ORELSE' hyp_subst_tac)];
1.67
1.68 -Goal "[| KK <= -(range shrK); Key K \\<in> analz (spies evs); evs \\<in> kerberos |] \
1.69 -\ ==> Key K \\<in> analz (Key ` KK Un spies evs)";
1.70 -by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
1.71 -qed "analz_mono_KK";
1.72 -
1.73 (*For the Oops2 case of the next theorem*)
1.74 Goal "[| evs \\<in> kerberos; \
1.75 \ Says Tgs A (Crypt AuthKey \
2.1 --- a/src/HOL/Auth/OtwayRees.ML Tue Mar 13 18:35:48 2001 +0100
2.2 +++ b/src/HOL/Auth/OtwayRees.ML Wed Mar 14 08:50:55 2001 +0100
2.3 @@ -17,10 +17,10 @@
2.4
2.5
2.6 (*A "possibility property": there are traces that reach the end*)
2.7 -Goal "B ~= Server \
2.8 +Goal "B \\<noteq> Server \
2.9 \ ==> \\<exists>NA K. \\<exists>evs \\<in> otway. \
2.10 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
2.11 -\ : set evs";
2.12 +\ \\<in> set evs";
2.13 by (REPEAT (resolve_tac [exI,bexI] 1));
2.14 by (rtac (otway.Nil RS
2.15 otway.OR1 RS otway.Reception RS
2.16 @@ -29,14 +29,14 @@
2.17 by possibility_tac;
2.18 result();
2.19
2.20 -Goal "[| Gets B X : set evs; evs : otway |] ==> \\<exists>A. Says A B X : set evs";
2.21 +Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> set evs";
2.22 by (etac rev_mp 1);
2.23 by (etac otway.induct 1);
2.24 by Auto_tac;
2.25 qed"Gets_imp_Says";
2.26
2.27 (*Must be proved separately for each protocol*)
2.28 -Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs";
2.29 +Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |] ==> X \\<in> knows Spy evs";
2.30 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
2.31 qed"Gets_imp_knows_Spy";
2.32 AddSDs [Gets_imp_knows_Spy RS parts.Inj];
2.33 @@ -46,18 +46,18 @@
2.34
2.35 (** For reasoning about the encrypted portion of messages **)
2.36
2.37 -Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \
2.38 -\ ==> X : analz (knows Spy evs)";
2.39 +Goal "[| Gets B {|N, Agent A, Agent B, X|} \\<in> set evs; evs \\<in> otway |] \
2.40 +\ ==> X \\<in> analz (knows Spy evs)";
2.41 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
2.42 qed "OR2_analz_knows_Spy";
2.43
2.44 -Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \
2.45 -\ ==> X : analz (knows Spy evs)";
2.46 +Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\<in> set evs; evs \\<in> otway |] \
2.47 +\ ==> X \\<in> analz (knows Spy evs)";
2.48 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
2.49 qed "OR4_analz_knows_Spy";
2.50
2.51 -Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
2.52 -\ ==> K : parts (knows Spy evs)";
2.53 +Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \\<in> set evs \
2.54 +\ ==> K \\<in> parts (knows Spy evs)";
2.55 by (Blast_tac 1);
2.56 qed "Oops_parts_knows_Spy";
2.57
2.58 @@ -79,13 +79,13 @@
2.59 sends messages containing X! **)
2.60
2.61 (*Spy never sees a good agent's shared key!*)
2.62 -Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
2.63 +Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
2.64 by (parts_induct_tac 1);
2.65 by (ALLGOALS Blast_tac);
2.66 qed "Spy_see_shrK";
2.67 Addsimps [Spy_see_shrK];
2.68
2.69 -Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
2.70 +Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
2.71 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
2.72 qed "Spy_analz_shrK";
2.73 Addsimps [Spy_analz_shrK];
2.74 @@ -98,8 +98,8 @@
2.75
2.76 (*Describes the form of K and NA when the Server sends this message. Also
2.77 for Oops case.*)
2.78 -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
2.79 -\ evs : otway |] \
2.80 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
2.81 +\ evs \\<in> otway |] \
2.82 \ ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)";
2.83 by (etac rev_mp 1);
2.84 by (etac otway.induct 1);
2.85 @@ -119,8 +119,8 @@
2.86 (****
2.87 The following is to prove theorems of the form
2.88
2.89 - Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
2.90 - Key K : analz (knows Spy evs)
2.91 + Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
2.92 + Key K \\<in> analz (knows Spy evs)
2.93
2.94 A more general formula must be proved inductively.
2.95 ****)
2.96 @@ -129,9 +129,9 @@
2.97 (** Session keys are not used to encrypt other session keys **)
2.98
2.99 (*The equality makes the induction hypothesis easier to apply*)
2.100 -Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) --> \
2.101 -\ (Key K : analz (Key`KK Un (knows Spy evs))) = \
2.102 -\ (K : KK | Key K : analz (knows Spy evs))";
2.103 +Goal "evs \\<in> otway ==> ALL K KK. KK <= - (range shrK) --> \
2.104 +\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
2.105 +\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
2.106 by (etac otway.induct 1);
2.107 by analz_knows_Spy_tac;
2.108 by (REPEAT_FIRST (resolve_tac [allI, impI]));
2.109 @@ -142,18 +142,18 @@
2.110 qed_spec_mp "analz_image_freshK";
2.111
2.112
2.113 -Goal "[| evs : otway; KAB \\<notin> range shrK |] \
2.114 -\ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \
2.115 -\ (K = KAB | Key K : analz (knows Spy evs))";
2.116 +Goal "[| evs \\<in> otway; KAB \\<notin> range shrK |] \
2.117 +\ ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
2.118 +\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
2.119 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
2.120 qed "analz_insert_freshK";
2.121
2.122
2.123 (*** The Key K uniquely identifies the Server's message. **)
2.124
2.125 -Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
2.126 -\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
2.127 -\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
2.128 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\<in> set evs; \
2.129 +\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\<in> set evs; \
2.130 +\ evs \\<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
2.131 by (etac rev_mp 1);
2.132 by (etac rev_mp 1);
2.133 by (etac otway.induct 1);
2.134 @@ -166,21 +166,21 @@
2.135 (**** Authenticity properties relating to NA ****)
2.136
2.137 (*Only OR1 can have caused such a part of a message to appear.*)
2.138 -Goal "[| A \\<notin> bad; evs : otway |] \
2.139 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
2.140 +Goal "[| A \\<notin> bad; evs \\<in> otway |] \
2.141 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
2.142 \ Says A B {|NA, Agent A, Agent B, \
2.143 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
2.144 -\ : set evs";
2.145 +\ \\<in> set evs";
2.146 by (parts_induct_tac 1);
2.147 by (Blast_tac 1);
2.148 qed_spec_mp "Crypt_imp_OR1";
2.149
2.150 Goal "[| Gets B {|NA, Agent A, Agent B, \
2.151 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
2.152 -\ A \\<notin> bad; evs : otway |] \
2.153 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
2.154 +\ A \\<notin> bad; evs \\<in> otway |] \
2.155 \ ==> Says A B {|NA, Agent A, Agent B, \
2.156 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
2.157 -\ : set evs";
2.158 +\ \\<in> set evs";
2.159 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1);
2.160 qed"Crypt_imp_OR1_Gets";
2.161
2.162 @@ -189,7 +189,7 @@
2.163
2.164 Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \
2.165 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \
2.166 -\ evs : otway; A \\<notin> bad |] \
2.167 +\ evs \\<in> otway; A \\<notin> bad |] \
2.168 \ ==> B = C";
2.169 by (etac rev_mp 1);
2.170 by (etac rev_mp 1);
2.171 @@ -202,8 +202,8 @@
2.172 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
2.173 OR2 encrypts Nonce NB. It prevents the attack that can occur in the
2.174 over-simplified version of this protocol: see OtwayRees_Bad.*)
2.175 -Goal "[| A \\<notin> bad; evs : otway |] \
2.176 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
2.177 +Goal "[| A \\<notin> bad; evs \\<in> otway |] \
2.178 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
2.179 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
2.180 \ \\<notin> parts (knows Spy evs)";
2.181 by (parts_induct_tac 1);
2.182 @@ -214,14 +214,14 @@
2.183
2.184 (*Crucial property: If the encrypted message appears, and A has used NA
2.185 to start a run, then it originated with the Server!*)
2.186 -Goal "[| A \\<notin> bad; evs : otway |] \
2.187 +Goal "[| A \\<notin> bad; evs \\<in> otway |] \
2.188 \ ==> Says A B {|NA, Agent A, Agent B, \
2.189 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \
2.190 -\ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \
2.191 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs --> \
2.192 +\ Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) \
2.193 \ --> (\\<exists>NB. Says Server B \
2.194 \ {|NA, \
2.195 \ Crypt (shrK A) {|NA, Key K|}, \
2.196 -\ Crypt (shrK B) {|NB, Key K|}|} : set evs)";
2.197 +\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs)";
2.198 by (parts_induct_tac 1);
2.199 by (Blast_tac 1);
2.200 (*OR1: it cannot be a new Nonce, contradiction.*)
2.201 @@ -238,14 +238,14 @@
2.202 bad form of this protocol, even though we can prove
2.203 Spy_not_see_encrypted_key*)
2.204 Goal "[| Says A B {|NA, Agent A, Agent B, \
2.205 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
2.206 -\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
2.207 -\ A \\<notin> bad; evs : otway |] \
2.208 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
2.209 +\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
2.210 +\ A \\<notin> bad; evs \\<in> otway |] \
2.211 \ ==> \\<exists>NB. Says Server B \
2.212 \ {|NA, \
2.213 \ Crypt (shrK A) {|NA, Key K|}, \
2.214 \ Crypt (shrK B) {|NB, Key K|}|} \
2.215 -\ : set evs";
2.216 +\ \\<in> set evs";
2.217 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
2.218 qed "A_trusts_OR4";
2.219
2.220 @@ -254,10 +254,10 @@
2.221 Does not in itself guarantee security: an attack could violate
2.222 the premises, e.g. by having A=Spy **)
2.223
2.224 -Goal "[| A \\<notin> bad; B \\<notin> bad; evs : otway |] \
2.225 +Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
2.226 \ ==> Says Server B \
2.227 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \
2.228 -\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
2.229 +\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs --> \
2.230 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \
2.231 \ Key K \\<notin> analz (knows Spy evs)";
2.232 by (etac otway.induct 1);
2.233 @@ -278,9 +278,9 @@
2.234
2.235 Goal "[| Says Server B \
2.236 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \
2.237 -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
2.238 +\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
2.239 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
2.240 -\ A \\<notin> bad; B \\<notin> bad; evs : otway |] \
2.241 +\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
2.242 \ ==> Key K \\<notin> analz (knows Spy evs)";
2.243 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1);
2.244 qed "Spy_not_see_encrypted_key";
2.245 @@ -289,10 +289,10 @@
2.246 (*A's guarantee. The Oops premise quantifies over NB because A cannot know
2.247 what it is.*)
2.248 Goal "[| Says A B {|NA, Agent A, Agent B, \
2.249 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
2.250 -\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
2.251 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
2.252 +\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
2.253 \ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
2.254 -\ A \\<notin> bad; B \\<notin> bad; evs : otway |] \
2.255 +\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
2.256 \ ==> Key K \\<notin> analz (knows Spy evs)";
2.257 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
2.258 qed "A_gets_good_key";
2.259 @@ -303,12 +303,12 @@
2.260 (*Only OR2 can have caused such a part of a message to appear. We do not
2.261 know anything about X: it does NOT have to have the right form.*)
2.262 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
2.263 -\ : parts (knows Spy evs); \
2.264 -\ B \\<notin> bad; evs : otway |] \
2.265 +\ \\<in> parts (knows Spy evs); \
2.266 +\ B \\<notin> bad; evs \\<in> otway |] \
2.267 \ ==> \\<exists>X. Says B Server \
2.268 \ {|NA, Agent A, Agent B, X, \
2.269 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
2.270 -\ : set evs";
2.271 +\ \\<in> set evs";
2.272 by (etac rev_mp 1);
2.273 by (parts_induct_tac 1);
2.274 by (ALLGOALS Blast_tac);
2.275 @@ -317,9 +317,9 @@
2.276
2.277 (** The Nonce NB uniquely identifies B's message. **)
2.278
2.279 -Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \
2.280 -\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \
2.281 -\ evs : otway; B \\<notin> bad |] \
2.282 +Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \\<in> parts(knows Spy evs); \
2.283 +\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \\<in> parts(knows Spy evs); \
2.284 +\ evs \\<in> otway; B \\<notin> bad |] \
2.285 \ ==> NC = NA & C = A";
2.286 by (etac rev_mp 1);
2.287 by (etac rev_mp 1);
2.288 @@ -330,16 +330,16 @@
2.289
2.290 (*If the encrypted message appears, and B has used Nonce NB,
2.291 then it originated with the Server! Quite messy proof.*)
2.292 -Goal "[| B \\<notin> bad; evs : otway |] \
2.293 -\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \
2.294 +Goal "[| B \\<notin> bad; evs \\<in> otway |] \
2.295 +\ ==> Crypt (shrK B) {|NB, Key K|} \\<in> parts (knows Spy evs) \
2.296 \ --> (ALL X'. Says B Server \
2.297 \ {|NA, Agent A, Agent B, X', \
2.298 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
2.299 -\ : set evs \
2.300 +\ \\<in> set evs \
2.301 \ --> Says Server B \
2.302 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \
2.303 \ Crypt (shrK B) {|NB, Key K|}|} \
2.304 -\ : set evs)";
2.305 +\ \\<in> set evs)";
2.306 by (asm_full_simp_tac (simpset() addsimps []) 1);
2.307 by (parts_induct_tac 1);
2.308 by (Blast_tac 1);
2.309 @@ -357,14 +357,14 @@
2.310 has sent the correct message.*)
2.311 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
2.312 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
2.313 -\ : set evs; \
2.314 -\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
2.315 -\ B \\<notin> bad; evs : otway |] \
2.316 +\ \\<in> set evs; \
2.317 +\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
2.318 +\ B \\<notin> bad; evs \\<in> otway |] \
2.319 \ ==> Says Server B \
2.320 \ {|NA, \
2.321 \ Crypt (shrK A) {|NA, Key K|}, \
2.322 \ Crypt (shrK B) {|NB, Key K|}|} \
2.323 -\ : set evs";
2.324 +\ \\<in> set evs";
2.325 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
2.326 qed "B_trusts_OR3";
2.327
2.328 @@ -372,10 +372,10 @@
2.329 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
2.330 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
2.331 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
2.332 -\ : set evs; \
2.333 -\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
2.334 +\ \\<in> set evs; \
2.335 +\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
2.336 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
2.337 -\ A \\<notin> bad; B \\<notin> bad; evs : otway |] \
2.338 +\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
2.339 \ ==> Key K \\<notin> analz (knows Spy evs)";
2.340 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
2.341 qed "B_gets_good_key";
2.342 @@ -383,11 +383,11 @@
2.343
2.344 Goal "[| Says Server B \
2.345 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \
2.346 -\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
2.347 -\ B \\<notin> bad; evs : otway |] \
2.348 +\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
2.349 +\ B \\<notin> bad; evs \\<in> otway |] \
2.350 \ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X, \
2.351 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
2.352 -\ : set evs";
2.353 +\ \\<in> set evs";
2.354 by (etac rev_mp 1);
2.355 by (etac otway.induct 1);
2.356 by (ALLGOALS Asm_simp_tac);
2.357 @@ -399,13 +399,13 @@
2.358 (*After getting and checking OR4, agent A can trust that B has been active.
2.359 We could probably prove that X has the expected form, but that is not
2.360 strictly necessary for authentication.*)
2.361 -Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
2.362 +Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
2.363 \ Says A B {|NA, Agent A, Agent B, \
2.364 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
2.365 -\ A \\<notin> bad; B \\<notin> bad; evs : otway |] \
2.366 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
2.367 +\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
2.368 \ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, \
2.369 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
2.370 -\ : set evs";
2.371 +\ \\<in> set evs";
2.372 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj]
2.373 addSDs [A_trusts_OR4, OR3_imp_OR2]) 1);
2.374 qed "A_auths_B";
3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 13 18:35:48 2001 +0100
3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML Wed Mar 14 08:50:55 2001 +0100
3.3 @@ -17,7 +17,7 @@
3.4
3.5
3.6 (*A "possibility property": there are traces that reach the end*)
3.7 -Goal "B ~= Server \
3.8 +Goal "B \\<noteq> Server \
3.9 \ ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway. \
3.10 \ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
3.11 \ \\<in> set evs";
3.12 @@ -112,8 +112,8 @@
3.13 (****
3.14 The following is to prove theorems of the form
3.15
3.16 - Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
3.17 - Key K : analz (knows Spy evs)
3.18 + Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
3.19 + Key K \\<in> analz (knows Spy evs)
3.20
3.21 A more general formula must be proved inductively.
3.22 ****)
3.23 @@ -168,7 +168,7 @@
3.24 (**** Authenticity properties relating to NA ****)
3.25
3.26 (*If the encrypted message appears then it originated with the Server!*)
3.27 -Goal "[| A \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.28 +Goal "[| A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.29 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
3.30 \ --> (\\<exists>NB. Says Server B \
3.31 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
3.32 @@ -186,7 +186,7 @@
3.33 Freshness may be inferred from nonce NA.*)
3.34 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
3.35 \ \\<in> set evs; \
3.36 -\ A \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.37 +\ A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.38 \ ==> \\<exists>NB. Says Server B \
3.39 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
3.40 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3.41 @@ -239,7 +239,7 @@
3.42 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
3.43 \ \\<in> set evs; \
3.44 \ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
3.45 -\ A \\<notin> bad; B \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.46 +\ A \\<notin> bad; B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.47 \ ==> Key K \\<notin> analz (knows Spy evs)";
3.48 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
3.49 qed "A_gets_good_key";
3.50 @@ -248,7 +248,7 @@
3.51 (**** Authenticity properties relating to NB ****)
3.52
3.53 (*If the encrypted message appears then it originated with the Server!*)
3.54 -Goal "[| B \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.55 +Goal "[| B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.56 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
3.57 \ --> (\\<exists>NA. Says Server B \
3.58 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
3.59 @@ -266,7 +266,7 @@
3.60 has sent the correct message in round 3.*)
3.61 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3.62 \ \\<in> set evs; \
3.63 -\ B \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.64 +\ B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.65 \ ==> \\<exists>NA. Says Server B \
3.66 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
3.67 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3.68 @@ -279,7 +279,7 @@
3.69 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3.70 \ \\<in> set evs; \
3.71 \ ALL NA. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
3.72 -\ A \\<notin> bad; B \\<notin> bad; A ~= B; evs \\<in> otway |] \
3.73 +\ A \\<notin> bad; B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
3.74 \ ==> Key K \\<notin> analz (knows Spy evs)";
3.75 by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
3.76 qed "B_gets_good_key";
4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 13 18:35:48 2001 +0100
4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Mar 14 08:50:55 2001 +0100
4.3 @@ -19,7 +19,7 @@
4.4 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
4.5
4.6 (*A "possibility property": there are traces that reach the end*)
4.7 -Goal "B ~= Server \
4.8 +Goal "B \\<noteq> Server \
4.9 \ ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway. \
4.10 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
4.11 \ \\<in> set evs";
4.12 @@ -207,9 +207,9 @@
4.13 (*** Attempting to prove stronger properties ***)
4.14
4.15 (*Only OR1 can have caused such a part of a message to appear.
4.16 - The premise A ~= B prevents OR2's similar-looking cryptogram from being
4.17 + The premise A \\<noteq> B prevents OR2's similar-looking cryptogram from being
4.18 picked up. Original Otway-Rees doesn't need it.*)
4.19 -Goal "[| A \\<notin> bad; A ~= B; evs \\<in> otway |] \
4.20 +Goal "[| A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
4.21 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
4.22 \ Says A B {|NA, Agent A, Agent B, \
4.23 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs";
4.24 @@ -220,10 +220,10 @@
4.25
4.26 (*Crucial property: If the encrypted message appears, and A has used NA
4.27 to start a run, then it originated with the Server!
4.28 - The premise A ~= B allows use of Crypt_imp_OR1*)
4.29 + The premise A \\<noteq> B allows use of Crypt_imp_OR1*)
4.30 (*Only it is FALSE. Somebody could make a fake message to Server
4.31 substituting some other nonce NA' for NB.*)
4.32 -Goal "[| A \\<notin> bad; A ~= B; evs \\<in> otway |] \
4.33 +Goal "[| A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
4.34 \ ==> Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) --> \
4.35 \ Says A B {|NA, Agent A, Agent B, \
4.36 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
5.1 --- a/src/HOL/Auth/Yahalom.ML Tue Mar 13 18:35:48 2001 +0100
5.2 +++ b/src/HOL/Auth/Yahalom.ML Wed Mar 14 08:50:55 2001 +0100
5.3 @@ -107,8 +107,8 @@
5.4 qed_spec_mp "new_keys_not_used";
5.5 Addsimps [new_keys_not_used];
5.6
5.7 -(*Earlier, \\<forall>protocol proofs declared this theorem.
5.8 - But Yahalom and Kerberos IV are the only ones that need it!*)
5.9 +(*Earlier, all protocol proofs declared this theorem.
5.10 + But few of them actually need it! (Another is Kerberos IV) *)
5.11 bind_thm ("new_keys_not_analzd",
5.12 [analz_subset_parts RS keysFor_mono,
5.13 new_keys_not_used] MRS contra_subsetD);