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