src/HOL/Auth/OtwayRees_AN.ML
changeset 3519 ab0a9fbed4c0
parent 3516 470626799511
child 3543 82f33248d89d
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  (*A "possibility property": there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
     1.7 -\        ==> EX K. EX NA. EX evs: otway lost.                                 \
     1.8 +\        ==> EX K. EX NA. EX evs: otway.                                 \
     1.9  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    1.10  \             : set evs";
    1.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.12 @@ -33,7 +33,7 @@
    1.13  (**** Inductive proofs about otway ****)
    1.14  
    1.15  (*Nobody sends themselves messages*)
    1.16 -goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    1.17 +goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    1.18  by (etac otway.induct 1);
    1.19  by (Auto_tac());
    1.20  qed_spec_mp "not_Says_to_self";
    1.21 @@ -44,12 +44,12 @@
    1.22  (** For reasoning about the encrypted portion of messages **)
    1.23  
    1.24  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    1.25 -\                X : analz (sees lost Spy evs)";
    1.26 +\                X : analz (sees Spy evs)";
    1.27  by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.28  qed "OR4_analz_sees_Spy";
    1.29  
    1.30  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.31 -\                  : set evs ==> K : parts (sees lost Spy evs)";
    1.32 +\                  : set evs ==> K : parts (sees Spy evs)";
    1.33  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.34  qed "Oops_parts_sees_Spy";
    1.35  
    1.36 @@ -60,40 +60,34 @@
    1.37  bind_thm ("OR4_parts_sees_Spy",
    1.38            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.39  
    1.40 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    1.41 -  We instantiate the variable to "lost" since leaving it as a Var would
    1.42 -  interfere with simplification.*)
    1.43 -val parts_induct_tac = 
    1.44 -    let val tac = forw_inst_tac [("lost","lost")] 
    1.45 -    in  etac otway.induct	   1 THEN 
    1.46 -        tac OR4_parts_sees_Spy     6 THEN
    1.47 -        tac Oops_parts_sees_Spy    7 THEN
    1.48 -	prove_simple_subgoals_tac  1
    1.49 -    end;
    1.50 +(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.51 +fun parts_induct_tac i = 
    1.52 +    etac otway.induct i			THEN 
    1.53 +    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
    1.54 +    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
    1.55 +    prove_simple_subgoals_tac  i;
    1.56  
    1.57  
    1.58 -(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.59 +(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    1.60      sends messages containing X! **)
    1.61  
    1.62  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.63  goal thy 
    1.64 - "!!evs. evs : otway lost \
    1.65 -\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.66 -by parts_induct_tac;
    1.67 + "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.68 +by (parts_induct_tac 1);
    1.69  by (Fake_parts_insert_tac 1);
    1.70  by (Blast_tac 1);
    1.71  qed "Spy_see_shrK";
    1.72  Addsimps [Spy_see_shrK];
    1.73  
    1.74  goal thy 
    1.75 - "!!evs. evs : otway lost \
    1.76 -\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.77 + "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.78  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.79  qed "Spy_analz_shrK";
    1.80  Addsimps [Spy_analz_shrK];
    1.81  
    1.82 -goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.83 -\                  evs : otway lost |] ==> A:lost";
    1.84 +goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
    1.85 +\                  evs : otway |] ==> A:lost";
    1.86  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.87  qed "Spy_see_shrK_D";
    1.88  
    1.89 @@ -102,9 +96,9 @@
    1.90  
    1.91  
    1.92  (*Nobody can have used non-existent keys!*)
    1.93 -goal thy "!!evs. evs : otway lost ==>          \
    1.94 -\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    1.95 -by parts_induct_tac;
    1.96 +goal thy "!!evs. evs : otway ==>          \
    1.97 +\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
    1.98 +by (parts_induct_tac 1);
    1.99  (*Fake*)
   1.100  by (best_tac
   1.101        (!claset addIs [impOfSubs analz_subset_parts]
   1.102 @@ -131,7 +125,7 @@
   1.103  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.104  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.105  \             : set evs;                                            \
   1.106 -\           evs : otway lost |]                                     \
   1.107 +\           evs : otway |]                                     \
   1.108  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   1.109  by (etac rev_mp 1);
   1.110  by (etac otway.induct 1);
   1.111 @@ -140,10 +134,10 @@
   1.112  qed "Says_Server_message_form";
   1.113  
   1.114  
   1.115 -(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.116 +(*For proofs involving analz.*)
   1.117  val analz_sees_tac = 
   1.118 -    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.119 -    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.120 +    dtac OR4_analz_sees_Spy 6 THEN
   1.121 +    forward_tac [Says_Server_message_form] 7 THEN
   1.122      assume_tac 7 THEN
   1.123      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.124  
   1.125 @@ -151,8 +145,8 @@
   1.126  (****
   1.127   The following is to prove theorems of the form
   1.128  
   1.129 -  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   1.130 -  Key K : analz (sees lost Spy evs)
   1.131 +  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   1.132 +  Key K : analz (sees Spy evs)
   1.133  
   1.134   A more general formula must be proved inductively.
   1.135  ****)
   1.136 @@ -162,10 +156,10 @@
   1.137  
   1.138  (*The equality makes the induction hypothesis easier to apply*)
   1.139  goal thy  
   1.140 - "!!evs. evs : otway lost ==>                                    \
   1.141 -\  ALL K KK. KK <= Compl (range shrK) -->                        \
   1.142 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
   1.143 -\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.144 + "!!evs. evs : otway ==>                                    \
   1.145 +\  ALL K KK. KK <= Compl (range shrK) -->                   \
   1.146 +\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
   1.147 +\            (K : KK | Key K : analz (sees Spy evs))";
   1.148  by (etac otway.induct 1);
   1.149  by analz_sees_tac;
   1.150  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.151 @@ -179,9 +173,9 @@
   1.152  
   1.153  
   1.154  goal thy
   1.155 - "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
   1.156 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
   1.157 -\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.158 + "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   1.159 +\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
   1.160 +\        (K = KAB | Key K : analz (sees Spy evs))";
   1.161  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.162  qed "analz_insert_freshK";
   1.163  
   1.164 @@ -189,7 +183,7 @@
   1.165  (*** The Key K uniquely identifies the Server's  message. **)
   1.166  
   1.167  goal thy 
   1.168 - "!!evs. evs : otway lost ==>                              \
   1.169 + "!!evs. evs : otway ==>                                   \
   1.170  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.171  \       Says Server B                                      \
   1.172  \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
   1.173 @@ -218,7 +212,7 @@
   1.174  \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   1.175  \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   1.176  \           : set evs;                                             \
   1.177 -\          evs : otway lost |]                                     \
   1.178 +\          evs : otway |]                                          \
   1.179  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.180  by (prove_unique_tac lemma 1);
   1.181  qed "unique_session_keys";
   1.182 @@ -229,14 +223,14 @@
   1.183  
   1.184  (*If the encrypted message appears then it originated with the Server!*)
   1.185  goal thy 
   1.186 - "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   1.187 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   1.188 -\      : parts (sees lost Spy evs)                          \
   1.189 + "!!evs. [| A ~: lost;  evs : otway |]                 \
   1.190 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}   \
   1.191 +\      : parts (sees Spy evs)                          \
   1.192  \     --> (EX NB. Says Server B                                          \
   1.193  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.194  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.195  \                  : set evs)";
   1.196 -by parts_induct_tac;
   1.197 +by (parts_induct_tac 1);
   1.198  by (Fake_parts_insert_tac 1);
   1.199  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.200  (*OR3*)
   1.201 @@ -249,7 +243,7 @@
   1.202  goal thy 
   1.203   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   1.204  \            : set evs;                                                 \
   1.205 -\           A ~: lost;  evs : otway lost |]                             \
   1.206 +\           A ~: lost;  evs : otway |]                                  \
   1.207  \        ==> EX NB. Says Server B                                       \
   1.208  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   1.209  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.210 @@ -264,13 +258,13 @@
   1.211      the premises, e.g. by having A=Spy **)
   1.212  
   1.213  goal thy 
   1.214 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   1.215 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
   1.216  \        ==> Says Server B                                                 \
   1.217  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   1.218  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   1.219  \            : set evs -->                                                 \
   1.220  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
   1.221 -\            Key K ~: analz (sees lost Spy evs)";
   1.222 +\            Key K ~: analz (sees Spy evs)";
   1.223  by (etac otway.induct 1);
   1.224  by analz_sees_tac;
   1.225  by (ALLGOALS
   1.226 @@ -295,8 +289,8 @@
   1.227  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.228  \             : set evs;                                            \
   1.229  \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   1.230 -\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.231 -\        ==> Key K ~: analz (sees lost Spy evs)";
   1.232 +\           A ~: lost;  B ~: lost;  evs : otway |]                  \
   1.233 +\        ==> Key K ~: analz (sees Spy evs)";
   1.234  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.235  by (blast_tac (!claset addSEs [lemma]) 1);
   1.236  qed "Spy_not_see_encrypted_key";
   1.237 @@ -306,14 +300,14 @@
   1.238  
   1.239  (*If the encrypted message appears then it originated with the Server!*)
   1.240  goal thy 
   1.241 - "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   1.242 -\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   1.243 -\         : parts (sees lost Spy evs)                                       \
   1.244 + "!!evs. [| B ~: lost;  evs : otway |]                                 \
   1.245 +\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                \
   1.246 +\         : parts (sees Spy evs)                                       \
   1.247  \        --> (EX NA. Says Server B                                          \
   1.248  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.249  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.250  \                     : set evs)";
   1.251 -by parts_induct_tac;
   1.252 +by (parts_induct_tac 1);
   1.253  by (Fake_parts_insert_tac 1);
   1.254  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.255  (*OR3*)
   1.256 @@ -324,7 +318,7 @@
   1.257  (*Guarantee for B: if it gets a well-formed certificate then the Server
   1.258    has sent the correct message in round 3.*)
   1.259  goal thy 
   1.260 - "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   1.261 + "!!evs. [| B ~: lost;  evs : otway;                                        \
   1.262  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.263  \            : set evs |]                                                   \
   1.264  \        ==> EX NA. Says Server B                                           \