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