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