src/HOL/Auth/WooLam.ML
author paulson
Fri, 29 Nov 1996 17:58:18 +0100
changeset 2283 68829cf138fc
parent 2274 1b1b46adc9b3
child 2321 083912bc5775
permissions -rw-r--r--
Swapping arguments of Crypt; removing argument lost
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/WooLam
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     2
    ID:         $Id$
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     5
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     6
Inductive relation "woolam" for the Woo-Lam protocol.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     7
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     8
Simplified version from page 11 of
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     9
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    10
  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    11
*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    12
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    13
open WooLam;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    14
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    15
proof_timing:=true;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    16
HOL_quantifiers := false;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    17
Pretty.setdepth 20;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    18
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    19
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    20
(*Weak liveness: there are traces that reach the end*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    21
goal thy 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    22
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    23
\        ==> EX NB. EX evs: woolam.               \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    24
\               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    25
\                 : set_of_list evs";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    26
by (REPEAT (resolve_tac [exI,bexI] 1));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    27
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    28
	  woolam.WL4 RS woolam.WL5) 2);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    29
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    30
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    31
by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    32
result();
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    33
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    34
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    35
(**** Inductive proofs about woolam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    36
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    37
(*Nobody sends themselves messages*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    38
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    39
by (etac woolam.induct 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    40
by (Auto_tac());
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    41
qed_spec_mp "not_Says_to_self";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    42
Addsimps [not_Says_to_self];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    43
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    44
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    45
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    46
(** For reasoning about the encrypted portion of messages **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    47
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    48
goal thy "!!evs. Says A' B X : set_of_list evs \
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    49
\                ==> X : analz (sees lost Spy evs)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    50
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    51
qed "WL4_analz_sees_Spy";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    52
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    53
bind_thm ("WL4_parts_sees_Spy",
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    54
          WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    55
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    56
val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    57
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    58
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    59
fun parts_induct_tac i = SELECT_GOAL
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    60
    (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    61
             (*Fake message*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    62
             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    63
                                           impOfSubs Fake_parts_insert]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    64
                                    addss (!simpset)) 2)) THEN
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    65
     (*Base case*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    66
     fast_tac (!claset addss (!simpset)) 1 THEN
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    67
     ALLGOALS Asm_simp_tac) i;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    68
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    69
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    70
    sends messages containing X! **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    71
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    72
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    73
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    74
 "!!evs. evs : woolam \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    75
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    76
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    77
by (Auto_tac());
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    78
qed "Spy_see_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    79
Addsimps [Spy_see_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    80
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    81
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    82
 "!!evs. evs : woolam \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    83
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    84
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    85
qed "Spy_analz_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    86
Addsimps [Spy_analz_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    87
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    88
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    89
\                  evs : woolam |] ==> A:lost";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    90
by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    91
qed "Spy_see_shrK_D";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    92
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    93
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    94
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    95
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    96
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    97
(*** Future nonces can't be seen or used! ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    98
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    99
goal thy "!!evs. evs : woolam ==> \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   100
\                length evs <= length evt --> \
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   101
\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   102
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   103
by (REPEAT_FIRST (fast_tac (!claset 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   104
                              addSEs partsEs
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   105
                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   106
                              addEs [leD RS notE]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   107
			      addDs  [impOfSubs analz_subset_parts,
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   108
                                      impOfSubs parts_insert_subset_Un,
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   109
                                      Suc_leD]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   110
                              addss (!simpset))));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   111
qed_spec_mp "new_nonces_not_seen";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   112
Addsimps [new_nonces_not_seen];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   113
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   114
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   115
(**** Autheticity properties for Woo-Lam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   116
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   117
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   118
(*** WL4 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   119
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   120
(*If the encrypted message appears then it originated with Alice*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   121
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   122
 "!!evs. [| A ~: lost;  evs : woolam |]                   \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   123
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   124
\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   125
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   126
by (Fast_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   127
qed_spec_mp "NB_Crypt_imp_Alice_msg";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   128
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   129
(*Guarantee for Server: if it gets a message containing a certificate from 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   130
  Alice, then she originated that certificate.  But we DO NOT know that B
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   131
  ever saw it: the Spy may have rerouted the message to the Server.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   132
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   133
 "!!evs. [| A ~: lost;  evs : woolam;               \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   134
\           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   135
\            : set_of_list evs |]                                  \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   136
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   137
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   138
                      addSEs [MPair_parts]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   139
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   140
qed "Server_trust_WL4";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   141
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   142
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   143
(*** WL5 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   144
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   145
(*Server sent WL5 only if it received the right sort of message*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   146
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   147
 "!!evs. evs : woolam ==>                                              \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   148
\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   149
\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   150
\               : set_of_list evs)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   151
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   152
by (ALLGOALS Fast_tac);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   153
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   154
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   155
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   156
(*If the encrypted message appears then it originated with the Server!*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   157
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   158
 "!!evs. [| B ~: lost;  evs : woolam |]                   \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   159
\    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   160
\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   161
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   162
qed_spec_mp "NB_Crypt_imp_Server_msg";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   163
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   164
(*Partial guarantee for B: if it gets a message of correct form then the Server
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   165
  sent the same message.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   166
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   167
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   168
\           B ~: lost;  evs : woolam |]                                  \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   169
\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   170
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   171
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   172
qed "B_got_WL5";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   173
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   174
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   175
  the nonce using her key.  This event can be no older than the nonce itself.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   176
  But A may have sent the nonce to some other agent and it could have reached
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   177
  the Server via the Spy.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   178
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   179
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   180
\           A ~: lost;  B ~: lost;  evs : woolam  |] \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   181
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   182
by (fast_tac (!claset addIs  [Server_trust_WL4]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   183
                      addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   184
qed "B_trust_WL5";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   185
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   186
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   187
(*B only issues challenges in response to WL1.  Useful??*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   188
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   189
 "!!evs. [| B ~= Spy;  evs : woolam |]                   \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   190
\    ==> Says B A (Nonce NB) : set_of_list evs        \
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   191
\        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   192
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   193
by (ALLGOALS Fast_tac);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   194
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   195
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   196
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   197
(**CANNOT be proved because A doesn't know where challenges come from...
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   198
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   199
 "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   200
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   201
\        Says B A (Nonce NB) : set_of_list evs        \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   202
\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   203
by (parts_induct_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   204
by (Step_tac 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   205
by (best_tac (!claset addSEs partsEs
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   206
                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   207
**)