src/HOL/Auth/WooLam.thy
changeset 11251 a6816d47f41d
parent 11185 1b737b4c2108
child 13507 febb8e5d2a9d
     1.1 --- a/src/HOL/Auth/WooLam.thy	Wed Apr 11 11:53:54 2001 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Apr 12 12:45:05 2001 +0200
     1.3 @@ -14,52 +14,166 @@
     1.4    Computer Security Foundations Workshop, 1996.
     1.5  *)
     1.6  
     1.7 -WooLam = Shared + 
     1.8 +theory WooLam = Shared:
     1.9  
    1.10 -consts  woolam  :: event list set
    1.11 +consts  woolam  :: "event list set"
    1.12  inductive woolam
    1.13 -  intrs 
    1.14 +  intros
    1.15           (*Initial trace is empty*)
    1.16 -    Nil  "[] \\<in> woolam"
    1.17 +   Nil:  "[] \<in> woolam"
    1.18  
    1.19           (** These rules allow agents to send messages to themselves **)
    1.20  
    1.21           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.22             invent new nonces here, but he can also use NS1.  Common to
    1.23             all similar protocols.*)
    1.24 -    Fake "[| evsf \\<in> woolam;  X \\<in> synth (analz (spies evsf)) |]
    1.25 -          ==> Says Spy B X  # evsf \\<in> woolam"
    1.26 +   Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
    1.27 +          ==> Says Spy B X  # evsf \<in> woolam"
    1.28  
    1.29           (*Alice initiates a protocol run*)
    1.30 -    WL1  "[| evs1 \\<in> woolam |]
    1.31 -          ==> Says A B (Agent A) # evs1 \\<in> woolam"
    1.32 +   WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
    1.33  
    1.34           (*Bob responds to Alice's message with a challenge.*)
    1.35 -    WL2  "[| evs2 \\<in> woolam;  Says A' B (Agent A) \\<in> set evs2 |]
    1.36 -          ==> Says B A (Nonce NB) # evs2 \\<in> woolam"
    1.37 +   WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
    1.38 +          ==> Says B A (Nonce NB) # evs2 \<in> woolam"
    1.39  
    1.40           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.41             B is *not* properly determined -- Alice essentially broadcasts
    1.42             her reply.*)
    1.43 -    WL3  "[| evs3 \\<in> woolam;
    1.44 -             Says A  B (Agent A)  \\<in> set evs3;
    1.45 -             Says B' A (Nonce NB) \\<in> set evs3 |]
    1.46 -          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\<in> woolam"
    1.47 +   WL3:  "[| evs3 \<in> woolam;
    1.48 +             Says A  B (Agent A)  \<in> set evs3;
    1.49 +             Says B' A (Nonce NB) \<in> set evs3 |]
    1.50 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
    1.51  
    1.52           (*Bob forwards Alice's response to the Server.  NOTE: usually
    1.53             the messages are shown in chronological order, for clarity.
    1.54             But here, exchanging the two events would cause the lemma
    1.55             WL4_analz_spies to pick up the wrong assumption!*)
    1.56 -    WL4  "[| evs4 \\<in> woolam;  
    1.57 -             Says A'  B X         \\<in> set evs4;
    1.58 -             Says A'' B (Agent A) \\<in> set evs4 |]
    1.59 -          ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\<in> woolam"
    1.60 +   WL4:  "[| evs4 \<in> woolam;
    1.61 +             Says A'  B X         \<in> set evs4;
    1.62 +             Says A'' B (Agent A) \<in> set evs4 |]
    1.63 +          ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
    1.64  
    1.65           (*Server decrypts Alice's response for Bob.*)
    1.66 -    WL5  "[| evs5 \\<in> woolam;  
    1.67 +   WL5:  "[| evs5 \<in> woolam;
    1.68               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.69 -               \\<in> set evs5 |]
    1.70 +               \<in> set evs5 |]
    1.71            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    1.72 -                 # evs5 \\<in> woolam"
    1.73 +                 # evs5 \<in> woolam"
    1.74 +
    1.75 +
    1.76 +declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    1.77 +declare parts.Body  [dest]
    1.78 +declare analz_into_parts [dest]
    1.79 +declare Fake_parts_insert_in_Un  [dest]
    1.80 +
    1.81 +
    1.82 +(*A "possibility property": there are traces that reach the end*)
    1.83 +lemma "\<exists>NB. \<exists>evs \<in> woolam.
    1.84 +             Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \<in> set evs"
    1.85 +apply (intro exI bexI)
    1.86 +apply (rule_tac [2] woolam.Nil
    1.87 +                    [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
    1.88 +                     THEN woolam.WL4, THEN woolam.WL5])
    1.89 +apply possibility
    1.90 +done
    1.91 +
    1.92 +(*Could prove forwarding lemmas for WL4, but we do not need them!*)
    1.93 +
    1.94 +(**** Inductive proofs about woolam ****)
    1.95 +
    1.96 +(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    1.97 +    sends messages containing X! **)
    1.98 +
    1.99 +(*Spy never sees a good agent's shared key!*)
   1.100 +lemma Spy_see_shrK [simp]:
   1.101 +     "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   1.102 +apply (erule woolam.induct, force, simp_all)
   1.103 +apply blast+
   1.104 +done
   1.105 +
   1.106 +lemma Spy_analz_shrK [simp]:
   1.107 +     "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   1.108 +by auto
   1.109 +
   1.110 +lemma Spy_see_shrK_D [dest!]:
   1.111 +     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> woolam|] ==> A \<in> bad"
   1.112 +by (blast dest: Spy_see_shrK)
   1.113 +
   1.114 +
   1.115 +(**** Autheticity properties for Woo-Lam ****)
   1.116 +
   1.117 +(*** WL4 ***)
   1.118 +
   1.119 +(*If the encrypted message appears then it originated with Alice*)
   1.120 +lemma NB_Crypt_imp_Alice_msg:
   1.121 +     "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
   1.122 +         A \<notin> bad;  evs \<in> woolam |]
   1.123 +      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   1.124 +apply (erule rev_mp, erule woolam.induct, force, simp_all)
   1.125 +apply blast+
   1.126 +done
   1.127 +
   1.128 +(*Guarantee for Server: if it gets a message containing a certificate from
   1.129 +  Alice, then she originated that certificate.  But we DO NOT know that B
   1.130 +  ever saw it: the Spy may have rerouted the message to the Server.*)
   1.131 +lemma Server_trusts_WL4 [dest]:
   1.132 +     "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
   1.133 +           \<in> set evs;
   1.134 +         A \<notin> bad;  evs \<in> woolam |]
   1.135 +      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   1.136 +by (blast intro!: NB_Crypt_imp_Alice_msg)
   1.137 +
   1.138 +
   1.139 +(*** WL5 ***)
   1.140 +
   1.141 +(*Server sent WL5 only if it received the right sort of message*)
   1.142 +lemma Server_sent_WL5 [dest]:
   1.143 +     "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
   1.144 +         evs \<in> woolam |]
   1.145 +      ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
   1.146 +             \<in> set evs"
   1.147 +apply (erule rev_mp, erule woolam.induct, force, simp_all)
   1.148 +apply blast+
   1.149 +done
   1.150 +
   1.151 +(*If the encrypted message appears then it originated with the Server!*)
   1.152 +lemma NB_Crypt_imp_Server_msg [rule_format]:
   1.153 +     "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
   1.154 +         B \<notin> bad;  evs \<in> woolam |]
   1.155 +      ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
   1.156 +apply (erule rev_mp, erule woolam.induct, force, simp_all)
   1.157 +apply blast+
   1.158 +done
   1.159 +
   1.160 +(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   1.161 +  the nonce using her key.  This event can be no older than the nonce itself.
   1.162 +  But A may have sent the nonce to some other agent and it could have reached
   1.163 +  the Server via the Spy.*)
   1.164 +lemma B_trusts_WL5:
   1.165 +     "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
   1.166 +         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
   1.167 +      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   1.168 +by (blast dest!: NB_Crypt_imp_Server_msg)
   1.169 +
   1.170 +
   1.171 +(*B only issues challenges in response to WL1.  Not used.*)
   1.172 +lemma B_said_WL2:
   1.173 +     "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
   1.174 +      ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
   1.175 +apply (erule rev_mp, erule woolam.induct, force, simp_all)
   1.176 +apply blast+
   1.177 +done
   1.178 +
   1.179 +
   1.180 +(**CANNOT be proved because A doesn't know where challenges come from...*)
   1.181 +lemma "[| A \<notin> bad;  B \<noteq> Spy;  evs \<in> woolam |]
   1.182 +  ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
   1.183 +      Says B A (Nonce NB) \<in> set evs
   1.184 +      --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   1.185 +apply (erule rev_mp, erule woolam.induct, force, simp_all)
   1.186 +apply blast
   1.187 +apply auto
   1.188 +oops
   1.189  
   1.190  end