Swapping arguments of Crypt; removing argument lost
authorpaulson
Fri Nov 29 17:58:18 1996 +0100 (1996-11-29)
changeset 228368829cf138fc
parent 2282 90fb68d597f8
child 2284 80ebd1a213fd
Swapping arguments of Crypt; removing argument lost
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
     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
     2.1 --- a/src/HOL/Auth/WooLam.thy	Fri Nov 29 15:31:13 1996 +0100
     2.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Nov 29 17:58:18 1996 +0100
     2.3 @@ -16,47 +16,48 @@
     2.4  
     2.5  WooLam = Shared + 
     2.6  
     2.7 -consts  woolam   :: "agent set => event list set"
     2.8 -inductive "woolam lost"
     2.9 +consts  lost    :: agent set        (*No need for it to be a variable*)
    2.10 +	woolam  :: event list set
    2.11 +inductive woolam
    2.12    intrs 
    2.13           (*Initial trace is empty*)
    2.14 -    Nil  "[]: woolam lost"
    2.15 +    Nil  "[]: woolam"
    2.16  
    2.17           (*The spy MAY say anything he CAN say.  We do not expect him to
    2.18             invent new nonces here, but he can also use NS1.  Common to
    2.19             all similar protocols.*)
    2.20 -    Fake "[| evs: woolam lost;  B ~= Spy;  
    2.21 +    Fake "[| evs: woolam;  B ~= Spy;  
    2.22               X: synth (analz (sees lost Spy evs)) |]
    2.23 -          ==> Says Spy B X  # evs : woolam lost"
    2.24 +          ==> Says Spy B X  # evs : woolam"
    2.25  
    2.26           (*Alice initiates a protocol run*)
    2.27 -    WL1  "[| evs: woolam lost;  A ~= B |]
    2.28 -          ==> Says A B (Agent A) # evs : woolam lost"
    2.29 +    WL1  "[| evs: woolam;  A ~= B |]
    2.30 +          ==> Says A B (Agent A) # evs : woolam"
    2.31  
    2.32           (*Bob responds to Alice's message with a challenge.*)
    2.33 -    WL2  "[| evs: woolam lost;  A ~= B;
    2.34 +    WL2  "[| evs: woolam;  A ~= B;
    2.35               Says A' B (Agent A) : set_of_list evs |]
    2.36 -          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
    2.37 +          ==> Says B A (Nonce (newN evs)) # evs : woolam"
    2.38  
    2.39           (*Alice responds to Bob's challenge by encrypting NB with her key.
    2.40             B is *not* properly determined -- Alice essentially broadcasts
    2.41             her reply.*)
    2.42 -    WL3  "[| evs: woolam lost;  A ~= B;
    2.43 +    WL3  "[| evs: woolam;  A ~= B;
    2.44               Says B' A (Nonce NB) : set_of_list evs;
    2.45               Says A  B (Agent A)  : set_of_list evs |]
    2.46 -          ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
    2.47 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    2.48  
    2.49           (*Bob forwards Alice's response to the Server.*)
    2.50 -    WL4  "[| evs: woolam lost;  B ~= Server;  
    2.51 +    WL4  "[| evs: woolam;  B ~= Server;  
    2.52               Says A'  B X         : set_of_list evs;
    2.53               Says A'' B (Agent A) : set_of_list evs |]
    2.54 -          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
    2.55 +          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    2.56  
    2.57           (*Server decrypts Alice's response for Bob.*)
    2.58 -    WL5  "[| evs: woolam lost;  B ~= Server;
    2.59 -             Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
    2.60 +    WL5  "[| evs: woolam;  B ~= Server;
    2.61 +             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    2.62                 : set_of_list evs |]
    2.63 -          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
    2.64 -                 # evs : woolam lost"
    2.65 +          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    2.66 +                 # evs : woolam"
    2.67  
    2.68  end