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
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
Inductive relation "woolam" for the Woo-Lam protocol.
paulson@2274
     7
paulson@2274
     8
Simplified version from page 11 of
paulson@2274
     9
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
paulson@2274
    10
  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
paulson@2274
    11
paulson@2274
    12
Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
paulson@2274
    13
  Some New Attacks upon Security Protocols.
paulson@2274
    14
  Computer Security Foundations Workshop, 1996.
paulson@2274
    15
*)
paulson@2274
    16
paulson@11251
    17
theory WooLam = Shared:
paulson@2274
    18
paulson@11251
    19
consts  woolam  :: "event list set"
paulson@2283
    20
inductive woolam
paulson@11251
    21
  intros
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.*)
paulson@11251
    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*)
paulson@11251
    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.*)
paulson@11251
    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.*)
paulson@11251
    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!*)
paulson@11251
    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.*)
paulson@11251
    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@11251
    77
                     THEN woolam.WL4, THEN woolam.WL5])
paulson@11251
    78
apply 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@11251
    91
apply (erule woolam.induct, force, simp_all)
paulson@11251
    92
apply blast+
paulson@11251
    93
done
paulson@11251
    94
paulson@11251
    95
lemma Spy_analz_shrK [simp]:
paulson@11251
    96
     "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@11251
    97
by auto
paulson@11251
    98
paulson@11251
    99
lemma Spy_see_shrK_D [dest!]:
paulson@11251
   100
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> woolam|] ==> A \<in> bad"
paulson@11251
   101
by (blast dest: Spy_see_shrK)
paulson@11251
   102
paulson@11251
   103
paulson@11251
   104
(**** Autheticity properties for Woo-Lam ****)
paulson@11251
   105
paulson@11251
   106
(*** WL4 ***)
paulson@11251
   107
paulson@11251
   108
(*If the encrypted message appears then it originated with Alice*)
paulson@11251
   109
lemma NB_Crypt_imp_Alice_msg:
paulson@11251
   110
     "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
paulson@11251
   111
         A \<notin> bad;  evs \<in> woolam |]
paulson@11251
   112
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@11251
   113
apply (erule rev_mp, erule woolam.induct, force, simp_all)
paulson@11251
   114
apply blast+
paulson@11251
   115
done
paulson@11251
   116
paulson@11251
   117
(*Guarantee for Server: if it gets a message containing a certificate from
paulson@11251
   118
  Alice, then she originated that certificate.  But we DO NOT know that B
paulson@11251
   119
  ever saw it: the Spy may have rerouted the message to the Server.*)
paulson@11251
   120
lemma Server_trusts_WL4 [dest]:
paulson@11251
   121
     "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
paulson@11251
   122
           \<in> set evs;
paulson@11251
   123
         A \<notin> bad;  evs \<in> woolam |]
paulson@11251
   124
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@11251
   125
by (blast intro!: NB_Crypt_imp_Alice_msg)
paulson@11251
   126
paulson@11251
   127
paulson@11251
   128
(*** WL5 ***)
paulson@11251
   129
paulson@11251
   130
(*Server sent WL5 only if it received the right sort of message*)
paulson@11251
   131
lemma Server_sent_WL5 [dest]:
paulson@11251
   132
     "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
paulson@11251
   133
         evs \<in> woolam |]
paulson@11251
   134
      ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
paulson@11251
   135
             \<in> set evs"
paulson@11251
   136
apply (erule rev_mp, erule woolam.induct, force, simp_all)
paulson@11251
   137
apply blast+
paulson@11251
   138
done
paulson@11251
   139
paulson@11251
   140
(*If the encrypted message appears then it originated with the Server!*)
paulson@11251
   141
lemma NB_Crypt_imp_Server_msg [rule_format]:
paulson@11251
   142
     "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
paulson@11251
   143
         B \<notin> bad;  evs \<in> woolam |]
paulson@11251
   144
      ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
paulson@11251
   145
apply (erule rev_mp, erule woolam.induct, force, simp_all)
paulson@11251
   146
apply blast+
paulson@11251
   147
done
paulson@11251
   148
paulson@11251
   149
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
paulson@11251
   150
  the nonce using her key.  This event can be no older than the nonce itself.
paulson@11251
   151
  But A may have sent the nonce to some other agent and it could have reached
paulson@11251
   152
  the Server via the Spy.*)
paulson@11251
   153
lemma B_trusts_WL5:
paulson@11251
   154
     "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
paulson@11251
   155
         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
paulson@11251
   156
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@11251
   157
by (blast dest!: NB_Crypt_imp_Server_msg)
paulson@11251
   158
paulson@11251
   159
paulson@11251
   160
(*B only issues challenges in response to WL1.  Not used.*)
paulson@11251
   161
lemma B_said_WL2:
paulson@11251
   162
     "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
paulson@11251
   163
      ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
paulson@11251
   164
apply (erule rev_mp, erule woolam.induct, force, simp_all)
paulson@11251
   165
apply blast+
paulson@11251
   166
done
paulson@11251
   167
paulson@11251
   168
paulson@11251
   169
(**CANNOT be proved because A doesn't know where challenges come from...*)
paulson@11251
   170
lemma "[| A \<notin> bad;  B \<noteq> Spy;  evs \<in> woolam |]
paulson@11251
   171
  ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
paulson@11251
   172
      Says B A (Nonce NB) \<in> set evs
paulson@11251
   173
      --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@11251
   174
apply (erule rev_mp, erule woolam.induct, force, simp_all)
paulson@11251
   175
apply blast
paulson@11251
   176
apply auto
paulson@11251
   177
oops
paulson@2274
   178
paulson@2274
   179
end