src/HOL/Auth/OtwayRees_Bad.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
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:
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/OtwayRees_Bad
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     2
    ID:         $Id$
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     5
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     6
Inductive relation "otway" for the Otway-Rees protocol.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     7
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     8
The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    10
  Proc. Royal Soc. 426 (1989)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    11
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    12
This file illustrates the consequences of such errors.  We can still prove
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    13
impressive-looking properties such as Spy_not_see_encrypted_key, yet the
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    14
protocol is open to a middleperson attack.  Attempting to prove some key lemmas
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    15
indicates the possibility of this attack.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    16
*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    17
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    18
open OtwayRees_Bad;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    19
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    20
proof_timing:=true;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    21
HOL_quantifiers := false;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    22
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    23
(*Replacing the variable by a constant improves search speed by 50%!*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    24
val Says_imp_sees_Spy' = 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    25
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    26
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    27
(*A "possibility property": there are traces that reach the end*)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    28
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    29
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    30
\        ==> EX K. EX NA. EX evs: otway.          \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
    31
\               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    32
\                 : set evs";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    33
by (REPEAT (resolve_tac [exI,bexI] 1));
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    34
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    35
by possibility_tac;
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    36
result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    37
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    38
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    39
(**** Inductive proofs about otway ****)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    40
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    41
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    42
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    43
by (etac otway.induct 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    44
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    45
qed_spec_mp "not_Says_to_self";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    46
Addsimps [not_Says_to_self];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    47
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    48
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    49
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    50
(** For reasoning about the encrypted portion of messages **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    51
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    52
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    53
\                X : analz (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    54
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    55
qed "OR2_analz_sees_Spy";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    56
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    57
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    58
\                X : analz (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    59
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    60
qed "OR4_analz_sees_Spy";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    61
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    62
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    63
\                 ==> K : parts (sees lost Spy evs)";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
    64
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    65
qed "Oops_parts_sees_Spy";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    66
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    67
(*OR2_analz... and OR4_analz... let us treat those cases using the same 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    68
  argument as for the Fake case.  This is possible for most, but not all,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    69
  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
    70
  messages originate from the Spy. *)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    71
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    72
bind_thm ("OR2_parts_sees_Spy",
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    73
          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    74
bind_thm ("OR4_parts_sees_Spy",
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    75
          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    76
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    77
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    78
val parts_induct_tac = 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    79
    etac otway.induct 1 THEN 
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    80
    forward_tac [OR2_parts_sees_Spy] 4 THEN 
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    81
    forward_tac [OR4_parts_sees_Spy] 6 THEN
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    82
    forward_tac [Oops_parts_sees_Spy] 7 THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    83
    prove_simple_subgoals_tac 1;
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    84
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    85
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
    86
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    87
    sends messages containing X! **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    88
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    89
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    90
goal thy 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    91
 "!!evs. evs : otway \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    92
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    93
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    94
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    95
by (Blast_tac 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    96
qed "Spy_see_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    97
Addsimps [Spy_see_shrK];
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    98
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
    99
goal thy 
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   100
 "!!evs. evs : otway \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   101
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   102
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   103
qed "Spy_analz_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   104
Addsimps [Spy_analz_shrK];
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   105
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   106
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   107
\                  evs : otway |] ==> A:lost";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   108
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   109
qed "Spy_see_shrK_D";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   110
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   111
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: 2107
diff changeset
   112
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   113
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   114
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   115
(*Nobody can have used non-existent keys!*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   116
goal thy "!!evs. evs : otway ==>          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   117
\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   118
by parts_induct_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   119
(*Fake*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   120
by (best_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   121
      (!claset addIs [impOfSubs analz_subset_parts]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   122
               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
   123
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
3207
fe79ad367d77 renamed unsafe_addss to addss
oheimb
parents: 3121
diff changeset
   124
               addss (!simpset)) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   125
(*OR1-3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   126
by (ALLGOALS Blast_tac);
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2131
diff changeset
   127
qed_spec_mp "new_keys_not_used";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   128
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   129
bind_thm ("new_keys_not_analzd",
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
   130
          [analz_subset_parts RS keysFor_mono,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
   131
           new_keys_not_used] MRS contra_subsetD);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   132
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   133
Addsimps [new_keys_not_used, new_keys_not_analzd];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   134
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   135
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   136
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   137
(*** Proofs involving analz ***)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   138
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   139
(*Describes the form of K and NA when the Server sends this message.  Also
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   140
  for Oops case.*)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   141
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   142
 "!!evs. [| Says Server B                                                 \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   143
\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   144
\           evs : otway |]                                                \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   145
\     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   146
by (etac rev_mp 1);
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   147
by (etac otway.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   148
by (prove_simple_subgoals_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   149
by (Blast_tac 1); 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   150
qed "Says_Server_message_form";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   151
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   152
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   153
(*For proofs involving analz.*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   154
val analz_sees_tac = 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   155
    dtac OR2_analz_sees_Spy 4 THEN 
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   156
    dtac OR4_analz_sees_Spy 6 THEN
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   157
    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2417
diff changeset
   158
    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   159
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   160
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   161
(****
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   162
 The following is to prove theorems of the form
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   163
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   164
  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2417
diff changeset
   165
  Key K : analz (sees lost Spy evs)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   166
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   167
 A more general formula must be proved inductively.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   168
****)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   169
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   170
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   171
(** Session keys are not used to encrypt other session keys **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   172
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   173
(*The equality makes the induction hypothesis easier to apply*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   174
goal thy  
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   175
 "!!evs. evs : otway ==>                                         \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   176
\  ALL K KK. KK <= Compl (range shrK) -->                        \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   177
\            (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
   178
\            (K : KK | Key K : analz (sees lost Spy evs))";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
   179
by (etac otway.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   180
by analz_sees_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   181
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
   182
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
   183
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: 3207
diff changeset
   184
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   185
by (spy_analz_tac 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   186
(*Base*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   187
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   188
qed_spec_mp "analz_image_freshK";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   189
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   190
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   191
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   192
 "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>              \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   193
\        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
   194
\        (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
   195
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
   196
qed "analz_insert_freshK";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   197
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   198
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   199
(*** The Key K uniquely identifies the Server's  message. **)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   200
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   201
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   202
 "!!evs. evs : otway ==>                                                  \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   203
\   EX B' NA' NB' X'. ALL B NA NB X.                                      \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   204
\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   205
\     B=B' & NA=NA' & NB=NB' & X=X'";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2002
diff changeset
   206
by (etac otway.induct 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   207
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   208
by (Step_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   209
(*Remaining cases: OR3 and OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   210
by (ex_strip_tac 2);
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   211
by (Blast_tac 2);
2107
23e8f15ec95f The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents: 2052
diff changeset
   212
by (expand_case_tac "K = ?y" 1);
23e8f15ec95f The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents: 2052
diff changeset
   213
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   214
(*...we assume X is a recent message, and handle this case by contradiction*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   215
by (blast_tac (!claset addSEs sees_Spy_partsEs
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   216
                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   217
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   218
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   219
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   220
 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   221
\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   222
\           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
2417
95f275c8476e New tactic: prove_unique_tac
paulson
parents: 2375
diff changeset
   223
by (prove_unique_tac lemma 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   224
qed "unique_session_keys";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   225
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   226
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   227
(*Crucial security property, but not itself enough to guarantee correctness!*)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   228
goal thy 
2166
d276a806cc10 Tidying up: removing redundant assumptions, etc.
paulson
parents: 2160
diff changeset
   229
 "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
d276a806cc10 Tidying up: removing redundant assumptions, etc.
paulson
parents: 2160
diff changeset
   230
\        ==> Says Server B                                            \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   231
\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   232
\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   233
\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
2166
d276a806cc10 Tidying up: removing redundant assumptions, etc.
paulson
parents: 2160
diff changeset
   234
\            Key K ~: analz (sees lost Spy evs)";
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   235
by (etac otway.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   236
by analz_sees_tac;
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   237
by (ALLGOALS
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   238
    (asm_simp_tac (!simpset addcongs [conj_cong] 
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   239
                            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: 3207
diff changeset
   240
				      analz_insert_freshK]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   241
                            setloop split_tac [expand_if])));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   242
(*Oops*)
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   243
by (blast_tac (!claset addSDs [unique_session_keys]) 4);
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   244
(*OR4*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   245
by (Blast_tac 3);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   246
(*OR3*)
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   247
by (blast_tac (!claset addSEs sees_Spy_partsEs
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   248
                       addIs [impOfSubs analz_subset_parts]) 2);
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   249
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   250
by (spy_analz_tac 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   251
val lemma = result() RS mp RS mp RSN(2,rev_notE);
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   252
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   253
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   254
 "!!evs. [| Says Server B                                         \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   255
\            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   256
\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   257
\           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   258
\           A ~: lost;  B ~: lost;  evs : otway |]                \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   259
\        ==> Key K ~: analz (sees lost Spy evs)";
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   260
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   261
by (blast_tac (!claset addSEs [lemma]) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   262
qed "Spy_not_see_encrypted_key";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   263
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   264
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   265
(*** Attempting to prove stronger properties ***)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   266
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   267
(*Only OR1 can have caused such a part of a message to appear.
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   268
  I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   269
  Perhaps it's because OR2 has two similar-looking encrypted messages in
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   270
        this version.*)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   271
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   272
 "!!evs. [| A ~: lost;  A ~= B;  evs : otway |]                \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   273
\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   274
\             : parts (sees lost Spy evs) -->                  \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   275
\            Says A B {|NA, Agent A, Agent B,                  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   276
\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   277
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   278
by (Fake_parts_insert_tac 1);
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   279
by (Blast_tac 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   280
qed_spec_mp "Crypt_imp_OR1";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   281
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   282
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   283
(*Crucial property: If the encrypted message appears, and A has used NA
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   284
  to start a run, then it originated with the Server!*)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   285
(*Only it is FALSE.  Somebody could make a fake message to Server
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   286
          substituting some other nonce NA' for NB.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   287
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   288
 "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                         \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   289
\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   290
\            Says A B {|NA, Agent A, Agent B,                      \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   291
\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   292
\             : set evs -->                                    \
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   293
\            (EX B NB. Says Server B                           \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   294
\                 {|NA,                                        \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   295
\                   Crypt (shrK A) {|NA, Key K|},              \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   296
\                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   297
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   298
by (Fake_parts_insert_tac 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   299
(*OR1: it cannot be a new Nonce, contradiction.*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   300
by (blast_tac (!claset addSIs [parts_insertI]
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   301
                      addSEs sees_Spy_partsEs) 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   302
(*OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   303
by (REPEAT (Safe_step_tac 2));
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   304
by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   305
by (blast_tac (!claset addSIs [Crypt_imp_OR1]
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2837
diff changeset
   306
                       addEs  sees_Spy_partsEs) 2);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   307
(*OR3*)  (** LEVEL 5 **)
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   308
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   309
by (step_tac (!claset delrules [disjCI, impCE]) 1);
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   310
(*The hypotheses at this point suggest an attack in which nonce NA is used
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   311
  in two different roles:
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   312
          Says B' Server
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   313
           {|Nonce NAa, Agent Aa, Agent A,
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   314
             Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   315
             Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   316
          : set evsa;
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   317
          Says A B
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   318
           {|Nonce NA, Agent A, Agent B,
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   319
             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   320
          : set evsa 
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   321
*)
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2107
diff changeset
   322
writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
2002
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   323
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   324
2052
d9f7f4b2613e Working again with new theory Shared
paulson
parents: 2032
diff changeset
   325
(*Thus the key property A_can_trust probably fails too.*)