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