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