src/HOL/Auth/WooLam.ML
author paulson
Thu, 02 Jul 1998 17:48:11 +0200
changeset 5114 c729d4c299c1
parent 5076 fbc9d95b62ba
child 5223 4cb05273f764
permissions -rw-r--r--
Deleted leading parameters thanks to new Goal command
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
4449
wenzelm
parents: 4091
diff changeset
    15
set proof_timing;
2274
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
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    18
AddEs spies_partsEs;
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    19
AddDs [impOfSubs analz_subset_parts];
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    20
AddDs [impOfSubs Fake_parts_insert];
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    21
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    22
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
    23
(*A "possibility property": there are traces that reach the end*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    24
Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    25
\     ==> EX NB. EX evs: woolam.               \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    26
\           Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    27
by (REPEAT (resolve_tac [exI,bexI] 1));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    28
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    29
          woolam.WL4 RS woolam.WL5) 2);
3471
cd37ec057028 Now the possibility proof calls the appropriate tactic
paulson
parents: 3466
diff changeset
    30
by possibility_tac;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    31
result();
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    32
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    33
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    34
(**** Inductive proofs about woolam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    35
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    36
(*Nobody sends themselves messages*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    37
Goal "evs : woolam ==> ALL A X. Says A A X ~: set evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    38
by (etac woolam.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4470
diff changeset
    39
by Auto_tac;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    40
qed_spec_mp "not_Says_to_self";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    41
Addsimps [not_Says_to_self];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    42
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    43
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    44
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    45
(** For reasoning about the encrypted portion of messages **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    46
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    47
Goal "Says A' B X : set evs ==> X : analz (spies evs)";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    48
by (etac (Says_imp_spies RS analz.Inj) 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    49
qed "WL4_analz_spies";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    50
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    51
bind_thm ("WL4_parts_spies",
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    52
          WL4_analz_spies RS (impOfSubs analz_subset_parts));
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    53
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    54
(*For proving the easier theorems about X ~: parts (spies evs) *)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
    55
fun parts_induct_tac i = 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
    56
    etac woolam.induct i  THEN 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    57
    forward_tac [WL4_parts_spies] (i+5)  THEN
3471
cd37ec057028 Now the possibility proof calls the appropriate tactic
paulson
parents: 3466
diff changeset
    58
    prove_simple_subgoals_tac 1;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    59
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    60
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    61
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    62
    sends messages containing X! **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    63
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    64
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    65
Goal "evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
    66
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    67
by (Blast_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    68
qed "Spy_see_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    69
Addsimps [Spy_see_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    70
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    71
Goal "evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4470
diff changeset
    72
by Auto_tac;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    73
qed "Spy_analz_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    74
Addsimps [Spy_analz_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    75
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    76
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    77
	Spy_analz_shrK RSN (2, rev_iffD1)];
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    78
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    79
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    80
(**** Autheticity properties for Woo-Lam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    81
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    82
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    83
(*** WL4 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    84
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    85
(*If the encrypted message appears then it originated with Alice*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    86
Goal "[| Crypt (shrK A) (Nonce NB) : parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    87
\        A ~: bad;  evs : woolam |]                      \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    88
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    89
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
    90
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    91
by (ALLGOALS Blast_tac);
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    92
qed "NB_Crypt_imp_Alice_msg";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    93
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    94
(*Guarantee for Server: if it gets a message containing a certificate from 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    95
  Alice, then she originated that certificate.  But we DO NOT know that B
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    96
  ever saw it: the Spy may have rerouted the message to the Server.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    97
Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    98
\          : set evs;                                                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    99
\        A ~: bad;  evs : woolam |]                                     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   100
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   101
by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1);
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
   102
qed "Server_trusts_WL4";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   103
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   104
AddDs [Server_trusts_WL4];
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   105
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   106
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   107
(*** WL5 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   108
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   109
(*Server sent WL5 only if it received the right sort of message*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   110
Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs;      \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   111
\        evs : woolam |]                                                \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   112
\     ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   113
\            : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   114
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
   115
by (parts_induct_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   116
by (ALLGOALS Blast_tac);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   117
qed "Server_sent_WL5";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   118
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   119
AddDs [Server_sent_WL5];
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   120
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   121
(*If the encrypted message appears then it originated with the Server!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   122
Goal "[| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   123
\        B ~: bad;  evs : woolam |]                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   124
\     ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   125
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
   126
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   127
by (Blast_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   128
qed_spec_mp "NB_Crypt_imp_Server_msg";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   129
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   130
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   131
  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
   132
  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
   133
  the Server via the Spy.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   134
Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   135
\        A ~: bad;  B ~: bad;  evs : woolam  |]                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   136
\     ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   137
by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1);
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
   138
qed "B_trusts_WL5";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   139
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   140
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   141
(*B only issues challenges in response to WL1.  Not used.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   142
Goal "[| Says B A (Nonce NB) : set evs;  B ~= Spy;  evs : woolam |]  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   143
\     ==> EX A'. Says A' B (Agent A) : set evs";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   144
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
   145
by (parts_induct_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   146
by (ALLGOALS Blast_tac);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   147
qed "B_said_WL2";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   148
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   149
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   150
(**CANNOT be proved because A doesn't know where challenges come from...
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   151
Goal "[| A ~: bad;  B ~= Spy;  evs : woolam |]           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   152
\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) &  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   153
\     Says B A (Nonce NB) : set evs                       \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   154
\     --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3471
diff changeset
   155
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   156
by (Blast_tac 1);
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   157
by Safe_tac;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   158
**)