src/HOL/Auth/NS_Shared.ML
author paulson
Thu, 08 Jan 1998 18:10:34 +0100
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4831 dae4d63a1318
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/NS_Shared
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     8
From page 247 of
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
  Proc. Royal Soc. 426 (1989)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
open NS_Shared;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    14
4449
wenzelm
parents: 4422
diff changeset
    15
set proof_timing;
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
diff changeset
    16
HOL_quantifiers := false;
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
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
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
diff changeset
    22
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
    23
(*A "possibility property": there are traces that reach the end*)
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
diff changeset
    24
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    25
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
    26
\        ==> EX N K. EX evs: ns_shared.               \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    27
\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
diff changeset
    28
by (REPEAT (resolve_tac [exI,bexI] 1));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    29
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    30
          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    31
by possibility_tac;
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    32
result();
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    33
3675
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    34
goal thy 
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    35
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    36
\        ==> EX evs: ns_shared.          \
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    37
\               Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    38
by (REPEAT (resolve_tac [exI,bexI] 1));
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    39
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    40
          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
70dd312b70b2 Deleted the redundant simprule not_parts_not_analz
paulson
parents: 3651
diff changeset
    41
by possibility_tac;
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    42
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    43
(**** Inductive proofs about ns_shared ****)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    44
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    45
(*Nobody sends themselves messages*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    46
goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    47
by (etac ns_shared.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4470
diff changeset
    48
by Auto_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    49
qed_spec_mp "not_Says_to_self";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    50
Addsimps [not_Says_to_self];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    51
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    53
(*For reasoning about the encrypted portion of message NS3*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    54
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    55
\                ==> X : parts (spies evs)";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    56
by (Blast_tac 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    57
qed "NS3_msg_in_parts_spies";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    58
                              
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    59
goal thy
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    60
    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    61
\           ==> K : parts (spies evs)";
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    62
by (Blast_tac 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    63
qed "Oops_parts_spies";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    64
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    65
(*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: 3516
diff changeset
    66
fun parts_induct_tac i = 
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
    67
  EVERY [etac ns_shared.induct i,
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
    68
	 REPEAT (FIRSTGOAL analz_mono_contra_tac),
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
    69
	 forward_tac [Oops_parts_spies] (i+7),
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
    70
	 forward_tac [NS3_msg_in_parts_spies] (i+4),
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
    71
	 prove_simple_subgoals_tac i];
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    72
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    73
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    74
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    75
    sends messages containing X! **)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    76
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    77
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    78
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    79
 "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    80
by (parts_induct_tac 1);
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
    81
by (ALLGOALS Blast_tac);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    82
qed "Spy_see_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    83
Addsimps [Spy_see_shrK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    84
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    85
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    86
 "!!evs. evs : ns_shared ==> (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
    87
by Auto_tac;
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    88
qed "Spy_analz_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    89
Addsimps [Spy_analz_shrK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    90
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    91
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
    92
	Spy_analz_shrK RSN (2, rev_iffD1)];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    93
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    94
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    95
(*Nobody can have used non-existent keys!*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    96
goal thy "!!evs. evs : ns_shared ==>      \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
    97
\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    98
by (parts_induct_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    99
(*Fake*)
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
   100
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   101
(*NS2, NS4, NS5*)
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   102
by (ALLGOALS (Blast_tac));
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2131
diff changeset
   103
qed_spec_mp "new_keys_not_used";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   104
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   105
bind_thm ("new_keys_not_analzd",
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   106
          [analz_subset_parts RS keysFor_mono,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   107
           new_keys_not_used] MRS contra_subsetD);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   108
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   109
Addsimps [new_keys_not_used, new_keys_not_analzd];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   110
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   111
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   112
(** Lemmas concerning the form of items passed in messages **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   113
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   114
(*Describes the form of K, X and K' when the Server sends this message.*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   115
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   116
 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   117
\           evs : ns_shared |]                           \
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   118
\        ==> K ~: range shrK &                           \
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   119
\            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   120
\            K' = shrK A";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   121
by (etac rev_mp 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   122
by (etac ns_shared.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4470
diff changeset
   123
by Auto_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   124
qed "Says_Server_message_form";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   125
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   126
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   127
(*If the encrypted message appears then it originated with the Server*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   128
goal thy
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   129
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   130
\           A ~: bad;  evs : ns_shared |]                                 \
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   131
\         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
3651
5f6ab7fbd53b Simplified the statement of A_trusts_NS2
paulson
parents: 3519
diff changeset
   132
\               : set evs";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   133
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   134
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   135
by (Blast_tac 1);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   136
qed "A_trusts_NS2";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   137
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   138
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   139
goal thy
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   140
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   141
\           A ~: bad;  evs : ns_shared |]                                 \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   142
\         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   143
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   144
qed "cert_A_form";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   145
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   146
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   147
(*EITHER describes the form of X when the following message is sent, 
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   148
  OR     reduces it to the Fake case.
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   149
  Use Says_Server_message_form if applicable.*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   150
goal thy 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   151
 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
3651
5f6ab7fbd53b Simplified the statement of A_trusts_NS2
paulson
parents: 3519
diff changeset
   152
\              : set evs;                                                  \
5f6ab7fbd53b Simplified the statement of A_trusts_NS2
paulson
parents: 3519
diff changeset
   153
\           evs : ns_shared |]                                             \
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   154
\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   155
\            | X : analz (spies evs)";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   156
by (case_tac "A : bad" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   157
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   158
                       addss (simpset())) 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   159
by (blast_tac (claset() addSDs [cert_A_form]) 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   160
qed "Says_S_message_form";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   161
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   162
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   163
(*For proofs involving analz.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   164
val analz_spies_tac = 
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   165
    forward_tac [Says_Server_message_form] 8 THEN
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   166
    forward_tac [Says_S_message_form] 5 THEN 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   167
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   168
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   169
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   170
(****
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   171
 The following is to prove theorems of the form
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   172
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   173
  Key K : analz (insert (Key KAB) (spies evs)) ==>
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   174
  Key K : analz (spies evs)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   175
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   176
 A more general formula must be proved inductively.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   177
****)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   178
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   179
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   180
(*NOT useful in this form, but it says that session keys are not used
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   181
  to encrypt messages containing other keys, in the actual protocol.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   182
  We require that agents should behave like this subsequently also.*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   183
goal thy 
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   184
 "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   185
\           (Crypt KAB X) : parts (spies evs) &         \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   186
\           Key K : parts {X} --> Key K : parts (spies evs)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   187
by (parts_induct_tac 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   188
(*Fake*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   189
by (blast_tac (claset() addSEs partsEs
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   190
                        addDs [impOfSubs parts_insert_subset_Un]) 1);
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   191
(*Base, NS4 and NS5*)
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4470
diff changeset
   192
by Auto_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   193
result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   194
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   195
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   196
(** Session keys are not used to encrypt other session keys **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   197
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   198
(*The equality makes the induction hypothesis easier to apply*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   199
goal thy  
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   200
 "!!evs. evs : ns_shared ==>                             \
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   201
\  ALL K KK. KK <= Compl (range shrK) -->                \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   202
\            (Key K : analz (Key``KK Un (spies evs))) =  \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   203
\            (K : KK | Key K : analz (spies evs))";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   204
by (etac ns_shared.induct 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   205
by analz_spies_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   206
by (REPEAT_FIRST (resolve_tac [allI, impI]));
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   207
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   208
(*Takes 9 secs*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   209
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   210
(*Fake*) 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4331
diff changeset
   211
by (spy_analz_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   212
qed_spec_mp "analz_image_freshK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   213
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   214
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   215
goal thy
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   216
 "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   217
\        Key K : analz (insert (Key KAB) (spies evs)) = \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   218
\        (K = KAB | Key K : analz (spies evs))";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   219
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   220
qed "analz_insert_freshK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   221
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   222
2558
6e8d130463e3 Corrected faulty comment
paulson
parents: 2529
diff changeset
   223
(** The session key K uniquely identifies the message **)
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   224
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   225
goal thy 
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   226
 "!!evs. evs : ns_shared ==>                                               \
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   227
\      EX A' NA' B' X'. ALL A NA B X.                                      \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   228
\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   229
\       -->         A=A' & NA=NA' & B=B' & X=X'";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   230
by (etac ns_shared.induct 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   231
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   232
by Safe_tac;
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   233
(*NS3*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   234
by (ex_strip_tac 2);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   235
by (Blast_tac 2);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   236
(*NS2: it can't be a new key*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   237
by (expand_case_tac "K = ?y" 1);
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   238
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   239
by (Blast_tac 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   240
val lemma = result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   241
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   242
(*In messages of this form, the session key uniquely identifies the rest*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   243
goal thy 
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   244
 "!!evs. [| Says Server A                                               \
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   245
\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   246
\           Says Server A'                                              \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   247
\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   248
\           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2374
diff changeset
   249
by (prove_unique_tac lemma 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   250
qed "unique_session_keys";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   251
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   252
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   253
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   254
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   255
goal thy 
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   256
 "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   257
\        ==> Says Server A                                             \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   258
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   259
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   260
\             : set evs -->                                            \
4537
4e835bd9fada Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents: 4509
diff changeset
   261
\        (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) -->          \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   262
\        Key K ~: analz (spies evs)";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   263
by (etac ns_shared.induct 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   264
by analz_spies_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   265
by (ALLGOALS 
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   266
    (asm_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   267
     (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   268
			  pushes @ expand_ifs))));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   269
(*Oops*)
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
   270
by (blast_tac (claset() addSDs [unique_session_keys]) 5);
3679
8df171ccdbd8 Fixed comments
paulson
parents: 3675
diff changeset
   271
(*NS3, replay sub-case*) 
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   272
by (Blast_tac 4);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   273
(*NS2*)
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   274
by (Blast_tac 2);
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   275
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   276
by (spy_analz_tac 1);
3679
8df171ccdbd8 Fixed comments
paulson
parents: 3675
diff changeset
   277
(*NS3, Server sub-case*) (**LEVEL 6 **)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   278
by (clarify_tac (claset() delrules [impCE]) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   279
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
2170
c5e460f1ebb4 Ran expandshort
paulson
parents: 2165
diff changeset
   280
by (assume_tac 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   281
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   282
			       Crypt_Spy_analz_bad]) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   283
by (blast_tac (claset() addDs [unique_session_keys]) 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   284
val lemma = result() RS mp RS mp RSN(2,rev_notE);
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   285
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   286
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   287
(*Final version: Server's message in the most abstract form*)
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   288
goal thy 
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   289
 "!!evs. [| Says Server A                                        \
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   290
\              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
4537
4e835bd9fada Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents: 4509
diff changeset
   291
\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   292
\           A ~: bad;  B ~: bad;  evs : ns_shared                \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3679
diff changeset
   293
\        |] ==> Key K ~: analz (spies evs)";
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   294
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   295
by (blast_tac (claset() addSDs [lemma]) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   296
qed "Spy_not_see_encrypted_key";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   297
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   298
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   299
(**** Guarantees available at various stages of protocol ***)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   300
3651
5f6ab7fbd53b Simplified the statement of A_trusts_NS2
paulson
parents: 3519
diff changeset
   301
A_trusts_NS2 RS Spy_not_see_encrypted_key;
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   302
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   303
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   304
(*If the encrypted message appears then it originated with the Server*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   305
goal thy
4237
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   306
 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
fb01353e363b The dtac was discarding information, though apparently no proofs were hurt
paulson
parents: 4091
diff changeset
   307
\           B ~: bad;  evs : ns_shared |]                              \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   308
\         ==> EX NA. Says Server A                                     \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   309
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   310
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   311
\             : set evs";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   312
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   313
by (parts_induct_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   314
by (ALLGOALS Blast_tac);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   315
qed "B_trusts_NS3";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   316
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   317
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   318
goal thy
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   319
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   320
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   321
\              : set evs;                                             \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   322
\           Key K ~: analz (spies evs);                               \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   323
\           evs : ns_shared |]                  \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   324
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   325
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   326
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   327
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   328
by (parts_induct_tac 1);
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   329
(*NS3*)
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   330
by (Blast_tac 3);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   331
by (Blast_tac 1);
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   332
(*NS2: contradiction from the assumptions  
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   333
  Key K ~: used evs2  and Crypt K (Nonce NB) : parts (spies evs2) *)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   334
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   335
			addSDs [Crypt_imp_keysFor]) 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   336
(**LEVEL 7**)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   337
(*NS4*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   338
by (Clarify_tac 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   339
by (not_bad_tac "Ba" 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   340
by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   341
qed "A_trusts_NS4_lemma";
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   342
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   343
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   344
(*This version no longer assumes that K is secure*)
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   345
goal thy
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   346
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   347
\           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
4537
4e835bd9fada Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents: 4509
diff changeset
   348
\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   349
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   350
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   351
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
4267
cdc193e38925 tidying
paulson
parents: 4237
diff changeset
   352
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   353
qed "A_trusts_NS4";
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   354
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   355
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   356
(*If the session key has been used in NS4 then somebody has forwarded
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   357
  component X in some instance of NS4.  Perhaps an interesting property, 
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   358
  but not needed (after all) for the proofs below.*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   359
goal thy
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   360
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);     \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   361
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   362
\             : set evs;                                              \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   363
\           Key K ~: analz (spies evs);                               \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   364
\           evs : ns_shared |]                              \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   365
\        ==> EX A'. Says A' B X : set evs";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   366
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   367
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   368
by (etac rev_mp 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   369
by (parts_induct_tac 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   370
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   371
by (ALLGOALS Clarify_tac);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   372
by (Blast_tac 1);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   373
(**LEVEL 7**)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   374
(*NS2*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   375
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   376
			addSDs [Crypt_imp_keysFor]) 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   377
(*NS4*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   378
by (not_bad_tac "Ba" 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   379
by (Asm_full_simp_tac 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   380
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   381
by (ALLGOALS Clarify_tac);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   382
by (blast_tac (claset() addDs [unique_session_keys]) 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   383
qed "NS4_implies_NS3";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   384
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   385
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   386
goal thy
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   387
 "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   388
\        ==> Key K ~: analz (spies evs) -->                            \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   389
\            Says Server A                                     \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   390
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   391
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   392
\             : set evs -->         \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   393
\            Says B A (Crypt K (Nonce NB))  : set evs -->  \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   394
\            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   395
\            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   396
by (parts_induct_tac 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   397
(*NS4*)
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   398
by (Blast_tac 4);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   399
(*NS3*)
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   400
by (blast_tac (claset() addSDs [cert_A_form]) 3);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   401
(*NS2*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   402
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   403
			addSDs [Crypt_imp_keysFor]) 2);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   404
by (Blast_tac 1);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   405
(**LEVEL 5**)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   406
(*NS5*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   407
by (Clarify_tac 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   408
by (not_bad_tac "Aa" 1);
4470
af3239def3d4 Tidied using more default rules
paulson
parents: 4449
diff changeset
   409
by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   410
val lemma = result();
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   411
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   412
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   413
(*Very strong Oops condition reveals protocol's weakness*)
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   414
goal thy
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   415
 "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   416
\           Says B A (Crypt K (Nonce NB))  : set evs;                \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   417
\           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
4537
4e835bd9fada Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents: 4509
diff changeset
   418
\           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
4331
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   419
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   420
\        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   421
by (dtac B_trusts_NS3 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   422
by (ALLGOALS Clarify_tac);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   423
by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma]
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   424
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
34bb65b037dd New guarantee B_trusts_NS5, and tidying
paulson
parents: 4267
diff changeset
   425
qed "B_trusts_NS5";