src/HOL/Auth/OtwayRees_AN.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3466 30791e5a69c4
child 3516 470626799511
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/OtwayRees
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     2
    ID:         $Id$
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     5
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     6
Inductive relation "otway" for the Otway-Rees protocol.
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     7
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     8
Simplified version with minimal encryption but explicit messages
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     9
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    10
From page 11 of
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    11
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    12
  IEEE Trans. SE 22 (1), 1996
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    13
*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    14
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    15
open OtwayRees_AN;
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    16
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    17
proof_timing:=true;
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    18
HOL_quantifiers := false;
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    19
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    20
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
    21
(*A "possibility property": there are traces that reach the end*)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    22
goal thy 
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
    23
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
    24
\        ==> EX K. EX NA. EX evs: otway lost.                                 \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
    25
\             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    26
\             : set evs";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    27
by (REPEAT (resolve_tac [exI,bexI] 1));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    28
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
    29
by possibility_tac;
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    30
result();
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    31
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    32
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    33
(**** Inductive proofs about otway ****)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    34
2106
1a52e2c5897e Generaly tidying up
paulson
parents: 2090
diff changeset
    35
(*Monotonicity*)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    36
goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    37
by (rtac subsetI 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    38
by (etac otway.induct 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    39
by (REPEAT_FIRST
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    40
    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    41
                              :: otway.intrs))));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    42
qed "otway_mono";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    43
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    44
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    45
goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    46
by (etac otway.induct 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    47
by (Auto_tac());
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    48
qed_spec_mp "not_Says_to_self";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    49
Addsimps [not_Says_to_self];
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    50
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    51
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    52
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    53
(** For reasoning about the encrypted portion of messages **)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    54
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    55
goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    56
\                X : analz (sees lost Spy evs)";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
    57
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    58
qed "OR4_analz_sees_Spy";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    59
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
    60
goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    61
\                  : set evs ==> K : parts (sees lost Spy evs)";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
    62
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    63
qed "Oops_parts_sees_Spy";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    64
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    65
(*OR4_analz_sees_Spy lets us treat those cases using the same 
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    66
  argument as for the Fake case.  This is possible for most, but not all,
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    67
  proofs, since Fake messages originate from the Spy. *)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    68
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    69
bind_thm ("OR4_parts_sees_Spy",
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    70
          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    71
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    72
(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    73
  We instantiate the variable to "lost" since leaving it as a Var would
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    74
  interfere with simplification.*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    75
val parts_induct_tac = 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    76
    let val tac = forw_inst_tac [("lost","lost")] 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    77
    in  etac otway.induct	   1 THEN 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    78
        tac OR4_parts_sees_Spy     6 THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    79
        tac Oops_parts_sees_Spy    7 THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    80
	prove_simple_subgoals_tac  1
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    81
    end;
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    82
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    83
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    84
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    85
    sends messages containing X! **)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    86
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    87
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    88
goal thy 
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    89
 "!!evs. evs : otway lost \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    90
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    91
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    92
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
    93
by (Blast_tac 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    94
qed "Spy_see_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    95
Addsimps [Spy_see_shrK];
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    96
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    97
goal thy 
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    98
 "!!evs. evs : otway lost \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
    99
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   100
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   101
qed "Spy_analz_shrK";
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   102
Addsimps [Spy_analz_shrK];
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   103
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   104
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   105
\                  evs : otway lost |] ==> A:lost";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   106
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   107
qed "Spy_see_shrK_D";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   108
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   109
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   110
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   111
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   112
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   113
(*Nobody can have used non-existent keys!*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   114
goal thy "!!evs. evs : otway lost ==>          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   115
\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   116
by parts_induct_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   117
(*Fake*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   118
by (best_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   119
      (!claset addIs [impOfSubs analz_subset_parts]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   120
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   121
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
3207
fe79ad367d77 renamed unsafe_addss to addss
oheimb
parents: 3121
diff changeset
   122
               addss (!simpset)) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   123
(*OR3*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   124
by (Blast_tac 1);
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2131
diff changeset
   125
qed_spec_mp "new_keys_not_used";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   126
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   127
bind_thm ("new_keys_not_analzd",
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   128
          [analz_subset_parts RS keysFor_mono,
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   129
           new_keys_not_used] MRS contra_subsetD);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   130
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   131
Addsimps [new_keys_not_used, new_keys_not_analzd];
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   132
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   133
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   134
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   135
(*** Proofs involving analz ***)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   136
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   137
(*Describes the form of K and NA when the Server sends this message.*)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   138
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   139
 "!!evs. [| Says Server B                                           \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   140
\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   141
\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   142
\             : set evs;                                            \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   143
\           evs : otway lost |]                                     \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   144
\        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   145
by (etac rev_mp 1);
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   146
by (etac otway.induct 1);
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   147
by (ALLGOALS Asm_simp_tac);
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   148
by (Blast_tac 1);
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   149
qed "Says_Server_message_form";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   150
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   151
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   152
(*For proofs involving analz.  We again instantiate the variable to "lost".*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   153
val analz_sees_tac = 
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   154
    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2106
diff changeset
   155
    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   156
    assume_tac 7 THEN
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2417
diff changeset
   157
    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   158
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   159
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   160
(****
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   161
 The following is to prove theorems of the form
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   162
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   163
  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2417
diff changeset
   164
  Key K : analz (sees lost Spy evs)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   165
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   166
 A more general formula must be proved inductively.
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   167
****)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   168
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   169
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   170
(** Session keys are not used to encrypt other session keys **)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   171
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   172
(*The equality makes the induction hypothesis easier to apply*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   173
goal thy  
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   174
 "!!evs. evs : otway lost ==>                                    \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   175
\  ALL K KK. KK <= Compl (range shrK) -->                        \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   176
\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   177
\            (K : KK | Key K : analz (sees lost Spy evs))";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   178
by (etac otway.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   179
by analz_sees_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   180
by (REPEAT_FIRST (resolve_tac [allI, impI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   181
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   182
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   183
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   184
by (spy_analz_tac 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   185
(*Base*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   186
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   187
qed_spec_mp "analz_image_freshK";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   188
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   189
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   190
goal thy
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   191
 "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   192
\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   193
\        (K = KAB | Key K : analz (sees lost Spy evs))";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   194
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   195
qed "analz_insert_freshK";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   196
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   197
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   198
(*** The Key K uniquely identifies the Server's  message. **)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   199
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   200
goal thy 
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
   201
 "!!evs. evs : otway lost ==>                              \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   202
\      EX A' B' NA' NB'. ALL A B NA NB.                    \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   203
\       Says Server B                                      \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   204
\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   205
\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   206
\       --> A=A' & B=B' & NA=NA' & NB=NB'";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   207
by (etac otway.induct 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   208
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   209
by (Step_tac 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   210
(*Remaining cases: OR3 and OR4*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   211
by (ex_strip_tac 2);
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   212
by (Blast_tac 2);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   213
by (expand_case_tac "K = ?y" 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   214
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   215
(*...we assume X is a recent message and handle this case by contradiction*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   216
by (blast_tac (!claset addSEs sees_Spy_partsEs
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   217
                       delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   218
val lemma = result();
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   219
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   220
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   221
goal thy 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   222
"!!evs. [| Says Server B                                           \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   223
\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   224
\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   225
\           : set evs;                                             \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   226
\          Says Server B'                                          \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   227
\            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   228
\              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   229
\           : set evs;                                             \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   230
\          evs : otway lost |]                                     \
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   231
\       ==> A=A' & B=B' & NA=NA' & NB=NB'";
2417
95f275c8476e New tactic: prove_unique_tac
paulson
parents: 2375
diff changeset
   232
by (prove_unique_tac lemma 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   233
qed "unique_session_keys";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   234
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   235
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   236
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   237
(**** Authenticity properties relating to NA ****)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   238
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   239
(*If the encrypted message appears then it originated with the Server!*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   240
goal thy 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   241
 "!!evs. [| A ~: lost;  evs : otway lost |]                 \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   242
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   243
\      : parts (sees lost Spy evs)                          \
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
   244
\     --> (EX NB. Says Server B                                          \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   245
\                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   246
\                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   247
\                  : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   248
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   249
by (Fake_parts_insert_tac 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   250
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   251
(*OR3*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   252
by (Blast_tac 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   253
qed_spec_mp "NA_Crypt_imp_Server_msg";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   254
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   255
2454
92f43ed48935 Corrected comments
paulson
parents: 2451
diff changeset
   256
(*Corollary: if A receives B's OR4 message then it originated with the Server.
92f43ed48935 Corrected comments
paulson
parents: 2451
diff changeset
   257
  Freshness may be inferred from nonce NA.*)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   258
goal thy 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   259
 "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   260
\            : set evs;                                                 \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   261
\           A ~: lost;  evs : otway lost |]                             \
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   262
\        ==> EX NB. Says Server B                                       \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   263
\                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   264
\                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   265
\                   : set evs";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   266
by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   267
                      addEs  sees_Spy_partsEs) 1);
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
   268
qed "A_trusts_OR4";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   269
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   270
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   271
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   272
    Does not in itself guarantee security: an attack could violate 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   273
    the premises, e.g. by having A=Spy **)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   274
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   275
goal thy 
2166
d276a806cc10 Tidying up: removing redundant assumptions, etc.
paulson
parents: 2160
diff changeset
   276
 "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   277
\        ==> Says Server B                                                 \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   278
\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   279
\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   280
\            : set evs -->                                                 \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   281
\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   282
\            Key K ~: analz (sees lost Spy evs)";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   283
by (etac otway.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   284
by analz_sees_tac;
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   285
by (ALLGOALS
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   286
    (asm_simp_tac (!simpset addcongs [conj_cong] 
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   287
                            addsimps [analz_insert_eq, not_parts_not_analz, 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   288
				      analz_insert_freshK]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   289
                            setloop split_tac [expand_if])));
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   290
(*Oops*)
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   291
by (blast_tac (!claset addSDs [unique_session_keys]) 4);
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   292
(*OR4*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   293
by (Blast_tac 3);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   294
(*OR3*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   295
by (blast_tac (!claset addSEs sees_Spy_partsEs
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   296
                       addIs [impOfSubs analz_subset_parts]) 2);
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   297
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   298
by (spy_analz_tac 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   299
val lemma = result() RS mp RS mp RSN(2,rev_notE);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   300
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   301
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   302
 "!!evs. [| Says Server B                                           \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   303
\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   304
\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   305
\             : set evs;                                            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   306
\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   307
\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   308
\        ==> Key K ~: analz (sees lost Spy evs)";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   309
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2837
diff changeset
   310
by (blast_tac (!claset addSEs [lemma]) 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   311
qed "Spy_not_see_encrypted_key";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   312
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   313
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   314
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   315
 "!!evs. [| C ~: {A,B,Server};                                      \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   316
\           Says Server B                                           \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   317
\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   318
\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   319
\             : set evs;                                            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   320
\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   321
\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2454
diff changeset
   322
\        ==> Key K ~: analz (sees lost C evs)";
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   323
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   324
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   325
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2837
diff changeset
   326
by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   327
qed "Agent_not_see_encrypted_key";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   328
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   329
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   330
(**** Authenticity properties relating to NB ****)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   331
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   332
(*If the encrypted message appears then it originated with the Server!*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   333
goal thy 
2106
1a52e2c5897e Generaly tidying up
paulson
parents: 2090
diff changeset
   334
 "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   335
\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
2106
1a52e2c5897e Generaly tidying up
paulson
parents: 2090
diff changeset
   336
\         : parts (sees lost Spy evs)                                       \
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   337
\        --> (EX NA. Says Server B                                          \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   338
\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   339
\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   340
\                     : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   341
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 3102
diff changeset
   342
by (Fake_parts_insert_tac 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   343
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   344
(*OR3*)
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   345
by (Blast_tac 1);
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   346
qed_spec_mp "NB_Crypt_imp_Server_msg";
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   347
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   348
2454
92f43ed48935 Corrected comments
paulson
parents: 2451
diff changeset
   349
(*Guarantee for B: if it gets a well-formed certificate then the Server
92f43ed48935 Corrected comments
paulson
parents: 2451
diff changeset
   350
  has sent the correct message in round 3.*)
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
   351
goal thy 
2106
1a52e2c5897e Generaly tidying up
paulson
parents: 2090
diff changeset
   352
 "!!evs. [| B ~: lost;  evs : otway lost;                                   \
2837
dee1c7f1f576 Trivial renamings (for consistency with CSFW papers)
paulson
parents: 2637
diff changeset
   353
\           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   354
\            : set evs |]                                                   \
2106
1a52e2c5897e Generaly tidying up
paulson
parents: 2090
diff changeset
   355
\        ==> EX NA. Says Server B                                           \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   356
\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   357
\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   358
\                     : set evs";
3102
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   359
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
4d01cdc119d2 Some blast_tac calls; more needed
paulson
parents: 2891
diff changeset
   360
                       addEs  sees_Spy_partsEs) 1);
2331
d6a56ff0d94e Minor renamings
paulson
parents: 2284
diff changeset
   361
qed "B_trusts_OR3";