src/HOL/Auth/NS_Shared.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3466 30791e5a69c4
child 3516 470626799511
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    18
(*Replacing the variable by a constant improves search speed by 50%!*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    19
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    20
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1967
diff changeset
    21
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
    22
(*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
    23
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    24
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    25
\        ==> EX N K. EX evs: ns_shared lost.          \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    26
\               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
    27
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
    28
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
    29
          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
    30
by possibility_tac;
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    31
result();
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    32
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    33
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    34
(**** Inductive proofs about ns_shared ****)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    35
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
    36
(*Monotonicity*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    37
goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    38
by (rtac subsetI 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    39
by (etac ns_shared.induct 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    40
by (REPEAT_FIRST
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    41
    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    42
                              :: ns_shared.intrs))));
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    43
qed "ns_shared_mono";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    44
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    45
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    46
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    47
goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    48
by (etac ns_shared.induct 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    49
by (Auto_tac());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    50
qed_spec_mp "not_Says_to_self";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    51
Addsimps [not_Says_to_self];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    53
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    54
(*For reasoning about the encrypted portion of message NS3*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    55
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    56
\                ==> X : parts (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    57
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    58
qed "NS3_msg_in_parts_sees_Spy";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    59
                              
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    60
goal thy
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    61
    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    62
\           ==> K : parts (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    63
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    64
qed "Oops_parts_sees_Spy";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    65
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    66
(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    67
  We instantiate the variable to "lost" since leaving it as a Var would
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    68
  interfere with simplification.*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    69
val parts_induct_tac = 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    70
    etac ns_shared.induct 1  THEN 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    71
    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    72
    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    73
    prove_simple_subgoals_tac 1;
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
    74
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    75
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
    76
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
    77
    sends messages containing X! **)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    78
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    79
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    80
goal thy 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    81
 "!!evs. evs : ns_shared lost \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    82
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    83
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    84
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    85
by (Blast_tac 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    86
qed "Spy_see_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    87
Addsimps [Spy_see_shrK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    88
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    89
goal thy 
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    90
 "!!evs. evs : ns_shared lost \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    91
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    92
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    93
qed "Spy_analz_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    94
Addsimps [Spy_analz_shrK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    95
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    96
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    97
\                  evs : ns_shared lost |] ==> A:lost";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    98
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
    99
qed "Spy_see_shrK_D";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   100
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   101
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
   102
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   103
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   104
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   105
(*Nobody can have used non-existent keys!*)
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2131
diff changeset
   106
goal thy "!!evs. evs : ns_shared lost ==>      \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   107
\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   108
by parts_induct_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   109
(*Fake*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   110
by (best_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   111
      (!claset addIs [impOfSubs analz_subset_parts]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   112
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   113
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   114
               addss (!simpset)) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   115
(*NS2, NS4, NS5*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   116
by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2131
diff changeset
   117
qed_spec_mp "new_keys_not_used";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   118
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   119
bind_thm ("new_keys_not_analzd",
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   120
          [analz_subset_parts RS keysFor_mono,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   121
           new_keys_not_used] MRS contra_subsetD);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   122
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   123
Addsimps [new_keys_not_used, new_keys_not_analzd];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   124
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   125
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   126
(** Lemmas concerning the form of items passed in messages **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   127
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   128
(*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
   129
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   130
 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   131
\             : set evs;                                      \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   132
\           evs : ns_shared lost |]                           \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   133
\        ==> K ~: range shrK &                                \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   134
\            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   135
\            K' = shrK A";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   136
by (etac rev_mp 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   137
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
   138
by (Auto_tac());
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   139
qed "Says_Server_message_form";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   140
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   141
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   142
(*If the encrypted message appears then it originated with the Server*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   143
goal thy
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   144
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   145
\            : parts (sees lost Spy evs);                              \
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   146
\           A ~: lost;  evs : ns_shared lost |]                        \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   147
\         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   148
\             Says Server A                                            \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   149
\              (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
   150
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   151
\             : set evs";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   152
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   153
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   154
by (Fake_parts_insert_tac 1);
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   155
by (Auto_tac());
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   156
qed "A_trusts_NS2";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   157
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   158
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   159
(*EITHER describes the form of X when the following message is sent, 
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   160
  OR     reduces it to the Fake case.
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   161
  Use Says_Server_message_form if applicable.*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   162
goal thy 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   163
 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   164
\            : set evs;          evs : ns_shared lost |]                   \
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   165
\        ==> (K ~: range shrK & 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
   166
\            | X : analz (sees lost Spy evs)";
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   167
by (case_tac "A : lost" 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   168
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   169
                      addss (!simpset)) 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   170
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   171
by (blast_tac (!claset addEs  partsEs
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   172
                      addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   173
qed "Says_S_message_form";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   174
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   175
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   176
(*For proofs involving analz.  We again instantiate the variable to "lost".*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   177
val analz_sees_tac = 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   178
    forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   179
    forw_inst_tac [("lost","lost")] 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
   180
    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
   181
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   182
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
 The following is to prove theorems of the form
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   185
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   186
  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2374
diff changeset
   187
  Key K : analz (sees lost Spy evs)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   188
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   189
 A more general formula must be proved inductively.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   190
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   191
****)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   192
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   193
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   194
(*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
   195
  to encrypt messages containing other keys, in the actual protocol.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   196
  We require that agents should behave like this subsequently also.*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   197
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   198
 "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   199
\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   200
\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   201
by parts_induct_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   202
(*Deals with Faked messages*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   203
by (blast_tac (!claset addSEs partsEs
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   204
                       addDs [impOfSubs parts_insert_subset_Un]) 1);
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   205
(*Base, NS4 and NS5*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   206
by (Auto_tac());
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   207
result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   208
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   209
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   210
(** Session keys are not used to encrypt other session keys **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   211
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   212
(*The equality makes the induction hypothesis easier to apply*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   213
goal thy  
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   214
 "!!evs. evs : ns_shared lost ==>                                \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   215
\  ALL K KK. KK <= Compl (range shrK) -->                        \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   216
\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   217
\            (K : KK | Key K : analz (sees lost Spy evs))";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   218
by (etac ns_shared.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   219
by analz_sees_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   220
by (REPEAT_FIRST (resolve_tac [allI, impI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   221
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   222
(*Takes 24 secs*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   223
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
   224
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   225
by (spy_analz_tac 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   226
(*Base*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   227
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   228
qed_spec_mp "analz_image_freshK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   229
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   230
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   231
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   232
 "!!evs. [| evs : ns_shared lost;  KAB ~: range shrK |] ==>     \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   233
\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   234
\        (K = KAB | Key K : analz (sees lost Spy evs))";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   235
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
   236
qed "analz_insert_freshK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   237
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   238
2558
6e8d130463e3 Corrected faulty comment
paulson
parents: 2529
diff changeset
   239
(** The session key K uniquely identifies the message **)
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   240
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   241
goal thy 
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2374
diff changeset
   242
 "!!evs. evs : ns_shared lost ==>                                        \
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2374
diff changeset
   243
\      EX A' NA' B' X'. ALL A NA B X.                                    \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   244
\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   245
\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   246
by (etac ns_shared.induct 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   247
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   248
by (Step_tac 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   249
(*NS3*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   250
by (ex_strip_tac 2);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   251
by (Blast_tac 2);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   252
(*NS2: it can't be a new key*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   253
by (expand_case_tac "K = ?y" 1);
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   254
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   255
by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   256
                      addSEs sees_Spy_partsEs) 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   257
val lemma = result();
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
(*In messages of this form, the session key uniquely identifies the rest*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   260
goal thy 
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   261
 "!!evs. [| Says Server A                                    \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   262
\             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   263
\                  : set evs;                                \ 
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
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, X'|}) \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   266
\                  : set evs;                                \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   267
\           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2374
diff changeset
   268
by (prove_unique_tac lemma 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   269
qed "unique_session_keys";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   270
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   271
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   272
(** 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
   273
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   274
goal thy 
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   275
 "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   276
\        ==> Says Server A                                             \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   277
\              (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
   278
\                                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
   279
\             : set evs -->                                            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   280
\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
2050
1b3343fa1278 Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm
paulson
parents: 2045
diff changeset
   281
\        Key K ~: analz (sees lost Spy evs)";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   282
by (etac ns_shared.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   283
by analz_sees_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   284
by (ALLGOALS 
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   285
    (asm_simp_tac 
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   286
     (!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   287
			  analz_insert_freshK] @ pushes)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   288
               setloop split_tac [expand_if])));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   289
(*Oops*)
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   290
by (blast_tac (!claset addDs [unique_session_keys]) 5);
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   291
(*NS4*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   292
by (Blast_tac 4);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   293
(*NS2*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   294
by (blast_tac (!claset addSEs sees_Spy_partsEs
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   295
                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   296
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3441
diff changeset
   297
by (spy_analz_tac 1);
2529
e40ca839758d Simplified Oops case of main theorem
paulson
parents: 2516
diff changeset
   298
(*NS3*) (**LEVEL 6 **)
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   299
by (step_tac (!claset delrules [impCE]) 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   300
by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
2170
c5e460f1ebb4 Ran expandshort
paulson
parents: 2165
diff changeset
   301
by (assume_tac 2);
3441
6d2887123fa0 Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents: 3121
diff changeset
   302
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
6d2887123fa0 Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents: 3121
diff changeset
   303
			      Crypt_Spy_analz_lost]) 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   304
by (blast_tac (!claset addDs [unique_session_keys]) 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   305
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
   306
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   307
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   308
(*Final version: Server's message in the most abstract form*)
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   309
goal thy 
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   310
 "!!evs. [| Says Server A                                               \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   311
\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   312
\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   313
\           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   314
\        |] ==> Key K ~: analz (sees lost Spy evs)";
2015
d4a8fd8a8065 Simplification of proof of unique_session_keys
paulson
parents: 1999
diff changeset
   315
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   316
by (blast_tac (!claset addSDs [lemma]) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   317
qed "Spy_not_see_encrypted_key";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   318
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   319
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   320
goal thy 
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   321
 "!!evs. [| C ~: {A,B,Server};                                          \
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   322
\           Says Server A                                               \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   323
\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   324
\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   325
\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   326
\        ==> Key K ~: analz (sees lost C evs)";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   327
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   328
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   329
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   330
by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2027
diff changeset
   331
qed "Agent_not_see_encrypted_key";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   332
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   333
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   334
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   335
(**** Guarantees available at various stages of protocol ***)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   336
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   337
A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   338
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   339
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   340
(*If the encrypted message appears then it originated with the Server*)
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   341
goal thy
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   342
 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   343
\           B ~: lost;  evs : ns_shared lost |]                        \
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   344
\         ==> EX NA. Says Server A                                     \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   345
\              (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
   346
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   347
\             : set evs";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   348
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   349
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   350
by (Fake_parts_insert_tac 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   351
(*Fake case*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   352
by (ALLGOALS Blast_tac);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   353
qed "B_trusts_NS3";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   354
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   355
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   356
goal thy
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   357
 "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   358
\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   359
\            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   360
\            : set evs -->                                             \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   361
\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   362
\            Says B A (Crypt K (Nonce NB)) : set evs";
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   363
by (etac ns_shared.induct 1);
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   364
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   365
by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   366
by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   367
by (TRYALL (rtac impI));
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   368
by (REPEAT_FIRST
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   369
    (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   370
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   371
(**LEVEL 7**)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   372
by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   373
                       addDs [impOfSubs analz_subset_parts]) 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   374
by (Blast_tac 2);
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   375
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   376
(*Subgoal 1: contradiction from the assumptions  
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   377
  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
2170
c5e460f1ebb4 Ran expandshort
paulson
parents: 2165
diff changeset
   378
by (dtac Crypt_imp_invKey_keysFor 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   379
(**LEVEL 11**)
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   380
by (Asm_full_simp_tac 1);
2170
c5e460f1ebb4 Ran expandshort
paulson
parents: 2165
diff changeset
   381
by (rtac disjI1 1);
2070
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   382
by (thin_tac "?PP-->?QQ" 1);
84f4572a6b20 New guarantees for each line of protocol
paulson
parents: 2050
diff changeset
   383
by (case_tac "Ba : lost" 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   384
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   385
			      unique_session_keys]) 2);
3441
6d2887123fa0 Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents: 3121
diff changeset
   386
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
6d2887123fa0 Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents: 3121
diff changeset
   387
			      Crypt_Spy_analz_lost]) 1);
2103
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   388
val lemma = result();
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   389
bfd2e8cca89c Tidied up the proof of A_trust_NS4
paulson
parents: 2070
diff changeset
   390
goal thy
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   391
 "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   392
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   393
\           : set evs;                                                \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   394
\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2122
diff changeset
   395
\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   396
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   397
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   398
                       addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   399
qed "A_trusts_NS4";