src/HOL/Auth/WooLam.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 16417 9bc16273c2d4
child 23746 a455e69c31cc
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:      HOL/Auth/WooLam
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header{*The Woo-Lam Protocol*}
     8 
     9 theory WooLam imports Public begin
    10 
    11 text{*Simplified version from page 11 of
    12   Abadi and Needham (1996). 
    13   Prudent Engineering Practice for Cryptographic Protocols.
    14   IEEE Trans. S.E. 22(1), pages 6-15.
    15 
    16 Note: this differs from the Woo-Lam protocol discussed by Lowe (1996):
    17   Some New Attacks upon Security Protocols.
    18   Computer Security Foundations Workshop
    19 *}
    20 
    21 consts  woolam  :: "event list set"
    22 inductive woolam
    23   intros
    24          (*Initial trace is empty*)
    25    Nil:  "[] \<in> woolam"
    26 
    27          (** These rules allow agents to send messages to themselves **)
    28 
    29          (*The spy MAY say anything he CAN say.  We do not expect him to
    30            invent new nonces here, but he can also use NS1.  Common to
    31            all similar protocols.*)
    32    Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
    33           ==> Says Spy B X  # evsf \<in> woolam"
    34 
    35          (*Alice initiates a protocol run*)
    36    WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
    37 
    38          (*Bob responds to Alice's message with a challenge.*)
    39    WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
    40           ==> Says B A (Nonce NB) # evs2 \<in> woolam"
    41 
    42          (*Alice responds to Bob's challenge by encrypting NB with her key.
    43            B is *not* properly determined -- Alice essentially broadcasts
    44            her reply.*)
    45    WL3:  "[| evs3 \<in> woolam;
    46              Says A  B (Agent A)  \<in> set evs3;
    47              Says B' A (Nonce NB) \<in> set evs3 |]
    48           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
    49 
    50          (*Bob forwards Alice's response to the Server.  NOTE: usually
    51            the messages are shown in chronological order, for clarity.
    52            But here, exchanging the two events would cause the lemma
    53            WL4_analz_spies to pick up the wrong assumption!*)
    54    WL4:  "[| evs4 \<in> woolam;
    55              Says A'  B X         \<in> set evs4;
    56              Says A'' B (Agent A) \<in> set evs4 |]
    57           ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
    58 
    59          (*Server decrypts Alice's response for Bob.*)
    60    WL5:  "[| evs5 \<in> woolam;
    61              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    62                \<in> set evs5 |]
    63           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    64                  # evs5 \<in> woolam"
    65 
    66 
    67 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    68 declare parts.Body  [dest]
    69 declare analz_into_parts [dest]
    70 declare Fake_parts_insert_in_Un  [dest]
    71 
    72 
    73 (*A "possibility property": there are traces that reach the end*)
    74 lemma "\<exists>NB. \<exists>evs \<in> woolam.
    75              Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \<in> set evs"
    76 apply (intro exI bexI)
    77 apply (rule_tac [2] woolam.Nil
    78                     [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
    79                      THEN woolam.WL4, THEN woolam.WL5], possibility)
    80 done
    81 
    82 (*Could prove forwarding lemmas for WL4, but we do not need them!*)
    83 
    84 (**** Inductive proofs about woolam ****)
    85 
    86 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    87     sends messages containing X! **)
    88 
    89 (*Spy never sees a good agent's shared key!*)
    90 lemma Spy_see_shrK [simp]:
    91      "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    92 by (erule woolam.induct, force, simp_all, blast+)
    93 
    94 lemma Spy_analz_shrK [simp]:
    95      "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
    96 by auto
    97 
    98 lemma Spy_see_shrK_D [dest!]:
    99      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> woolam|] ==> A \<in> bad"
   100 by (blast dest: Spy_see_shrK)
   101 
   102 
   103 (**** Autheticity properties for Woo-Lam ****)
   104 
   105 (*** WL4 ***)
   106 
   107 (*If the encrypted message appears then it originated with Alice*)
   108 lemma NB_Crypt_imp_Alice_msg:
   109      "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
   110          A \<notin> bad;  evs \<in> woolam |]
   111       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   112 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   113 
   114 (*Guarantee for Server: if it gets a message containing a certificate from
   115   Alice, then she originated that certificate.  But we DO NOT know that B
   116   ever saw it: the Spy may have rerouted the message to the Server.*)
   117 lemma Server_trusts_WL4 [dest]:
   118      "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
   119            \<in> set evs;
   120          A \<notin> bad;  evs \<in> woolam |]
   121       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   122 by (blast intro!: NB_Crypt_imp_Alice_msg)
   123 
   124 
   125 (*** WL5 ***)
   126 
   127 (*Server sent WL5 only if it received the right sort of message*)
   128 lemma Server_sent_WL5 [dest]:
   129      "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
   130          evs \<in> woolam |]
   131       ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
   132              \<in> set evs"
   133 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   134 
   135 (*If the encrypted message appears then it originated with the Server!*)
   136 lemma NB_Crypt_imp_Server_msg [rule_format]:
   137      "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
   138          B \<notin> bad;  evs \<in> woolam |]
   139       ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
   140 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   141 
   142 (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   143   the nonce using her key.  This event can be no older than the nonce itself.
   144   But A may have sent the nonce to some other agent and it could have reached
   145   the Server via the Spy.*)
   146 lemma B_trusts_WL5:
   147      "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
   148          A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
   149       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   150 by (blast dest!: NB_Crypt_imp_Server_msg)
   151 
   152 
   153 (*B only issues challenges in response to WL1.  Not used.*)
   154 lemma B_said_WL2:
   155      "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
   156       ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
   157 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   158 
   159 
   160 (**CANNOT be proved because A doesn't know where challenges come from...*)
   161 lemma "[| A \<notin> bad;  B \<noteq> Spy;  evs \<in> woolam |]
   162   ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
   163       Says B A (Nonce NB) \<in> set evs
   164       --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   165 apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
   166 oops
   167 
   168 end