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