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