src/HOL/Auth/WooLam.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11251 a6816d47f41d
child 14207 f20fbb141673
permissions -rw-r--r--
tidying of 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@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@13507
    90
apply (erule woolam.induct, force, simp_all, blast+)
paulson@11251
    91
done
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@13507
   111
apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
paulson@11251
   112
done
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@13507
   133
apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
paulson@11251
   134
done
paulson@11251
   135
paulson@11251
   136
(*If the encrypted message appears then it originated with the Server!*)
paulson@11251
   137
lemma NB_Crypt_imp_Server_msg [rule_format]:
paulson@11251
   138
     "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
paulson@11251
   139
         B \<notin> bad;  evs \<in> woolam |]
paulson@11251
   140
      ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
paulson@13507
   141
apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
paulson@11251
   142
done
paulson@11251
   143
paulson@11251
   144
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
paulson@11251
   145
  the nonce using her key.  This event can be no older than the nonce itself.
paulson@11251
   146
  But A may have sent the nonce to some other agent and it could have reached
paulson@11251
   147
  the Server via the Spy.*)
paulson@11251
   148
lemma B_trusts_WL5:
paulson@11251
   149
     "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
paulson@11251
   150
         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
paulson@11251
   151
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@11251
   152
by (blast dest!: NB_Crypt_imp_Server_msg)
paulson@11251
   153
paulson@11251
   154
paulson@11251
   155
(*B only issues challenges in response to WL1.  Not used.*)
paulson@11251
   156
lemma B_said_WL2:
paulson@11251
   157
     "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
paulson@11251
   158
      ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
paulson@13507
   159
apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
paulson@11251
   160
done
paulson@11251
   161
paulson@11251
   162
paulson@11251
   163
(**CANNOT be proved because A doesn't know where challenges come from...*)
paulson@11251
   164
lemma "[| A \<notin> bad;  B \<noteq> Spy;  evs \<in> woolam |]
paulson@11251
   165
  ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
paulson@11251
   166
      Says B A (Nonce NB) \<in> set evs
paulson@11251
   167
      --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
paulson@13507
   168
apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
paulson@11251
   169
oops
paulson@2274
   170
paulson@2274
   171
end