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