src/HOL/Auth/WooLam.ML
author paulson
Fri Jan 17 12:49:31 1997 +0100 (1997-01-17)
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 2637 e9b203f854ae
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
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
paulson@2274
    13
open WooLam;
paulson@2274
    14
paulson@2274
    15
proof_timing:=true;
paulson@2274
    16
HOL_quantifiers := false;
paulson@2274
    17
Pretty.setdepth 20;
paulson@2274
    18
paulson@2274
    19
paulson@2321
    20
(*A "possibility property": there are traces that reach the end*)
paulson@2274
    21
goal thy 
paulson@2274
    22
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
paulson@2283
    23
\        ==> EX NB. EX evs: woolam.               \
paulson@2283
    24
\               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
paulson@2274
    25
\                 : set_of_list evs";
paulson@2274
    26
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2274
    27
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
paulson@2516
    28
          woolam.WL4 RS woolam.WL5) 2);
paulson@2274
    29
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
paulson@2274
    30
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
paulson@2516
    31
by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
paulson@2516
    32
                                    addss (!simpset setsolver safe_solver))));
paulson@2274
    33
result();
paulson@2274
    34
paulson@2274
    35
paulson@2274
    36
(**** Inductive proofs about woolam ****)
paulson@2274
    37
paulson@2274
    38
(*Nobody sends themselves messages*)
paulson@2283
    39
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
paulson@2274
    40
by (etac woolam.induct 1);
paulson@2274
    41
by (Auto_tac());
paulson@2274
    42
qed_spec_mp "not_Says_to_self";
paulson@2274
    43
Addsimps [not_Says_to_self];
paulson@2274
    44
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@2274
    45
paulson@2274
    46
paulson@2274
    47
(** For reasoning about the encrypted portion of messages **)
paulson@2274
    48
paulson@2274
    49
goal thy "!!evs. Says A' B X : set_of_list evs \
paulson@2274
    50
\                ==> X : analz (sees lost Spy evs)";
paulson@2274
    51
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
paulson@2274
    52
qed "WL4_analz_sees_Spy";
paulson@2274
    53
paulson@2274
    54
bind_thm ("WL4_parts_sees_Spy",
paulson@2274
    55
          WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
paulson@2274
    56
paulson@2283
    57
val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
paulson@2274
    58
paulson@2274
    59
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
paulson@2274
    60
fun parts_induct_tac i = SELECT_GOAL
paulson@2274
    61
    (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
paulson@2274
    62
             (*Fake message*)
paulson@2274
    63
             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@2274
    64
                                           impOfSubs Fake_parts_insert]
paulson@2274
    65
                                    addss (!simpset)) 2)) THEN
paulson@2274
    66
     (*Base case*)
paulson@2274
    67
     fast_tac (!claset addss (!simpset)) 1 THEN
paulson@2274
    68
     ALLGOALS Asm_simp_tac) i;
paulson@2274
    69
paulson@2274
    70
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@2274
    71
    sends messages containing X! **)
paulson@2274
    72
paulson@2274
    73
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
paulson@2274
    74
goal thy 
paulson@2283
    75
 "!!evs. evs : woolam \
paulson@2274
    76
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@2274
    77
by (parts_induct_tac 1);
paulson@2274
    78
by (Auto_tac());
paulson@2274
    79
qed "Spy_see_shrK";
paulson@2274
    80
Addsimps [Spy_see_shrK];
paulson@2274
    81
paulson@2274
    82
goal thy 
paulson@2283
    83
 "!!evs. evs : woolam \
paulson@2274
    84
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@2274
    85
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@2274
    86
qed "Spy_analz_shrK";
paulson@2274
    87
Addsimps [Spy_analz_shrK];
paulson@2274
    88
paulson@2274
    89
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
paulson@2283
    90
\                  evs : woolam |] ==> A:lost";
paulson@2274
    91
by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
paulson@2274
    92
qed "Spy_see_shrK_D";
paulson@2274
    93
paulson@2274
    94
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
paulson@2274
    95
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
paulson@2274
    96
paulson@2274
    97
paulson@2274
    98
(**** Autheticity properties for Woo-Lam ****)
paulson@2274
    99
paulson@2274
   100
paulson@2274
   101
(*** WL4 ***)
paulson@2274
   102
paulson@2274
   103
(*If the encrypted message appears then it originated with Alice*)
paulson@2274
   104
goal thy 
paulson@2283
   105
 "!!evs. [| A ~: lost;  evs : woolam |]                   \
paulson@2283
   106
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
paulson@2283
   107
\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
paulson@2274
   108
by (parts_induct_tac 1);
paulson@2274
   109
by (Fast_tac 1);
paulson@2274
   110
qed_spec_mp "NB_Crypt_imp_Alice_msg";
paulson@2274
   111
paulson@2274
   112
(*Guarantee for Server: if it gets a message containing a certificate from 
paulson@2274
   113
  Alice, then she originated that certificate.  But we DO NOT know that B
paulson@2274
   114
  ever saw it: the Spy may have rerouted the message to the Server.*)
paulson@2274
   115
goal thy 
paulson@2283
   116
 "!!evs. [| A ~: lost;  evs : woolam;               \
paulson@2283
   117
\           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
paulson@2274
   118
\            : set_of_list evs |]                                  \
paulson@2283
   119
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
paulson@2274
   120
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
paulson@2274
   121
                      addSEs [MPair_parts]
paulson@2274
   122
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
paulson@2321
   123
qed "Server_trusts_WL4";
paulson@2274
   124
paulson@2274
   125
paulson@2274
   126
(*** WL5 ***)
paulson@2274
   127
paulson@2274
   128
(*Server sent WL5 only if it received the right sort of message*)
paulson@2274
   129
goal thy 
paulson@2283
   130
 "!!evs. evs : woolam ==>                                              \
paulson@2283
   131
\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
paulson@2283
   132
\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
paulson@2274
   133
\               : set_of_list evs)";
paulson@2274
   134
by (parts_induct_tac 1);
paulson@2274
   135
by (ALLGOALS Fast_tac);
paulson@2274
   136
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
paulson@2274
   137
paulson@2274
   138
paulson@2274
   139
(*If the encrypted message appears then it originated with the Server!*)
paulson@2274
   140
goal thy 
paulson@2283
   141
 "!!evs. [| B ~: lost;  evs : woolam |]                   \
paulson@2283
   142
\    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
paulson@2283
   143
\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
paulson@2274
   144
by (parts_induct_tac 1);
paulson@2274
   145
qed_spec_mp "NB_Crypt_imp_Server_msg";
paulson@2274
   146
paulson@2274
   147
(*Partial guarantee for B: if it gets a message of correct form then the Server
paulson@2274
   148
  sent the same message.*)
paulson@2274
   149
goal thy 
paulson@2283
   150
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
paulson@2283
   151
\           B ~: lost;  evs : woolam |]                                  \
paulson@2283
   152
\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
paulson@2274
   153
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
paulson@2274
   154
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
paulson@2274
   155
qed "B_got_WL5";
paulson@2274
   156
paulson@2274
   157
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
paulson@2274
   158
  the nonce using her key.  This event can be no older than the nonce itself.
paulson@2274
   159
  But A may have sent the nonce to some other agent and it could have reached
paulson@2274
   160
  the Server via the Spy.*)
paulson@2274
   161
goal thy 
paulson@2283
   162
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
paulson@2283
   163
\           A ~: lost;  B ~: lost;  evs : woolam  |] \
paulson@2283
   164
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
paulson@2321
   165
by (fast_tac (!claset addIs  [Server_trusts_WL4]
paulson@2274
   166
                      addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
paulson@2321
   167
qed "B_trusts_WL5";
paulson@2274
   168
paulson@2274
   169
paulson@2274
   170
(*B only issues challenges in response to WL1.  Useful??*)
paulson@2274
   171
goal thy 
paulson@2283
   172
 "!!evs. [| B ~= Spy;  evs : woolam |]                   \
paulson@2274
   173
\    ==> Says B A (Nonce NB) : set_of_list evs        \
paulson@2274
   174
\        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
paulson@2274
   175
by (parts_induct_tac 1);
paulson@2274
   176
by (ALLGOALS Fast_tac);
paulson@2274
   177
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
paulson@2274
   178
paulson@2274
   179
paulson@2274
   180
(**CANNOT be proved because A doesn't know where challenges come from...
paulson@2274
   181
goal thy 
paulson@2283
   182
 "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
paulson@2283
   183
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
paulson@2274
   184
\        Says B A (Nonce NB) : set_of_list evs        \
paulson@2283
   185
\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
paulson@2274
   186
by (parts_induct_tac 1);
paulson@2274
   187
by (Step_tac 1);
paulson@2516
   188
by (best_tac (!claset addSEs partsEs) 1);
paulson@2274
   189
**)