src/HOL/Auth/WooLam.ML
changeset 2283 68829cf138fc
parent 2274 1b1b46adc9b3
child 2321 083912bc5775
     1.1 --- a/src/HOL/Auth/WooLam.ML	Fri Nov 29 15:31:13 1996 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Nov 29 17:58:18 1996 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4  (*Weak liveness: there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.7 -\        ==> EX NB. EX evs: woolam lost.          \
     1.8 -\               Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) \
     1.9 +\        ==> EX NB. EX evs: woolam.               \
    1.10 +\               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
    1.11  \                 : set_of_list evs";
    1.12  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.13  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    1.14 @@ -35,7 +35,7 @@
    1.15  (**** Inductive proofs about woolam ****)
    1.16  
    1.17  (*Nobody sends themselves messages*)
    1.18 -goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.19 +goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
    1.20  by (etac woolam.induct 1);
    1.21  by (Auto_tac());
    1.22  qed_spec_mp "not_Says_to_self";
    1.23 @@ -53,9 +53,7 @@
    1.24  bind_thm ("WL4_parts_sees_Spy",
    1.25            WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.26  
    1.27 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    1.28 -  harder to complete, since simplification does less for us.*)
    1.29 -val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6;
    1.30 +val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
    1.31  
    1.32  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.33  fun parts_induct_tac i = SELECT_GOAL
    1.34 @@ -73,7 +71,7 @@
    1.35  
    1.36  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.37  goal thy 
    1.38 - "!!evs. evs : woolam lost \
    1.39 + "!!evs. evs : woolam \
    1.40  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.41  by (parts_induct_tac 1);
    1.42  by (Auto_tac());
    1.43 @@ -81,14 +79,14 @@
    1.44  Addsimps [Spy_see_shrK];
    1.45  
    1.46  goal thy 
    1.47 - "!!evs. evs : woolam lost \
    1.48 + "!!evs. evs : woolam \
    1.49  \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.50  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.51  qed "Spy_analz_shrK";
    1.52  Addsimps [Spy_analz_shrK];
    1.53  
    1.54  goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.55 -\                  evs : woolam lost |] ==> A:lost";
    1.56 +\                  evs : woolam |] ==> A:lost";
    1.57  by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.58  qed "Spy_see_shrK_D";
    1.59  
    1.60 @@ -98,7 +96,7 @@
    1.61  
    1.62  (*** Future nonces can't be seen or used! ***)
    1.63  
    1.64 -goal thy "!!evs. evs : woolam lost ==> \
    1.65 +goal thy "!!evs. evs : woolam ==> \
    1.66  \                length evs <= length evt --> \
    1.67  \                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.68  by (parts_induct_tac 1);
    1.69 @@ -121,9 +119,9 @@
    1.70  
    1.71  (*If the encrypted message appears then it originated with Alice*)
    1.72  goal thy 
    1.73 - "!!evs. [| A ~: lost;  evs : woolam lost |]                   \
    1.74 -\    ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs)        \
    1.75 -\        --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)";
    1.76 + "!!evs. [| A ~: lost;  evs : woolam |]                   \
    1.77 +\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
    1.78 +\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
    1.79  by (parts_induct_tac 1);
    1.80  by (Fast_tac 1);
    1.81  qed_spec_mp "NB_Crypt_imp_Alice_msg";
    1.82 @@ -132,10 +130,10 @@
    1.83    Alice, then she originated that certificate.  But we DO NOT know that B
    1.84    ever saw it: the Spy may have rerouted the message to the Server.*)
    1.85  goal thy 
    1.86 - "!!evs. [| A ~: lost;  evs : woolam lost;               \
    1.87 -\           Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \
    1.88 + "!!evs. [| A ~: lost;  evs : woolam;               \
    1.89 +\           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
    1.90  \            : set_of_list evs |]                                  \
    1.91 -\        ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
    1.92 +\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
    1.93  by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
    1.94                        addSEs [MPair_parts]
    1.95                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.96 @@ -146,9 +144,9 @@
    1.97  
    1.98  (*Server sent WL5 only if it received the right sort of message*)
    1.99  goal thy 
   1.100 - "!!evs. evs : woolam lost ==>                                              \
   1.101 -\        Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs   \
   1.102 -\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \
   1.103 + "!!evs. evs : woolam ==>                                              \
   1.104 +\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
   1.105 +\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   1.106  \               : set_of_list evs)";
   1.107  by (parts_induct_tac 1);
   1.108  by (ALLGOALS Fast_tac);
   1.109 @@ -157,18 +155,18 @@
   1.110  
   1.111  (*If the encrypted message appears then it originated with the Server!*)
   1.112  goal thy 
   1.113 - "!!evs. [| B ~: lost;  evs : woolam lost |]                   \
   1.114 -\    ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs)        \
   1.115 -\        --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
   1.116 + "!!evs. [| B ~: lost;  evs : woolam |]                   \
   1.117 +\    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   1.118 +\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   1.119  by (parts_induct_tac 1);
   1.120  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.121  
   1.122  (*Partial guarantee for B: if it gets a message of correct form then the Server
   1.123    sent the same message.*)
   1.124  goal thy 
   1.125 - "!!evs. [| Says S B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs; \
   1.126 -\           B ~: lost;  evs : woolam lost |]                                  \
   1.127 -\        ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
   1.128 + "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
   1.129 +\           B ~: lost;  evs : woolam |]                                  \
   1.130 +\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   1.131  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.132                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.133  qed "B_got_WL5";
   1.134 @@ -178,9 +176,9 @@
   1.135    But A may have sent the nonce to some other agent and it could have reached
   1.136    the Server via the Spy.*)
   1.137  goal thy 
   1.138 - "!!evs. [| Says S B (Crypt {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \
   1.139 -\           A ~: lost;  B ~: lost;  evs : woolam lost  |] \
   1.140 -\        ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
   1.141 + "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
   1.142 +\           A ~: lost;  B ~: lost;  evs : woolam  |] \
   1.143 +\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   1.144  by (fast_tac (!claset addIs  [Server_trust_WL4]
   1.145                        addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   1.146  qed "B_trust_WL5";
   1.147 @@ -188,7 +186,7 @@
   1.148  
   1.149  (*B only issues challenges in response to WL1.  Useful??*)
   1.150  goal thy 
   1.151 - "!!evs. [| B ~= Spy;  evs : woolam lost |]                   \
   1.152 + "!!evs. [| B ~= Spy;  evs : woolam |]                   \
   1.153  \    ==> Says B A (Nonce NB) : set_of_list evs        \
   1.154  \        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
   1.155  by (parts_induct_tac 1);
   1.156 @@ -198,10 +196,10 @@
   1.157  
   1.158  (**CANNOT be proved because A doesn't know where challenges come from...
   1.159  goal thy 
   1.160 - "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam lost |]                   \
   1.161 -\    ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) &  \
   1.162 + "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
   1.163 +\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
   1.164  \        Says B A (Nonce NB) : set_of_list evs        \
   1.165 -\        --> Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
   1.166 +\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   1.167  by (parts_induct_tac 1);
   1.168  by (Step_tac 1);
   1.169  by (best_tac (!claset addSEs partsEs