src/HOL/Auth/OtwayRees_Bad.ML
author paulson
Mon, 23 Sep 1996 17:41:57 +0200
changeset 2002 ed423882c6a9
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
Bad version of Otway-Rees and the new attack on it
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
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    13
impressive-looking properties such as Enemy_not_see_encrypted_key, yet the
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
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    23
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    24
(*Weak liveness: there are traces that reach the end*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    25
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    26
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    27
\        ==> EX K. EX NA. EX evs: otway.          \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    28
\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    29
\                 : set_of_list evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    30
by (REPEAT (resolve_tac [exI,bexI] 1));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    31
br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    32
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    33
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    34
by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    35
result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    36
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
(**** Inductive proofs about otway ****)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    39
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    40
(*The Enemy can see more than anybody else, except for their initial state*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    41
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    42
 "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    43
\     sees A evs <= initState A Un sees Enemy evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    44
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    45
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    46
			        addss (!simpset))));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    47
qed "sees_agent_subset_sees_Enemy";
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
(*Nobody sends themselves messages*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    51
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    52
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    53
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    54
qed_spec_mp "not_Says_to_self";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    55
Addsimps [not_Says_to_self];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    56
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
    57
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    58
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    59
(** For reasoning about the encrypted portion of messages **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    60
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    61
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    62
\                X : analz (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    63
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    64
qed "OR2_analz_sees_Enemy";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    65
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    66
goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    67
\                X : analz (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    68
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    69
qed "OR4_analz_sees_Enemy";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    70
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    71
goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    72
\                K : parts (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    73
by (fast_tac (!claset addSEs partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    74
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    75
qed "Reveal_parts_sees_Enemy";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    76
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    77
(*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
    78
  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
    79
  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    80
  messages originate from the Enemy. *)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    81
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    82
val parts_Fake_tac = 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    83
    dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    84
    dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    85
    dtac Reveal_parts_sees_Enemy 7;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    86
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    87
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    88
(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    89
    sends messages containing X! **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    90
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    91
(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    92
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    93
 "!!evs. [| evs : otway;  A ~: bad |]    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    94
\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    95
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    96
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    97
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    98
(*Deals with Fake message*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
    99
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   100
			     impOfSubs Fake_parts_insert]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   101
qed "Enemy_not_see_shrK";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   102
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   103
bind_thm ("Enemy_not_analz_shrK",
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   104
	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   105
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   106
Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   107
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   108
(*We go to some trouble to preserve R in the 3rd and 4th subgoals
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   109
  As usual fast_tac cannot be used because it uses the equalities too soon*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   110
val major::prems = 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   111
goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   112
\             evs : otway;                                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   113
\             A:bad ==> R                                  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   114
\           |] ==> R";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   115
br ccontr 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   116
br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   117
by (swap_res_tac prems 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   118
by (ALLGOALS (fast_tac (!claset addIs prems)));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   119
qed "Enemy_see_shrK_E";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   120
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   121
bind_thm ("Enemy_analz_shrK_E", 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   122
	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   123
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   124
AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   125
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   126
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   127
(*** Future keys can't be seen or used! ***)
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
(*Nobody can have SEEN keys that will be generated in the future.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   130
  This has to be proved anew for each protocol description,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   131
  but should go by similar reasoning every time.  Hardest case is the
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   132
  standard Fake rule.  
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   133
      The Union over C is essential for the induction! *)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   134
goal thy "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   135
\                length evs <= length evs' --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   136
\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   137
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   138
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   139
(*auto_tac does not work here, as it performs safe_tac first*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   140
by (ALLGOALS Asm_simp_tac);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   141
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   142
				       impOfSubs parts_insert_subset_Un,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   143
				       Suc_leD]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   144
			        addss (!simpset))));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   145
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   146
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   147
(*Variant needed for the main theorem below*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   148
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   149
 "!!evs. [| evs : otway;  length evs <= length evs' |]    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   150
\        ==> Key (newK evs') ~: parts (sees C evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   151
by (fast_tac (!claset addDs [lemma]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   152
qed "new_keys_not_seen";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   153
Addsimps [new_keys_not_seen];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   154
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   155
(*Another variant: old messages must contain old keys!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   156
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   157
 "!!evs. [| Says A B X : set_of_list evs;  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   158
\           Key (newK evt) : parts {X};    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   159
\           evs : otway                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   160
\        |] ==> length evt < length evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   161
br ccontr 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   162
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   163
	              addIs  [impOfSubs parts_mono, leI]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   164
qed "Says_imp_old_keys";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   165
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
(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
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
goal thy "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   170
\                length evs <= length evs' --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   171
\                          Nonce (newN evs') ~: (UN C. parts (sees C evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   172
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   173
(*auto_tac does not work here, as it performs safe_tac first*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   174
by (ALLGOALS (asm_simp_tac (!simpset addsimps [de_Morgan_disj]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   175
                                     addcongs [conj_cong])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   176
by (REPEAT_FIRST (fast_tac (!claset (*60 seconds???*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   177
			      addSEs [MPair_parts]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   178
			      addDs  [Says_imp_sees_Enemy RS parts.Inj,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   179
				      impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   180
				      impOfSubs parts_insert_subset_Un,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   181
				      Suc_leD]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   182
			      addss (!simpset))));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   183
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   184
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   185
(*Variant needed for the main theorem below*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   186
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   187
 "!!evs. [| evs : otway;  length evs <= length evs' |]    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   188
\        ==> Nonce (newN evs') ~: parts (sees C evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   189
by (fast_tac (!claset addDs [lemma]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   190
qed "new_nonces_not_seen";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   191
Addsimps [new_nonces_not_seen];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   192
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   193
(*Another variant: old messages must contain old nonces!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   194
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   195
 "!!evs. [| Says A B X : set_of_list evs;  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   196
\           Nonce (newN evt) : parts {X};    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   197
\           evs : otway                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   198
\        |] ==> length evt < length evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   199
br ccontr 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   200
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   201
	              addIs  [impOfSubs parts_mono, leI]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   202
qed "Says_imp_old_nonces";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   203
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   204
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   205
(*Nobody can have USED keys that will be generated in the future.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   206
  ...very like new_keys_not_seen*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   207
goal thy "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   208
\                length evs <= length evs' --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   209
\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   210
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   211
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   212
by (ALLGOALS Asm_simp_tac);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   213
(*OR1 and OR3*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   214
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   215
(*Fake, OR2, OR4: these messages send unknown (X) components*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   216
by (EVERY 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   217
    (map
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   218
     (best_tac
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   219
      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   220
		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   221
		      Suc_leD]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   222
	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   223
	       addss (!simpset)))
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   224
     [3,2,1]));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   225
(*Reveal: dummy message*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   226
by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   227
		      addIs  [less_SucI, impOfSubs keysFor_mono]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   228
		      addss (!simpset addsimps [le_def])) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   229
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   230
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   231
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   232
 "!!evs. [| evs : otway;  length evs <= length evs' |]    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   233
\        ==> newK evs' ~: keysFor (parts (sees C evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   234
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   235
qed "new_keys_not_used";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   236
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   237
bind_thm ("new_keys_not_analzd",
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   238
	  [analz_subset_parts RS keysFor_mono,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   239
	   new_keys_not_used] MRS contra_subsetD);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   240
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   241
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
   242
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   243
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   244
(** Lemmas concerning the form of items passed in messages **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   245
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   246
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   247
(****
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   248
 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
   249
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   250
          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   251
          Key K : analz (sees Enemy evs)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   252
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   253
 A more general formula must be proved inductively.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   254
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   255
****)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   256
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   257
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   258
(*NOT useful in this form, but it says that session keys are not used
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   259
  to encrypt messages containing other keys, in the actual protocol.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   260
  We require that agents should behave like this subsequently also.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   261
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   262
 "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   263
\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   264
\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   265
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   266
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   267
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   268
(*Deals with Faked messages*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   269
by (best_tac (!claset addSEs partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   270
		      addDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   271
                             impOfSubs parts_insert_subset_Un]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   272
                      addss (!simpset)) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   273
(*Base case and Reveal*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   274
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   275
result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   276
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   277
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   278
(** Specialized rewriting for this proof **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   279
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   280
Delsimps [image_insert];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   281
Addsimps [image_insert RS sym];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   282
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   283
Delsimps [image_Un];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   284
Addsimps [image_Un RS sym];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   285
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   286
goal thy "insert (Key (newK x)) (sees A evs) = \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   287
\         Key `` (newK``{x}) Un (sees A evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   288
by (Fast_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   289
val insert_Key_singleton = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   290
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   291
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   292
\         Key `` (f `` (insert x E)) Un C";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   293
by (Fast_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   294
val insert_Key_image = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   295
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   296
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   297
(*This lets us avoid analyzing the new message -- unless we have to!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   298
(*NEEDED??*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   299
goal thy "synth (analz (sees Enemy evs)) <=   \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   300
\         synth (analz (sees Enemy (Says A B X # evs)))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   301
by (Simp_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   302
br (subset_insertI RS analz_mono RS synth_mono) 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   303
qed "synth_analz_thin";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   304
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   305
AddIs [impOfSubs synth_analz_thin];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   306
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   307
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   308
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   309
(** 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
   310
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   311
(*Describes the form of Key K when the following message is sent.  The use of
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   312
  "parts" strengthens the induction hyp for proving the Fake case.  The
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   313
  assumptions on A are needed to prevent its being a Faked message.  (Based
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   314
  on NS_Shared/Says_S_message_form) *)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   315
goal thy
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   316
 "!!evs. evs: otway ==>  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   317
\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   318
\          A ~: bad --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   319
\        (EX evt:otway. K = newK evt)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   320
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   321
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   322
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   323
(*Deals with Fake message*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   324
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   325
			     impOfSubs Fake_parts_insert]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   326
val lemma = result() RS mp;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   327
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   328
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   329
(*EITHER describes the form of Key K when the following message is sent, 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   330
  OR     reduces it to the Fake case.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   331
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   332
 "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   333
\           evs : otway |]                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   334
\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   335
by (excluded_middle_tac "A : bad" 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   336
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   337
	              addss (!simpset)) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   338
by (forward_tac [lemma] 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   339
by (fast_tac (!claset addEs  partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   340
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   341
by (Fast_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   342
qed "Reveal_message_form";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   343
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   344
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   345
(*Lemma for the trivial direction of the if-and-only-if*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   346
goal thy  
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   347
 "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   348
\         (K : nE | Key K : analz sEe)  ==>     \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   349
\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   350
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   351
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   352
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   353
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   354
(*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
   355
goal thy  
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   356
 "!!evs. evs : otway ==> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   357
\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   358
\           (K : newK``E | Key K : analz (sees Enemy evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   359
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   360
bd OR2_analz_sees_Enemy 4;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   361
bd OR4_analz_sees_Enemy 6;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   362
bd Reveal_message_form 7;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   363
by (REPEAT_FIRST (ares_tac [allI, lemma]));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   364
by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   365
by (ALLGOALS (*Takes 28 secs*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   366
    (asm_simp_tac 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   367
     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   368
			 @ pushes)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   369
               setloop split_tac [expand_if])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   370
(** LEVEL 7 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   371
(*Reveal case 2, OR4, OR2, Fake*) 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   372
by (EVERY (map enemy_analz_tac [7,5,3,2]));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   373
(*Reveal case 1, OR3, Base*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   374
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   375
qed_spec_mp "analz_image_newK";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   376
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   377
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   378
goal thy
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   379
 "!!evs. evs : otway ==>                               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   380
\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   381
\        (K = newK evt | Key K : analz (sees Enemy evs))";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   382
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   383
				   insert_Key_singleton]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   384
by (Fast_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   385
qed "analz_insert_Key_newK";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   386
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   387
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   388
(*Describes the form of K and NA when the Server sends this message.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   389
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   390
 "!!evs. [| Says Server B \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   391
\            {|NA, Crypt {|NA, K|} (shrK A),                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   392
\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   393
\           evs : otway |]                                        \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   394
\        ==> (EX evt:otway. K = Key(newK evt)) &            \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   395
\            (EX i. NA = Nonce i)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   396
be rev_mp 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   397
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   398
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   399
qed "Says_Server_message_form";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   400
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   401
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   402
(*Crucial security property, but not itself enough to guarantee correctness!
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   403
  The need for quantification over N, C seems to indicate the problem.
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   404
  Omitting the Reveal message from the description deprives us of even 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   405
	this clue. *)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   406
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   407
 "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]        \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   408
\    ==> Says Server B \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   409
\          {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   410
\            Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   411
\        (ALL N C. Says C Enemy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   412
\        Key(newK evt) ~: analz (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   413
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   414
bd OR2_analz_sees_Enemy 4;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   415
bd OR4_analz_sees_Enemy 6;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   416
bd Reveal_message_form 7;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   417
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   418
by (ALLGOALS
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   419
    (asm_full_simp_tac 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   420
     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   421
			  analz_insert_Key_newK] @ pushes)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   422
               setloop split_tac [expand_if])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   423
(** LEVEL 6 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   424
(*Reveal case 1*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   425
by (Fast_tac 5);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   426
(*OR3*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   427
by (fast_tac (!claset addSIs [parts_insertI]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   428
		      addEs [Says_imp_old_keys RS less_irrefl]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   429
	              addss (!simpset)) 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   430
(*Reveal case 2, OR4, OR2, Fake*) 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   431
br conjI 3;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   432
by (REPEAT (enemy_analz_tac 1));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   433
val lemma = result() RS mp RS mp RSN(2,rev_notE);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   434
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   435
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   436
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   437
(*WEAK VERSION: NEED TO ELIMINATE QUANTIFICATION OVER N, C!!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   438
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   439
 "!!evs. [| Says Server B \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   440
\            {|NA, Crypt {|NA, K|} (shrK A),                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   441
\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   442
\           (ALL N C. Says C Enemy {|N, K|} ~: set_of_list evs);  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   443
\           A ~: bad;  B ~: bad;  evs : otway |]                  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   444
\        ==> K ~: analz (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   445
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   446
by (fast_tac (!claset addSEs [lemma]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   447
qed "Enemy_not_see_encrypted_key";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   448
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   449
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   450
(*** Attempting to prove stronger properties ***)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   451
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   452
(** The Key K uniquely identifies the Server's  message. **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   453
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   454
fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   455
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   456
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   457
 "!!evs. evs : otway ==>                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   458
\      EX A' B' NA' NB'. ALL A B NA NB.                    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   459
\       Says Server B \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   460
\            {|NA, Crypt {|NA, K|} (shrK A),                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   461
\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   462
\       A=A' & B=B' & NA=NA' & NB=NB'";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   463
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   464
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
   465
by (Step_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   466
(*Remaining cases: OR3 and OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   467
by (ex_strip_tac 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   468
by (Fast_tac 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   469
by (excluded_middle_tac "K = Key(newK evsa)" 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   470
by (Asm_simp_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   471
by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   472
(*...we assume X is a very new message, and handle this case by contradiction*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   473
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   474
	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   475
	              addss (!simpset addsimps [parts_insertI])) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   476
val lemma = result();
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   477
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   478
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   479
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   480
 "!!evs. [| Says Server B                                          \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   481
\              {|NA, Crypt {|NA, K|} (shrK A),                     \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   482
\                    Crypt {|NB, K|} (shrK B)|}                    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   483
\            : set_of_list evs;                                    \ 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   484
\           Says Server B'                                         \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   485
\              {|NA', Crypt {|NA', K|} (shrK A'),                  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   486
\                     Crypt {|NB', K|} (shrK B')|}                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   487
\            : set_of_list evs;                                    \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   488
\           evs : otway |]                                         \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   489
\        ==> A=A' & B=B' & NA=NA' & NB=NB'";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   490
bd lemma 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   491
by (REPEAT (etac exE 1));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   492
(*Duplicate the assumption*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   493
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   494
by (fast_tac (!claset addSDs [spec]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   495
qed "unique_session_keys";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   496
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   497
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   498
(*Could probably remove the A ~= B premise using another induction*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   499
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   500
 "!!evs. [| A ~: bad;  A ~= B; evs : otway |]               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   501
\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   502
\             : parts (sees Enemy evs) -->                  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   503
\            Says A B {|NA, Agent A, Agent B,               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   504
\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   505
\             : set_of_list evs";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   506
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   507
by parts_Fake_tac;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   508
by (ALLGOALS Asm_simp_tac);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   509
(*Fake*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   510
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   511
			      impOfSubs Fake_parts_insert]) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   512
by (Auto_tac());
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   513
qed_spec_mp "Crypt_imp_OR1";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   514
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   515
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   516
(*This key property is FALSE.  Somebody could make a fake message to Server
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   517
          substituting some other nonce NA' for NB.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   518
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   519
 "!!evs. [| A ~: bad;  evs : otway |]                                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   520
\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   521
\            Says A B {|Nonce NA, Agent A, Agent B,  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   522
\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   523
\             : set_of_list evs --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   524
\            (EX B NB. Says Server B               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   525
\                 {|Nonce NA,               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   526
\                   Crypt {|Nonce NA, Key K|} (shrK A),              \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   527
\                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   528
\                   : set_of_list evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   529
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   530
fun ftac rl = forward_tac [rl];
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   531
by (
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   532
    ftac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   533
    ftac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   534
    ftac Reveal_parts_sees_Enemy 7);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   535
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   536
(*  by parts_Fake_tac;  ?*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   537
by (ALLGOALS Asm_simp_tac);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   538
(*Fake*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   539
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   540
			      impOfSubs Fake_parts_insert]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   541
(*OR1: it cannot be a new Nonce, contradiction.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   542
by (fast_tac (!claset addSIs [parts_insertI]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   543
		      addSEs partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   544
		      addEs [Says_imp_old_nonces RS less_irrefl]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   545
	              addss (!simpset)) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   546
(*OR3 and OR4*)  (** LEVEL 5 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   547
(*OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   548
by (REPEAT (Safe_step_tac 2));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   549
by (best_tac (!claset addSDs [parts_cut]) 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   550
by (best_tac (!claset addSDs [parts_cut]) 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   551
by (forward_tac [Crypt_imp_OR1] 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   552
by (fast_tac (!claset addEs  partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   553
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 4);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   554
by (REPEAT (Fast_tac 2));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   555
(*OR3*)  (** LEVEL 11 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   556
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   557
fr impI;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   558
by (REPEAT (etac conjE 1 ORELSE hyp_subst_tac 1));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   559
fr impI;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   560
(*The hypotheses at this point suggest an attack in which nonce NA is used
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   561
  in two different places*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   562
writeln "GIVE UP!";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   563
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   564
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   565
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   566
(*What can A deduce from receipt of OR4?  This too is probably FALSE*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   567
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   568
 "!!evs. [| A ~: bad;  evs : otway |]                                 \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   569
\        ==> ALL B' NA K B.  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   570
\            Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   571
\             : set_of_list evs -->  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   572
\            Says A B {|Nonce NA, Agent A, Agent B,                     \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   573
\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   574
\             : set_of_list evs --> \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   575
\            (EX NB. Says Server B \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   576
\                     {|Nonce NA,               \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   577
\                       Crypt {|Nonce NA, Key K|} (shrK A),              \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   578
\                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   579
\                       : set_of_list evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   580
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   581
by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   582
(*OR2*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   583
by (Fast_tac 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   584
(*OR1: it cannot be a new Nonce, contradiction.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   585
by (fast_tac (!claset addSIs [parts_insertI]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   586
		      addEs [Says_imp_old_nonces RS less_irrefl]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   587
	              addss (!simpset)) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   588
by (ALLGOALS 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   589
    (asm_simp_tac (!simpset addsimps [all_conj_distrib, de_Morgan_disj, de_Morgan_conj])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   590
(*Fake, OR4*) (** LEVEL 5 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   591
by (step_tac (!claset delrules [MPair_analz]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   592
by (ALLGOALS Asm_simp_tac);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   593
by (fast_tac (!claset addSDs [spec]) 4);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   594
by (forward_tac [Crypt_imp_OR1] 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   595
by (fast_tac (!claset addEs  partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   596
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 5);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   597
by (REPEAT (Fast_tac 3));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   598
(** LEVEL 11 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   599
(*Fake (??) and OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   600
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   601
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   602
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,  de_Morgan_disj, de_Morgan_conj])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   603
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   604
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   605
(*** Session keys are issued at most once, and identify the principals ***)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   606
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   607
(** First, two lemmas for the Fake, OR2 and OR4 cases **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   608
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   609
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   610
 "!!evs. [| X : synth (analz (sees Enemy evs));                \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   611
\           Crypt X' (shrK C) : parts{X};                      \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   612
\           C ~: bad;  evs : otway |]  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   613
\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   614
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   615
	              addDs [impOfSubs parts_insert_subset_Un]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   616
                      addss (!simpset)) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   617
qed "Crypt_Fake_parts";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   618
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   619
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   620
 "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   621
\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   622
\            Crypt X' K : parts {Y}";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   623
bd parts_singleton 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   624
by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   625
qed "Crypt_parts_singleton";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   626
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   627
(*The Key K uniquely identifies a pair of senders in the message encrypted by
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   628
  C, but if C=Enemy then he could send all sorts of nonsense.*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   629
goal thy 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   630
 "!!evs. evs : otway ==>                                     \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   631
\      EX A B. ALL C.                                        \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   632
\         C ~: bad -->                                       \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   633
\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   634
\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   635
by (Simp_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   636
be otway.induct 1;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   637
bd OR2_analz_sees_Enemy 4;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   638
bd OR4_analz_sees_Enemy 6;
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   639
by (ALLGOALS 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   640
    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   641
by (REPEAT_FIRST (etac exE));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   642
(*OR4*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   643
by (ex_strip_tac 4);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   644
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   645
			      Crypt_parts_singleton]) 4);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   646
(*OR3: Case split propagates some context to other subgoal...*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   647
	(** LEVEL 8 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   648
by (excluded_middle_tac "K = newK evsa" 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   649
by (Asm_simp_tac 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   650
by (REPEAT (ares_tac [exI] 3));
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   651
(*...we prove this case by contradiction: the key is too new!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   652
by (fast_tac (!claset addIs [parts_insertI]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   653
		      addSEs partsEs
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   654
		      addEs [Says_imp_old_keys RS less_irrefl]
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   655
	              addss (!simpset)) 3);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   656
(*OR2*) (** LEVEL 12 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   657
(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   658
by (ex_strip_tac 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   659
by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   660
by (Simp_tac 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   661
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   662
			      Crypt_parts_singleton]) 2);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   663
(*Fake*) (** LEVEL 16 **)
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   664
by (ex_strip_tac 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   665
by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   666
qed "unique_session_keys2";
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   667
ed423882c6a9 Bad version of Otway-Rees and the new attack on it
paulson
parents:
diff changeset
   668