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