1.1 --- a/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 15:56:12 1998 +0200
1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 16:14:34 1998 +0200
1.3 @@ -16,9 +16,6 @@
1.4 Tidied by lcp.
1.5 *)
1.6
1.7 -proof_timing:=true;
1.8 -HOL_quantifiers := false;
1.9 -
1.10 AddEs spies_partsEs;
1.11 AddDs [impOfSubs analz_subset_parts];
1.12 AddDs [impOfSubs Fake_parts_insert];
2.1 --- a/src/HOL/Auth/NS_Public.ML Fri Aug 21 15:56:12 1998 +0200
2.2 +++ b/src/HOL/Auth/NS_Public.ML Fri Aug 21 16:14:34 1998 +0200
2.3 @@ -7,9 +7,6 @@
2.4 Version incorporating Lowe's fix (inclusion of B's identify in round 2).
2.5 *)
2.6
2.7 -set proof_timing;
2.8 -HOL_quantifiers := false;
2.9 -
2.10 AddEs spies_partsEs;
2.11 AddDs [impOfSubs analz_subset_parts];
2.12 AddDs [impOfSubs Fake_parts_insert];
3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 15:56:12 1998 +0200
3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 16:14:34 1998 +0200
3.3 @@ -11,8 +11,6 @@
3.4 Proc. Royal Soc. 426 (1989)
3.5 *)
3.6
3.7 -HOL_quantifiers := false;
3.8 -
3.9 AddEs spies_partsEs;
3.10 AddDs [impOfSubs analz_subset_parts];
3.11 AddDs [impOfSubs Fake_parts_insert];
4.1 --- a/src/HOL/Auth/NS_Shared.ML Fri Aug 21 15:56:12 1998 +0200
4.2 +++ b/src/HOL/Auth/NS_Shared.ML Fri Aug 21 16:14:34 1998 +0200
4.3 @@ -10,8 +10,6 @@
4.4 Proc. Royal Soc. 426 (1989)
4.5 *)
4.6
4.7 -HOL_quantifiers := false;
4.8 -
4.9 AddEs spies_partsEs;
4.10 AddDs [impOfSubs analz_subset_parts];
4.11 AddDs [impOfSubs Fake_parts_insert];
5.1 --- a/src/HOL/Auth/NS_Shared.thy Fri Aug 21 15:56:12 1998 +0200
5.2 +++ b/src/HOL/Auth/NS_Shared.thy Fri Aug 21 16:14:34 1998 +0200
5.3 @@ -71,8 +71,7 @@
5.4 (*This message models possible leaks of session keys.
5.5 The two Nonces identify the protocol run: the rule insists upon
5.6 the true senders in order to make them accurate.*)
5.7 - Oops "[| evso: ns_shared; A ~= Spy;
5.8 - Says B A (Crypt K (Nonce NB)) : set evso;
5.9 + Oops "[| evso: ns_shared; Says B A (Crypt K (Nonce NB)) : set evso;
5.10 Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
5.11 : set evso |]
5.12 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
6.1 --- a/src/HOL/Auth/OtwayRees.ML Fri Aug 21 15:56:12 1998 +0200
6.2 +++ b/src/HOL/Auth/OtwayRees.ML Fri Aug 21 16:14:34 1998 +0200
6.3 @@ -92,8 +92,7 @@
6.4
6.5
6.6 (*Nobody can have used non-existent keys!*)
6.7 -Goal "evs : otway ==> \
6.8 -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
6.9 +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
6.10 by (parts_induct_tac 1);
6.11 (*Fake*)
6.12 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
6.13 @@ -114,7 +113,7 @@
6.14 (*Describes the form of K and NA when the Server sends this message. Also
6.15 for Oops case.*)
6.16 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
6.17 -\ evs : otway |] \
6.18 +\ evs : otway |] \
6.19 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
6.20 by (etac rev_mp 1);
6.21 by (etac otway.induct 1);
6.22 @@ -144,23 +143,22 @@
6.23 (** Session keys are not used to encrypt other session keys **)
6.24
6.25 (*The equality makes the induction hypothesis easier to apply*)
6.26 -Goal "evs : otway ==> \
6.27 -\ ALL K KK. KK <= Compl (range shrK) --> \
6.28 -\ (Key K : analz (Key``KK Un (spies evs))) = \
6.29 -\ (K : KK | Key K : analz (spies evs))";
6.30 +Goal "evs : otway ==> ALL K KK. KK <= Compl (range shrK) --> \
6.31 +\ (Key K : analz (Key``KK Un (spies evs))) = \
6.32 +\ (K : KK | Key K : analz (spies evs))";
6.33 by (etac otway.induct 1);
6.34 by analz_spies_tac;
6.35 by (REPEAT_FIRST (resolve_tac [allI, impI]));
6.36 -by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
6.37 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
6.38 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
6.39 (*Fake*)
6.40 by (spy_analz_tac 1);
6.41 qed_spec_mp "analz_image_freshK";
6.42
6.43
6.44 -Goal "[| evs : otway; KAB ~: range shrK |] ==> \
6.45 -\ Key K : analz (insert (Key KAB) (spies evs)) = \
6.46 -\ (K = KAB | Key K : analz (spies evs))";
6.47 +Goal "[| evs : otway; KAB ~: range shrK |] \
6.48 +\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \
6.49 +\ (K = KAB | Key K : analz (spies evs))";
6.50 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
6.51 qed "analz_insert_freshK";
6.52
6.53 @@ -168,8 +166,8 @@
6.54 (*** The Key K uniquely identifies the Server's message. **)
6.55
6.56 Goal "evs : otway ==> \
6.57 -\ EX B' NA' NB' X'. ALL B NA NB X. \
6.58 -\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
6.59 +\ EX B' NA' NB' X'. ALL B NA NB X. \
6.60 +\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
6.61 \ B=B' & NA=NA' & NB=NB' & X=X'";
6.62 by (etac otway.induct 1);
6.63 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
7.1 --- a/src/HOL/Auth/OtwayRees.thy Fri Aug 21 15:56:12 1998 +0200
7.2 +++ b/src/HOL/Auth/OtwayRees.thy Fri Aug 21 16:14:34 1998 +0200
7.3 @@ -72,7 +72,7 @@
7.4
7.5 (*This message models possible leaks of session keys. The nonces
7.6 identify the protocol run.*)
7.7 - Oops "[| evso: otway; B ~= Spy;
7.8 + Oops "[| evso: otway;
7.9 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
7.10 : set evso |]
7.11 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
8.1 --- a/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 15:56:12 1998 +0200
8.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 16:14:34 1998 +0200
8.3 @@ -63,7 +63,7 @@
8.4
8.5 (*This message models possible leaks of session keys. The nonces
8.6 identify the protocol run. B is not assumed to know shrK A.*)
8.7 - Oops "[| evso: otway; B ~= Spy;
8.8 + Oops "[| evso: otway;
8.9 Says Server B
8.10 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
8.11 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
9.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 15:56:12 1998 +0200
9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 16:14:34 1998 +0200
9.3 @@ -69,7 +69,7 @@
9.4
9.5 (*This message models possible leaks of session keys. The nonces
9.6 identify the protocol run.*)
9.7 - Oops "[| evso: otway; B ~= Spy;
9.8 + Oops "[| evso: otway;
9.9 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
9.10 : set evso |]
9.11 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
10.1 --- a/src/HOL/Auth/ROOT.ML Fri Aug 21 15:56:12 1998 +0200
10.2 +++ b/src/HOL/Auth/ROOT.ML Fri Aug 21 16:14:34 1998 +0200
10.3 @@ -11,6 +11,7 @@
10.4 writeln"Root file for HOL/Auth";
10.5 set proof_timing;
10.6 goals_limit := 1;
10.7 +HOL_quantifiers := false;
10.8
10.9 (*Shared-key protocols*)
10.10 time_use_thy "NS_Shared";
11.1 --- a/src/HOL/Auth/Recur.ML Fri Aug 21 15:56:12 1998 +0200
11.2 +++ b/src/HOL/Auth/Recur.ML Fri Aug 21 16:14:34 1998 +0200
11.3 @@ -9,6 +9,11 @@
11.4 Pretty.setdepth 30;
11.5
11.6
11.7 +AddEs spies_partsEs;
11.8 +AddDs [impOfSubs analz_subset_parts];
11.9 +AddDs [impOfSubs Fake_parts_insert];
11.10 +
11.11 +
11.12 (** Possibility properties: traces that reach the end
11.13 ONE theorem would be more elegant and faster!
11.14 By induction on a list of agents (no repetitions)
11.15 @@ -104,8 +109,7 @@
11.16
11.17 val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
11.18
11.19 -Goal "Says C' B {|Crypt K X, X', RA|} : set evs \
11.20 -\ ==> RA : analz (spies evs)";
11.21 +Goal "Says C' B {|Crypt K X, X', RA|} : set evs ==> RA : analz (spies evs)";
11.22 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
11.23 qed "RA4_analz_spies";
11.24
11.25 @@ -121,11 +125,11 @@
11.26
11.27 (*For proving the easier theorems about X ~: parts (spies evs).*)
11.28 fun parts_induct_tac i =
11.29 - etac recur.induct i THEN
11.30 - forward_tac [RA2_parts_spies] (i+3) THEN
11.31 - forward_tac [respond_imp_responses] (i+4) THEN
11.32 - forward_tac [RA4_parts_spies] (i+5) THEN
11.33 - prove_simple_subgoals_tac i;
11.34 + EVERY [etac recur.induct i,
11.35 + forward_tac [RA4_parts_spies] (i+5),
11.36 + forward_tac [respond_imp_responses] (i+4),
11.37 + forward_tac [RA2_parts_spies] (i+3),
11.38 + prove_simple_subgoals_tac i];
11.39
11.40
11.41 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
11.42 @@ -136,16 +140,15 @@
11.43
11.44 Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
11.45 by (parts_induct_tac 1);
11.46 -by (Fake_parts_insert_tac 1);
11.47 -by (ALLGOALS
11.48 - (asm_simp_tac (simpset() addsimps [parts_insert2, parts_insert_spies])));
11.49 +by Auto_tac;
11.50 (*RA3*)
11.51 -by (blast_tac (claset() addDs [Key_in_parts_respond]) 1);
11.52 +by (auto_tac (claset() addDs [Key_in_parts_respond],
11.53 + simpset() addsimps [parts_insert_spies]));
11.54 qed "Spy_see_shrK";
11.55 Addsimps [Spy_see_shrK];
11.56
11.57 Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
11.58 -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
11.59 +by Auto_tac;
11.60 qed "Spy_analz_shrK";
11.61 Addsimps [Spy_analz_shrK];
11.62
11.63 @@ -156,16 +159,15 @@
11.64 (** Nobody can have used non-existent keys! **)
11.65
11.66 (*The special case of H={} has the same proof*)
11.67 -Goal "[| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
11.68 +Goal "[| K : keysFor (parts (insert RB H)); RB : responses evs |] \
11.69 \ ==> K : range shrK | K : keysFor (parts H)";
11.70 by (etac rev_mp 1);
11.71 -by (etac (respond_imp_responses RS responses.induct) 1);
11.72 +by (etac responses.induct 1);
11.73 by Auto_tac;
11.74 qed_spec_mp "Key_in_keysFor_parts";
11.75
11.76
11.77 -Goal "evs : recur ==> \
11.78 -\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
11.79 +Goal "evs : recur ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
11.80 by (parts_induct_tac 1);
11.81 (*RA3*)
11.82 by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
11.83 @@ -244,8 +246,7 @@
11.84
11.85 (*Everything that's hashed is already in past traffic. *)
11.86 Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \
11.87 -\ evs : recur; A ~: bad |] \
11.88 -\ ==> X : parts (spies evs)";
11.89 +\ evs : recur; A ~: bad |] ==> X : parts (spies evs)";
11.90 by (etac rev_mp 1);
11.91 by (parts_induct_tac 1);
11.92 (*RA3 requires a further induction*)
11.93 @@ -267,15 +268,14 @@
11.94 \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
11.95 \ --> B=B' & P=P'";
11.96 by (parts_induct_tac 1);
11.97 -by (Fake_parts_insert_tac 1);
11.98 +by (Blast_tac 1);
11.99 by (etac responses.induct 3);
11.100 by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib])));
11.101 by (clarify_tac (claset() addSEs partsEs) 1);
11.102 (*RA1,2: creation of new Nonce. Move assertion into global context*)
11.103 by (ALLGOALS (expand_case_tac "NA = ?y"));
11.104 by (REPEAT_FIRST (ares_tac [exI]));
11.105 -by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]
11.106 - addSEs spies_partsEs) 1));
11.107 +by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1));
11.108 val lemma = result();
11.109
11.110 Goalw [HPair_def]
11.111 @@ -342,10 +342,10 @@
11.112 qed "respond_certificate";
11.113
11.114
11.115 -Goal "!!K'. (PB,RB,KXY) : respond evs \
11.116 -\ ==> EX A' B'. ALL A B N. \
11.117 -\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
11.118 -\ --> (A'=A & B'=B) | (A'=B & B'=A)";
11.119 +Goal "(PB,RB,KXY) : respond evs \
11.120 +\ ==> EX A' B'. ALL A B N. \
11.121 +\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
11.122 +\ --> (A'=A & B'=B) | (A'=B & B'=A)";
11.123 by (etac respond.induct 1);
11.124 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib])));
11.125 (*Base case*)
11.126 @@ -354,19 +354,18 @@
11.127 by (expand_case_tac "K = KBC" 1);
11.128 by (dtac respond_Key_in_parts 1);
11.129 by (blast_tac (claset() addSIs [exI]
11.130 - addSEs partsEs
11.131 addDs [Key_in_parts_respond]) 1);
11.132 by (expand_case_tac "K = KAB" 1);
11.133 by (REPEAT (ares_tac [exI] 2));
11.134 by (ex_strip_tac 1);
11.135 by (dtac respond_certificate 1);
11.136 -by (Fast_tac 1);
11.137 +by (Blast_tac 1);
11.138 val lemma = result();
11.139
11.140 Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
11.141 -\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
11.142 -\ (PB,RB,KXY) : respond evs |] \
11.143 -\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
11.144 +\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
11.145 +\ (PB,RB,KXY) : respond evs |] \
11.146 +\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
11.147 by (prove_unique_tac lemma 1);
11.148 qed "unique_session_keys";
11.149
11.150 @@ -390,11 +389,11 @@
11.151 [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
11.152 by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib])));
11.153 (** LEVEL 5 **)
11.154 -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
11.155 +by (Blast_tac 1);
11.156 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
11.157 by (ALLGOALS Clarify_tac);
11.158 by (blast_tac (claset() addSDs [resp_analz_insert]
11.159 - addIs [impOfSubs analz_subset_parts]) 2);
11.160 + addIs [impOfSubs analz_subset_parts]) 2);
11.161 by (blast_tac (claset() addSDs [respond_certificate]) 1);
11.162 by (Asm_full_simp_tac 1);
11.163 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
11.164 @@ -456,7 +455,7 @@
11.165 \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
11.166 by (etac rev_mp 1);
11.167 by (parts_induct_tac 1);
11.168 -by (Fake_parts_insert_tac 1);
11.169 +by (Blast_tac 1);
11.170 (*RA3*)
11.171 by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1);
11.172 qed_spec_mp "Hash_auth_sender";
11.173 @@ -473,7 +472,7 @@
11.174 \ Crypt (shrK A) Y : parts {RC}";
11.175 by (etac rev_mp 1);
11.176 by (parts_induct_tac 1);
11.177 -by (Fake_parts_insert_tac 1);
11.178 +by (Blast_tac 1);
11.179 (*RA4*)
11.180 by (Blast_tac 4);
11.181 (*RA3*)
12.1 --- a/src/HOL/Auth/Recur.thy Fri Aug 21 15:56:12 1998 +0200
12.2 +++ b/src/HOL/Auth/Recur.thy Fri Aug 21 16:14:34 1998 +0200
12.3 @@ -92,7 +92,17 @@
12.4 RA|} : set evs4 |]
12.5 ==> Says B A RA # evs4 : recur"
12.6
12.7 -(**No "oops" message can easily be expressed. Each session key is
12.8 - associated--in two separate messages--with two nonces.
12.9 -***)
12.10 end
12.11 +
12.12 + (*No "oops" message can easily be expressed. Each session key is
12.13 + associated--in two separate messages--with two nonces. This is
12.14 + one try, but it isn't that useful. Re domino attack, note that
12.15 + Recur.ML proves that each session key is secure provided the two
12.16 + peers are, even if there are compromised agents elsewhere in
12.17 + the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts,
12.18 + etc.
12.19 +
12.20 + Oops "[| evso: recur; Says Server B RB : set evso;
12.21 + RB : responses evs'; Key K : parts {RB} |]
12.22 + ==> Notes Spy {|Key K, RB|} # evso : recur"
12.23 + *)
13.1 --- a/src/HOL/Auth/TLS.ML Fri Aug 21 15:56:12 1998 +0200
13.2 +++ b/src/HOL/Auth/TLS.ML Fri Aug 21 16:14:34 1998 +0200
13.3 @@ -163,8 +163,7 @@
13.4 little point in doing so: the loss of their private keys is a worse
13.5 breach of security.*)
13.6 Goalw [certificate_def]
13.7 - "[| certificate B KB : parts (spies evs); evs : tls |] \
13.8 -\ ==> pubK B = KB";
13.9 + "[| certificate B KB : parts (spies evs); evs : tls |] ==> pubK B = KB";
13.10 by (etac rev_mp 1);
13.11 by (parts_induct_tac 1);
13.12 by (Fake_parts_insert_tac 1);
13.13 @@ -193,7 +192,7 @@
13.14 (*** Properties of items found in Notes ***)
13.15
13.16 Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \
13.17 -\ ==> Crypt (pubK B) X : parts (spies evs)";
13.18 +\ ==> Crypt (pubK B) X : parts (spies evs)";
13.19 by (etac rev_mp 1);
13.20 by (analz_induct_tac 1);
13.21 by (blast_tac (claset() addIs [parts_insertI]) 1);
13.22 @@ -201,8 +200,8 @@
13.23
13.24 (*C may be either A or B*)
13.25 Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
13.26 -\ evs : tls \
13.27 -\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
13.28 +\ evs : tls |] \
13.29 +\ ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
13.30 by (etac rev_mp 1);
13.31 by (parts_induct_tac 1);
13.32 by (ALLGOALS Clarify_tac);
13.33 @@ -215,8 +214,8 @@
13.34
13.35 (*Compared with the theorem above, both premise and conclusion are stronger*)
13.36 Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
13.37 -\ evs : tls \
13.38 -\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
13.39 +\ evs : tls |] \
13.40 +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
13.41 by (etac rev_mp 1);
13.42 by (parts_induct_tac 1);
13.43 (*ServerAccepts*)
13.44 @@ -230,7 +229,7 @@
13.45 Goal "[| X : parts (spies evs); \
13.46 \ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \
13.47 \ evs : tls; A ~: bad |] \
13.48 -\ ==> Says A B X : set evs";
13.49 +\ ==> Says A B X : set evs";
13.50 by (etac rev_mp 1);
13.51 by (hyp_subst_tac 1);
13.52 by (parts_induct_tac 1);
13.53 @@ -242,7 +241,7 @@
13.54 \ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
13.55 \ certificate A KA : parts (spies evs); \
13.56 \ evs : tls; A ~: bad |] \
13.57 -\ ==> Says A B X : set evs";
13.58 +\ ==> Says A B X : set evs";
13.59 by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
13.60 qed "TrustCertVerify";
13.61
13.62 @@ -275,12 +274,13 @@
13.63 Addsimps [no_Notes_A_PRF];
13.64
13.65
13.66 -Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \
13.67 -\ evs : tls |] \
13.68 -\ ==> Nonce PMS : parts (spies evs)";
13.69 +Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); evs : tls |] \
13.70 +\ ==> Nonce PMS : parts (spies evs)";
13.71 by (etac rev_mp 1);
13.72 by (parts_induct_tac 1);
13.73 by (Fake_parts_insert_tac 1);
13.74 +(*SpyKeys*)
13.75 +by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 1);
13.76 (*Six others, all trivial or by freshness*)
13.77 by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]
13.78 addSEs spies_partsEs) 1));
13.79 @@ -321,9 +321,8 @@
13.80 **)
13.81
13.82 (*In A's internal Note, PMS determines A and B.*)
13.83 -Goal "evs : tls \
13.84 -\ ==> EX A' B'. ALL A B. \
13.85 -\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
13.86 +Goal "evs : tls ==> EX A' B'. ALL A B. \
13.87 +\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
13.88 by (parts_induct_tac 1);
13.89 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
13.90 (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
13.91 @@ -344,9 +343,9 @@
13.92
13.93 (*Key compromise lemma needed to prove analz_image_keys.
13.94 No collection of keys can help the spy get new private keys.*)
13.95 -Goal "evs : tls ==> \
13.96 -\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
13.97 -\ (priK B : KK | B : bad)";
13.98 +Goal "evs : tls \
13.99 +\ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
13.100 +\ (priK B : KK | B : bad)";
13.101 by (etac tls.induct 1);
13.102 by (ALLGOALS
13.103 (asm_simp_tac (analz_image_keys_ss
13.104 @@ -416,7 +415,7 @@
13.105 by (hyp_subst_tac 1);
13.106 by (analz_induct_tac 1);
13.107 (*SpyKeys*)
13.108 -by (blast_tac (claset() addSEs spies_partsEs) 3);
13.109 +by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 3);
13.110 (*Fake*)
13.111 by (Fake_parts_insert_tac 2);
13.112 (** LEVEL 6 **)
13.113 @@ -512,9 +511,9 @@
13.114 (*If A created PMS then nobody other than the Spy would send a message
13.115 using a clientK generated from that PMS.*)
13.116 Goal "[| evs : tls; A' ~= Spy |] \
13.117 -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.118 -\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
13.119 -\ A = A'";
13.120 +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.121 +\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
13.122 +\ A = A'";
13.123 by (analz_induct_tac 1); (*8 seconds*)
13.124 by (ALLGOALS Clarify_tac);
13.125 (*ClientFinished, ClientResume: by unicity of PMS*)
13.126 @@ -531,9 +530,9 @@
13.127 (*If A created PMS and has not leaked her clientK to the Spy,
13.128 then nobody has.*)
13.129 Goal "evs : tls \
13.130 -\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
13.131 -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.132 -\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
13.133 +\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
13.134 +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.135 +\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs)";
13.136 by (etac tls.induct 1);
13.137 (*This roundabout proof sequence avoids looping in simplification*)
13.138 by (ALLGOALS Simp_tac);
13.139 @@ -554,9 +553,9 @@
13.140 (*If A created PMS for B, then nobody other than B or the Spy would
13.141 send a message using a serverK generated from that PMS.*)
13.142 Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \
13.143 -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.144 -\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
13.145 -\ B = B'";
13.146 +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.147 +\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
13.148 +\ B = B'";
13.149 by (analz_induct_tac 1); (*9 seconds*)
13.150 by (ALLGOALS Clarify_tac);
13.151 (*ServerResume, ServerFinished: by unicity of PMS*)
13.152 @@ -690,10 +689,10 @@
13.153 ***)
13.154
13.155 Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \
13.156 -\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
13.157 -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.158 -\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \
13.159 -\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.160 +\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
13.161 +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
13.162 +\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \
13.163 +\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.164 by (hyp_subst_tac 1);
13.165 by (analz_induct_tac 1); (*15 seconds*)
13.166 by (ALLGOALS Clarify_tac);
13.167 @@ -716,7 +715,7 @@
13.168 \ Notes A {|Agent B, Nonce PMS|} : set evs; \
13.169 \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \
13.170 \ evs : tls; A ~: bad; B ~: bad |] \
13.171 -\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.172 +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.173 by (blast_tac (claset() addIs [lemma]
13.174 addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
13.175 qed "TrustClientMsg";
13.176 @@ -733,8 +732,8 @@
13.177 \ certificate A KA : parts (spies evs); \
13.178 \ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
13.179 \ : set evs; \
13.180 -\ evs : tls; A ~: bad; B ~: bad |] \
13.181 -\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.182 +\ evs : tls; A ~: bad; B ~: bad |] \
13.183 +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
13.184 by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify]
13.185 addDs [Says_imp_spies RS parts.Inj]) 1);
13.186 qed "AuthClientFinished";
14.1 --- a/src/HOL/Auth/TLS.thy Fri Aug 21 15:56:12 1998 +0200
14.2 +++ b/src/HOL/Auth/TLS.thy Fri Aug 21 16:14:34 1998 +0200
14.3 @@ -88,7 +88,7 @@
14.4
14.5 SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
14.6 "[| evsSK: tls;
14.7 - Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
14.8 + {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
14.9 ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
14.10 Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
14.11
15.1 --- a/src/HOL/Auth/Yahalom.thy Fri Aug 21 15:56:12 1998 +0200
15.2 +++ b/src/HOL/Auth/Yahalom.thy Fri Aug 21 16:14:34 1998 +0200
15.3 @@ -60,7 +60,7 @@
15.4 (*This message models possible leaks of session keys. The Nonces
15.5 identify the protocol run. Quoting Server here ensures they are
15.6 correct.*)
15.7 - Oops "[| evso: yahalom; A ~= Spy;
15.8 + Oops "[| evso: yahalom;
15.9 Says Server A {|Crypt (shrK A)
15.10 {|Agent B, Key K, Nonce NA, Nonce NB|},
15.11 X|} : set evso |]
16.1 --- a/src/HOL/Auth/Yahalom2.thy Fri Aug 21 15:56:12 1998 +0200
16.2 +++ b/src/HOL/Auth/Yahalom2.thy Fri Aug 21 16:14:34 1998 +0200
16.3 @@ -64,7 +64,7 @@
16.4 (*This message models possible leaks of session keys. The nonces
16.5 identify the protocol run. Quoting Server here ensures they are
16.6 correct. *)
16.7 - Oops "[| evso: yahalom; A ~= Spy;
16.8 + Oops "[| evso: yahalom;
16.9 Says Server A {|Nonce NB,
16.10 Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
16.11 X|} : set evso |]