New treatment of nonce creation
authorpaulson
Thu Jan 09 10:22:11 1997 +0100 (1997-01-09)
changeset 249747de509bdd55
parent 2496 40efb87985b5
child 2498 7914881f47c0
New treatment of nonce creation
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Public.thy
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Thu Jan 09 10:20:03 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Thu Jan 09 10:22:11 1997 +0100
     1.3 @@ -28,7 +28,8 @@
     1.4  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
     1.5  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
     1.6  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
     1.7 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
     1.8 +by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
     1.9 +				    addss (!simpset setsolver safe_solver))));
    1.10  result();
    1.11  
    1.12  
    1.13 @@ -82,24 +83,6 @@
    1.14  AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    1.15  
    1.16  
    1.17 -(*** Future nonces can't be seen or used! ***)
    1.18 -
    1.19 -goal thy "!!i. evs : ns_public ==>        \
    1.20 -\             length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
    1.21 -by (parts_induct_tac 1);
    1.22 -by (REPEAT_FIRST (fast_tac (!claset 
    1.23 -                              addSEs partsEs
    1.24 -                              addSDs  [Says_imp_sees_Spy' RS parts.Inj]
    1.25 -                              addEs [leD RS notE]
    1.26 -			      addDs  [impOfSubs analz_subset_parts,
    1.27 -                                      impOfSubs parts_insert_subset_Un,
    1.28 -                                      Suc_leD]
    1.29 -                              addss (!simpset))));
    1.30 -qed_spec_mp "new_nonces_not_seen";
    1.31 -Addsimps [new_nonces_not_seen];
    1.32 -
    1.33 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
    1.34 -
    1.35  fun analz_induct_tac i = 
    1.36      etac ns_public.induct i	THEN
    1.37      ALLGOALS (asm_simp_tac 
    1.38 @@ -117,11 +100,9 @@
    1.39  \     Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
    1.40  by (analz_induct_tac 1);
    1.41  (*NS3*)
    1.42 -by (fast_tac (!claset addSEs partsEs
    1.43 -                      addEs  [nonce_not_seen_now]) 4);
    1.44 +by (fast_tac (!claset addSEs partsEs) 4);
    1.45  (*NS2*)
    1.46 -by (fast_tac (!claset addSEs partsEs
    1.47 -                      addEs  [nonce_not_seen_now]) 3);
    1.48 +by (fast_tac (!claset addSEs partsEs) 3);
    1.49  (*Fake*)
    1.50  by (best_tac (!claset addIs [analz_insertI]
    1.51  		      addDs [impOfSubs analz_subset_parts,
    1.52 @@ -141,12 +122,13 @@
    1.53  \      A=A' & B=B')";
    1.54  by (analz_induct_tac 1);
    1.55  (*NS1*)
    1.56 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
    1.57  by (expand_case_tac "NA = ?y" 3 THEN
    1.58 -    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
    1.59 +    REPEAT (fast_tac (!claset addSEs partsEs) 3));
    1.60  (*Base*)
    1.61  by (fast_tac (!claset addss (!simpset)) 1);
    1.62  (*Fake*)
    1.63 -by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    1.64 +by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
    1.65  by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.66  by (ex_strip_tac 1);
    1.67  by (best_tac (!claset delrules [conjI]
    1.68 @@ -176,16 +158,16 @@
    1.69                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    1.70  (*NS1*)
    1.71  by (fast_tac (!claset addSEs partsEs
    1.72 -                      addSDs [new_nonces_not_seen, 
    1.73 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.74 +		      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.75 +                      addIs  [impOfSubs analz_subset_parts]) 2);
    1.76  (*Fake*)
    1.77 -by (REPEAT_FIRST spy_analz_tac);
    1.78 +by (spy_analz_tac 1);
    1.79  (*NS2*)
    1.80  by (Step_tac 1);
    1.81  by (fast_tac (!claset addSEs partsEs
    1.82 -                      addSDs [new_nonces_not_seen, 
    1.83 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.84 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.85 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.86 +(*14 seconds.  Much slower still if one tries to prove all NS2 in one step.*)
    1.87 +by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.88                        addDs  [unique_NA]) 1);
    1.89  bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
    1.90  
    1.91 @@ -203,8 +185,7 @@
    1.92  by (ALLGOALS Asm_simp_tac);
    1.93  (*NS1*)
    1.94  by (fast_tac (!claset addSEs partsEs
    1.95 -                      addSDs [new_nonces_not_seen, 
    1.96 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.97 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.98  (*Fake*)
    1.99  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.100  by (fast_tac (!claset addss (!simpset)) 1);
   1.101 @@ -261,12 +242,13 @@
   1.102  \        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & B=B')";
   1.103  by (analz_induct_tac 1);
   1.104  (*NS2*)
   1.105 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   1.106  by (expand_case_tac "NB = ?y" 3 THEN
   1.107 -    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   1.108 +    REPEAT (fast_tac (!claset addSEs partsEs) 3));
   1.109  (*Base*)
   1.110  by (fast_tac (!claset addss (!simpset)) 1);
   1.111  (*Fake*)
   1.112 -by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   1.113 +by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   1.114  by (step_tac (!claset addSIs [analz_insertI]) 1);
   1.115  by (ex_strip_tac 1);
   1.116  by (best_tac (!claset delrules [conjI]
   1.117 @@ -299,17 +281,16 @@
   1.118                        addDs  [unique_NB]) 4);
   1.119  (*NS1*)
   1.120  by (fast_tac (!claset addSEs partsEs
   1.121 -                      addSDs [new_nonces_not_seen, 
   1.122 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.123 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.124  (*Fake*)
   1.125 -by (REPEAT_FIRST spy_analz_tac);
   1.126 +by (spy_analz_tac 1);
   1.127  (*NS2*)
   1.128  by (Step_tac 1);
   1.129  by (fast_tac (!claset addSEs partsEs
   1.130 -                      addSDs [new_nonces_not_seen, 
   1.131 -                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.132 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.133 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   1.134 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
   1.135 +by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.136 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   1.137 +by (fast_tac (!claset addIs  [impOfSubs analz_subset_parts]) 1);
   1.138  bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp));
   1.139  
   1.140  
   1.141 @@ -330,8 +311,7 @@
   1.142  by (ALLGOALS Asm_simp_tac);
   1.143  (*NS1*)
   1.144  by (fast_tac (!claset addSEs partsEs
   1.145 -                      addSDs [new_nonces_not_seen, 
   1.146 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.147 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.148  (*Fake*)
   1.149  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.150  by (fast_tac (!claset addss (!simpset)) 1);
   1.151 @@ -377,8 +357,7 @@
   1.152  (*Fake, NS2, NS3*)
   1.153  (*NS1*)
   1.154  by (fast_tac (!claset addSEs partsEs
   1.155 -                      addSDs [new_nonces_not_seen, 
   1.156 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.157 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.158  (*Fake*)
   1.159  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.160  by (fast_tac (!claset addss (!simpset)) 1);
     2.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Jan 09 10:20:03 1997 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Jan 09 10:22:11 1997 +0100
     2.3 @@ -24,16 +24,15 @@
     2.4            ==> Says Spy B X  # evs : ns_public"
     2.5  
     2.6           (*Alice initiates a protocol run, sending a nonce to Bob*)
     2.7 -    NS1  "[| evs: ns_public;  A ~= B |]
     2.8 -          ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
     2.9 +    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
    2.10 +          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.11                   # evs  :  ns_public"
    2.12  
    2.13           (*Bob responds to Alice's message with a further nonce*)
    2.14 -    NS2  "[| evs: ns_public;  A ~= B;
    2.15 +    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    2.16               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.17                 : set_of_list evs |]
    2.18 -          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)), 
    2.19 -                                         Agent B|})
    2.20 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    2.21                  # evs  :  ns_public"
    2.22  
    2.23           (*Alice proves her existence by sending NB back to Bob.*)
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jan 09 10:20:03 1997 +0100
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Jan 09 10:22:11 1997 +0100
     3.3 @@ -32,7 +32,8 @@
     3.4  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
     3.5  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
     3.6  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
     3.7 -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
     3.8 +by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
     3.9 +				    addss (!simpset setsolver safe_solver))));
    3.10  result();
    3.11  
    3.12  
    3.13 @@ -86,24 +87,6 @@
    3.14  AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    3.15  
    3.16  
    3.17 -(*** Future nonces can't be seen or used! ***)
    3.18 -
    3.19 -goal thy "!!i. evs : ns_public ==>        \
    3.20 -\             length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
    3.21 -by (parts_induct_tac 1);
    3.22 -by (REPEAT_FIRST (fast_tac (!claset 
    3.23 -                              addSEs partsEs
    3.24 -                              addSDs  [Says_imp_sees_Spy' RS parts.Inj]
    3.25 -                              addEs [leD RS notE]
    3.26 -			      addDs  [impOfSubs analz_subset_parts,
    3.27 -                                      impOfSubs parts_insert_subset_Un,
    3.28 -                                      Suc_leD]
    3.29 -                              addss (!simpset))));
    3.30 -qed_spec_mp "new_nonces_not_seen";
    3.31 -Addsimps [new_nonces_not_seen];
    3.32 -
    3.33 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
    3.34 -
    3.35  fun analz_induct_tac i = 
    3.36      etac ns_public.induct i	THEN
    3.37      ALLGOALS (asm_simp_tac 
    3.38 @@ -122,11 +105,9 @@
    3.39  \     Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
    3.40  by (analz_induct_tac 1);
    3.41  (*NS3*)
    3.42 -by (fast_tac (!claset addSEs partsEs
    3.43 -                      addEs  [nonce_not_seen_now]) 4);
    3.44 +by (fast_tac (!claset addSEs partsEs) 4);
    3.45  (*NS2*)
    3.46 -by (fast_tac (!claset addSEs partsEs
    3.47 -                      addEs  [nonce_not_seen_now]) 3);
    3.48 +by (fast_tac (!claset addSEs partsEs) 3);
    3.49  (*Fake*)
    3.50  by (best_tac (!claset addIs [analz_insertI]
    3.51  		      addDs [impOfSubs analz_subset_parts,
    3.52 @@ -146,12 +127,13 @@
    3.53  \      A=A' & B=B')";
    3.54  by (analz_induct_tac 1);
    3.55  (*NS1*)
    3.56 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
    3.57  by (expand_case_tac "NA = ?y" 3 THEN
    3.58 -    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
    3.59 +    REPEAT (fast_tac (!claset addSEs partsEs) 3));
    3.60  (*Base*)
    3.61  by (fast_tac (!claset addss (!simpset)) 1);
    3.62  (*Fake*)
    3.63 -by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    3.64 +by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
    3.65  by (step_tac (!claset addSIs [analz_insertI]) 1);
    3.66  by (ex_strip_tac 1);
    3.67  by (best_tac (!claset delrules [conjI]
    3.68 @@ -181,15 +163,14 @@
    3.69                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    3.70  (*NS1*)
    3.71  by (fast_tac (!claset addSEs partsEs
    3.72 -                      addSDs [new_nonces_not_seen, 
    3.73 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    3.74 +		      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    3.75 +                      addIs  [impOfSubs analz_subset_parts]) 2);
    3.76  (*Fake*)
    3.77 -by (REPEAT_FIRST spy_analz_tac);
    3.78 +by (spy_analz_tac 1);
    3.79  (*NS2*)
    3.80  by (Step_tac 1);
    3.81  by (fast_tac (!claset addSEs partsEs
    3.82 -                      addSDs [new_nonces_not_seen, 
    3.83 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    3.84 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
    3.85  by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    3.86                        addDs  [unique_NA]) 1);
    3.87  bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
    3.88 @@ -206,8 +187,7 @@
    3.89  by (ALLGOALS Asm_simp_tac);
    3.90  (*NS1*)
    3.91  by (fast_tac (!claset addSEs partsEs
    3.92 -                      addSDs [new_nonces_not_seen, 
    3.93 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    3.94 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
    3.95  (*Fake*)
    3.96  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
    3.97  by (fast_tac (!claset addss (!simpset)) 1);
    3.98 @@ -219,7 +199,8 @@
    3.99  (*NS2*)
   3.100  by (Step_tac 1);
   3.101  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   3.102 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.103 +(*11 seconds*)
   3.104 +by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.105                        addDs  [unique_NA]) 1);
   3.106  qed_spec_mp "NA_decrypt_imp_B_msg";
   3.107  
   3.108 @@ -266,12 +247,13 @@
   3.109  \      A=A' & NA=NA')";
   3.110  by (analz_induct_tac 1);
   3.111  (*NS2*)
   3.112 +by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   3.113  by (expand_case_tac "NB = ?y" 3 THEN
   3.114 -    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   3.115 +    REPEAT (fast_tac (!claset addSEs partsEs) 3));
   3.116  (*Base*)
   3.117  by (fast_tac (!claset addss (!simpset)) 1);
   3.118  (*Fake*)
   3.119 -by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   3.120 +by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   3.121  by (step_tac (!claset addSIs [analz_insertI]) 1);
   3.122  by (ex_strip_tac 1);
   3.123  by (best_tac (!claset delrules [conjI]
   3.124 @@ -299,26 +281,18 @@
   3.125  by (analz_induct_tac 1);
   3.126  (*NS1*)
   3.127  by (fast_tac (!claset addSEs partsEs
   3.128 -                      addSDs [new_nonces_not_seen, 
   3.129 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.130 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.131  (*Fake*)
   3.132 -by (REPEAT_FIRST spy_analz_tac);
   3.133 +by (spy_analz_tac 1);
   3.134  (*NS2 and NS3*)
   3.135  by (Step_tac 1);
   3.136 +by (TRYALL (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI])));
   3.137  (*NS2*)
   3.138 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.139 -                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 3);
   3.140  by (fast_tac (!claset addSEs partsEs
   3.141 -                      addSDs [new_nonces_not_seen, 
   3.142 -                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.143 -by (Fast_tac 1);
   3.144 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.145 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.146 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.147  (*NS3*)
   3.148 -by (Fast_tac 2);
   3.149 -by (fast_tac (!claset addSEs partsEs
   3.150 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj,
   3.151 -			      new_nonces_not_seen, 
   3.152 -                              impOfSubs analz_subset_parts]) 1);
   3.153 -
   3.154  by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
   3.155      THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
   3.156  by (Fast_tac 1);
   3.157 @@ -338,8 +312,7 @@
   3.158  by (ALLGOALS Asm_simp_tac);
   3.159  (*NS1*)
   3.160  by (fast_tac (!claset addSEs partsEs
   3.161 -                      addSDs [new_nonces_not_seen, 
   3.162 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.163 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.164  (*Fake*)
   3.165  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   3.166  by (fast_tac (!claset addss (!simpset)) 1);
   3.167 @@ -380,16 +353,15 @@
   3.168  by (analz_induct_tac 1);
   3.169  (*NS1*)
   3.170  by (fast_tac (!claset addSEs partsEs
   3.171 -                      addSDs [new_nonces_not_seen, 
   3.172 -			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.173 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.174  (*Fake*)
   3.175 -by (REPEAT_FIRST spy_analz_tac);
   3.176 +by (spy_analz_tac 1);
   3.177  (*NS2 and NS3*)
   3.178  by (Step_tac 1);
   3.179 +by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
   3.180  (*NS2*)
   3.181  by (fast_tac (!claset addSEs partsEs
   3.182 -                      addSDs [new_nonces_not_seen, 
   3.183 -                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.184 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.185  by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.186                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.187  (*NS3*)
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jan 09 10:20:03 1997 +0100
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jan 09 10:22:11 1997 +0100
     4.3 @@ -28,15 +28,15 @@
     4.4            ==> Says Spy B X  # evs : ns_public"
     4.5  
     4.6           (*Alice initiates a protocol run, sending a nonce to Bob*)
     4.7 -    NS1  "[| evs: ns_public;  A ~= B |]
     4.8 -          ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
     4.9 +    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
    4.10 +          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.11                  # evs  :  ns_public"
    4.12  
    4.13           (*Bob responds to Alice's message with a further nonce*)
    4.14 -    NS2  "[| evs: ns_public;  A ~= B;
    4.15 +    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    4.16               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.17                 : set_of_list evs |]
    4.18 -          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs))|})
    4.19 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    4.20                  # evs  :  ns_public"
    4.21  
    4.22           (*Alice proves her existence by sending NB back to Bob.*)
     5.1 --- a/src/HOL/Auth/Public.ML	Thu Jan 09 10:20:03 1997 +0100
     5.2 +++ b/src/HOL/Auth/Public.ML	Thu Jan 09 10:22:11 1997 +0100
     5.3 @@ -11,6 +11,9 @@
     5.4  
     5.5  open Public;
     5.6  
     5.7 +(*Injectiveness of new nonces*)
     5.8 +AddIffs [inj_newN RS inj_eq];
     5.9 +
    5.10  (*Holds because Friend is injective: thus cannot prove for all f*)
    5.11  goal thy "(Friend x : Friend``A) = (x:A)";
    5.12  by (Auto_tac());
    5.13 @@ -24,23 +27,6 @@
    5.14    will not!*)
    5.15  Addsimps [o_def];
    5.16  
    5.17 -(*** Basic properties of pubK ***)
    5.18 -
    5.19 -(*Injectiveness and freshness of new keys and nonces*)
    5.20 -AddIffs [inj_pubK RS inj_eq, inj_newN RS inj_eq];
    5.21 -
    5.22 -(** Rewrites should not refer to  initState(Friend i) 
    5.23 -    -- not in normal form! **)
    5.24 -
    5.25 -Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
    5.26 -
    5.27 -goal thy "Nonce (newN i) ~: parts (initState lost B)";
    5.28 -by (agent.induct_tac "B" 1);
    5.29 -by (Auto_tac ());
    5.30 -qed "newN_notin_initState";
    5.31 -
    5.32 -AddIffs [newN_notin_initState];
    5.33 -
    5.34  goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
    5.35  by (agent.induct_tac "C" 1);
    5.36  by (auto_tac (!claset addIs [range_eqI], !simpset));
    5.37 @@ -63,6 +49,11 @@
    5.38  by (Auto_tac ());
    5.39  qed "sees_mono";
    5.40  
    5.41 +(*** Basic properties of pubK & priK ***)
    5.42 +
    5.43 +AddIffs [inj_pubK RS inj_eq];
    5.44 +Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
    5.45 +
    5.46  (*Agents see their own private keys!*)
    5.47  goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
    5.48  by (list.induct_tac "evs" 1);
    5.49 @@ -157,6 +148,48 @@
    5.50  Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
    5.51  
    5.52  
    5.53 +(*** Fresh nonces ***)
    5.54 +
    5.55 +goal thy "Nonce N ~: parts (initState lost B)";
    5.56 +by (agent.induct_tac "B" 1);
    5.57 +by (Auto_tac ());
    5.58 +qed "Nonce_notin_initState";
    5.59 +
    5.60 +AddIffs [Nonce_notin_initState];
    5.61 +
    5.62 +goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
    5.63 +be (impOfSubs parts_mono) 1;
    5.64 +by (Fast_tac 1);
    5.65 +qed "usedI";
    5.66 +
    5.67 +AddIs [usedI];
    5.68 +
    5.69 +(*Yields a supply of fresh nonces for possibility theorems.*)
    5.70 +goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
    5.71 +by (list.induct_tac "evs" 1);
    5.72 +by (res_inst_tac [("x","0")] exI 1);
    5.73 +by (Step_tac 1);
    5.74 +by (Full_simp_tac 1);
    5.75 +by (event.induct_tac "a" 1);
    5.76 +by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
    5.77 +by (msg.induct_tac "msg" 1);
    5.78 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
    5.79 +by (Step_tac 1);
    5.80 +(*MPair case*)
    5.81 +by (res_inst_tac [("x","Na+Nb")] exI 2);
    5.82 +by (fast_tac (!claset addSEs [add_leE]) 2);
    5.83 +(*Nonce case*)
    5.84 +by (res_inst_tac [("x","N + Suc nat")] exI 1);
    5.85 +by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
    5.86 +val lemma = result();
    5.87 +
    5.88 +goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
    5.89 +br (lemma RS exE) 1;
    5.90 +br selectI 1;
    5.91 +by (Fast_tac 1);
    5.92 +qed "Nonce_supply";
    5.93 +
    5.94 +
    5.95  (** Power of the Spy **)
    5.96  
    5.97  (*The Spy can see more than anybody else, except for their initial state*)
     6.1 --- a/src/HOL/Auth/Public.thy	Thu Jan 09 10:20:03 1997 +0100
     6.2 +++ b/src/HOL/Auth/Public.thy	Thu Jan 09 10:22:11 1997 +0100
     6.3 @@ -50,6 +50,13 @@
     6.4    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
     6.5  
     6.6  
     6.7 +constdefs
     6.8 +  (*Set of items that might be visible to somebody: complement of the set
     6.9 +        of fresh items*)
    6.10 +  used :: event list => msg set
    6.11 +    "used evs == parts (UN lost B. sees lost B evs)"
    6.12 +
    6.13 +
    6.14  (*Agents generate "random" nonces, uniquely determined by their argument.*)
    6.15  consts
    6.16    newN  :: nat => nat