src/HOL/Auth/WooLam.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 11150 67387142225e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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@4470
    13
AddEs spies_partsEs;
paulson@4470
    14
AddDs [impOfSubs analz_subset_parts];
paulson@4470
    15
AddDs [impOfSubs Fake_parts_insert];
paulson@4470
    16
paulson@2274
    17
paulson@2321
    18
(*A "possibility property": there are traces that reach the end*)
paulson@5434
    19
Goal "EX NB. EX evs: woolam.  \
paulson@5114
    20
\           Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
paulson@2274
    21
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2274
    22
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
paulson@2516
    23
          woolam.WL4 RS woolam.WL5) 2);
paulson@3471
    24
by possibility_tac;
paulson@2274
    25
result();
paulson@2274
    26
paulson@2274
    27
paulson@2274
    28
(**** Inductive proofs about woolam ****)
paulson@2274
    29
paulson@2274
    30
(** For reasoning about the encrypted portion of messages **)
paulson@2274
    31
paulson@5114
    32
Goal "Says A' B X : set evs ==> X : analz (spies evs)";
paulson@3683
    33
by (etac (Says_imp_spies RS analz.Inj) 1);
paulson@3683
    34
qed "WL4_analz_spies";
paulson@2274
    35
paulson@3683
    36
bind_thm ("WL4_parts_spies",
paulson@3683
    37
          WL4_analz_spies RS (impOfSubs analz_subset_parts));
paulson@2274
    38
paulson@3683
    39
(*For proving the easier theorems about X ~: parts (spies evs) *)
paulson@3519
    40
fun parts_induct_tac i = 
paulson@3519
    41
    etac woolam.induct i  THEN 
wenzelm@7499
    42
    ftac WL4_parts_spies (i+5)  THEN
paulson@3471
    43
    prove_simple_subgoals_tac 1;
paulson@2274
    44
paulson@2274
    45
paulson@3683
    46
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2274
    47
    sends messages containing X! **)
paulson@2274
    48
paulson@3683
    49
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@5114
    50
Goal "evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
paulson@3519
    51
by (parts_induct_tac 1);
paulson@4470
    52
by (Blast_tac 1);
paulson@2274
    53
qed "Spy_see_shrK";
paulson@2274
    54
Addsimps [Spy_see_shrK];
paulson@2274
    55
paulson@5114
    56
Goal "evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
paulson@4477
    57
by Auto_tac;
paulson@2274
    58
qed "Spy_analz_shrK";
paulson@2274
    59
Addsimps [Spy_analz_shrK];
paulson@2274
    60
paulson@4470
    61
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
paulson@4470
    62
	Spy_analz_shrK RSN (2, rev_iffD1)];
paulson@2274
    63
paulson@2274
    64
paulson@2274
    65
(**** Autheticity properties for Woo-Lam ****)
paulson@2274
    66
paulson@2274
    67
paulson@2274
    68
(*** WL4 ***)
paulson@2274
    69
paulson@2274
    70
(*If the encrypted message appears then it originated with Alice*)
paulson@5114
    71
Goal "[| Crypt (shrK A) (Nonce NB) : parts (spies evs);  \
paulson@5114
    72
\        A ~: bad;  evs : woolam |]                      \
paulson@5114
    73
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
paulson@4470
    74
by (etac rev_mp 1);
paulson@3519
    75
by (parts_induct_tac 1);
paulson@4470
    76
by (ALLGOALS Blast_tac);
paulson@4470
    77
qed "NB_Crypt_imp_Alice_msg";
paulson@2274
    78
paulson@2274
    79
(*Guarantee for Server: if it gets a message containing a certificate from 
paulson@2274
    80
  Alice, then she originated that certificate.  But we DO NOT know that B
paulson@2274
    81
  ever saw it: the Spy may have rerouted the message to the Server.*)
paulson@5114
    82
Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
paulson@5114
    83
\          : set evs;                                                   \
paulson@5114
    84
\        A ~: bad;  evs : woolam |]                                     \
paulson@5114
    85
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
paulson@4470
    86
by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1);
paulson@2321
    87
qed "Server_trusts_WL4";
paulson@2274
    88
paulson@4470
    89
AddDs [Server_trusts_WL4];
paulson@4470
    90
paulson@2274
    91
paulson@2274
    92
(*** WL5 ***)
paulson@2274
    93
paulson@2274
    94
(*Server sent WL5 only if it received the right sort of message*)
paulson@5114
    95
Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs;      \
paulson@5114
    96
\        evs : woolam |]                                                \
paulson@5114
    97
\     ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
paulson@5114
    98
\            : set evs";
paulson@4470
    99
by (etac rev_mp 1);
paulson@3519
   100
by (parts_induct_tac 1);
paulson@3121
   101
by (ALLGOALS Blast_tac);
paulson@4470
   102
qed "Server_sent_WL5";
paulson@2274
   103
paulson@4470
   104
AddDs [Server_sent_WL5];
paulson@2274
   105
paulson@2274
   106
(*If the encrypted message appears then it originated with the Server!*)
paulson@5114
   107
Goal "[| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs);  \
paulson@5114
   108
\        B ~: bad;  evs : woolam |]                           \
paulson@5114
   109
\     ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
paulson@4470
   110
by (etac rev_mp 1);
paulson@3519
   111
by (parts_induct_tac 1);
paulson@4470
   112
by (Blast_tac 1);
paulson@2274
   113
qed_spec_mp "NB_Crypt_imp_Server_msg";
paulson@2274
   114
paulson@2274
   115
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
paulson@2274
   116
  the nonce using her key.  This event can be no older than the nonce itself.
paulson@2274
   117
  But A may have sent the nonce to some other agent and it could have reached
paulson@2274
   118
  the Server via the Spy.*)
paulson@5114
   119
Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
paulson@5114
   120
\        A ~: bad;  B ~: bad;  evs : woolam  |]                  \
paulson@5114
   121
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
paulson@4470
   122
by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1);
paulson@2321
   123
qed "B_trusts_WL5";
paulson@2274
   124
paulson@2274
   125
paulson@4470
   126
(*B only issues challenges in response to WL1.  Not used.*)
paulson@5114
   127
Goal "[| Says B A (Nonce NB) : set evs;  B ~= Spy;  evs : woolam |]  \
paulson@5114
   128
\     ==> EX A'. Says A' B (Agent A) : set evs";
paulson@4470
   129
by (etac rev_mp 1);
paulson@3519
   130
by (parts_induct_tac 1);
paulson@3121
   131
by (ALLGOALS Blast_tac);
paulson@4470
   132
qed "B_said_WL2";
paulson@2274
   133
paulson@2274
   134
paulson@2274
   135
(**CANNOT be proved because A doesn't know where challenges come from...
paulson@5114
   136
Goal "[| A ~: bad;  B ~= Spy;  evs : woolam |]           \
paulson@5114
   137
\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) &  \
paulson@5114
   138
\     Says B A (Nonce NB) : set evs                       \
paulson@5114
   139
\     --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
paulson@3519
   140
by (parts_induct_tac 1);
paulson@4470
   141
by (Blast_tac 1);
paulson@3730
   142
by Safe_tac;
paulson@2274
   143
**)