src/HOL/Auth/Yahalom2.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3501 4ab477ffb4c6
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:
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Yahalom2
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     2
    ID:         $Id$
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     5
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     6
Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     7
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     8
This version trades encryption of NB for additional explicitness in YM3.
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
     9
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    10
From page 259 of
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    11
  Burrows, Abadi and Needham.  A Logic of Authentication.
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    12
  Proc. Royal Soc. 426 (1989)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    13
*)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    14
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    15
open Yahalom2;
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    16
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    17
proof_timing:=true;
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    18
HOL_quantifiers := false;
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    19
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    20
(*Replacing the variable by a constant improves speed*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    21
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    22
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    23
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
    24
(*A "possibility property": there are traces that reach the end*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    25
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    26
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]        \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    27
\        ==> EX X NB K. EX evs: yahalom lost.          \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
    28
\               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    29
by (REPEAT (resolve_tac [exI,bexI] 1));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    30
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    31
          yahalom.YM4) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    32
by possibility_tac;
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    33
result();
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    34
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    35
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    36
(**** Inductive proofs about yahalom ****)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    37
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    38
(*Monotonicity*)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    39
goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    40
by (rtac subsetI 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    41
by (etac yahalom.induct 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    42
by (REPEAT_FIRST
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    43
    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    44
			       :: yahalom.intrs))));
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    45
qed "yahalom_mono";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    46
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    47
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    48
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
    49
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    50
by (etac yahalom.induct 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    51
by (Auto_tac());
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    52
qed_spec_mp "not_Says_to_self";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    53
Addsimps [not_Says_to_self];
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    54
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    55
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    56
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    57
(** For reasoning about the encrypted portion of messages **)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    58
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    59
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
    60
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    61
\                X : analz (sees lost Spy evs)";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    62
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    63
qed "YM4_analz_sees_Spy";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    64
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    65
bind_thm ("YM4_parts_sees_Spy",
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    66
          YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    67
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
    68
(*Relates to both YM4 and Oops*)
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    69
goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    70
\                K : parts (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    71
by (blast_tac (!claset addSEs partsEs
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    72
                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    73
qed "YM4_Key_parts_sees_Spy";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    74
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    75
(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    76
  We instantiate the variable to "lost" since leaving it as a Var would
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    77
  interfere with simplification.*)
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    78
val parts_sees_tac = 
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    79
    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    80
    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    81
    prove_simple_subgoals_tac  1;
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    82
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    83
val parts_induct_tac = 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    84
    etac yahalom.induct 1 THEN parts_sees_tac;
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
    85
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    86
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    87
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    88
    sends messages containing X! **)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    89
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    90
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    91
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    92
 "!!evs. evs : yahalom lost \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    93
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    94
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    95
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    96
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    97
qed "Spy_see_shrK";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    98
Addsimps [Spy_see_shrK];
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
    99
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   100
goal thy 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   101
 "!!evs. evs : yahalom lost \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   102
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   103
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   104
qed "Spy_analz_shrK";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   105
Addsimps [Spy_analz_shrK];
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   106
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   107
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   108
\                  evs : yahalom lost |] ==> A:lost";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   109
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   110
qed "Spy_see_shrK_D";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   111
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   112
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   113
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   114
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   115
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   116
(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   117
goal thy "!!evs. evs : yahalom lost ==>          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   118
\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   119
by parts_induct_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   120
(*YM4: Key K is not fresh!*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   121
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   122
(*YM3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   123
by (blast_tac (!claset addss (!simpset)) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   124
(*Fake*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   125
by (best_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   126
      (!claset addIs [impOfSubs analz_subset_parts]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   127
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   128
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   129
               addss (!simpset)) 1);
2160
ad4382e546fc Simplified new_keys_not_seen, etc.: replaced the
paulson
parents: 2155
diff changeset
   130
qed_spec_mp "new_keys_not_used";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   131
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   132
bind_thm ("new_keys_not_analzd",
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   133
          [analz_subset_parts RS keysFor_mono,
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   134
           new_keys_not_used] MRS contra_subsetD);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   135
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   136
Addsimps [new_keys_not_used, new_keys_not_analzd];
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   137
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   138
(*Describes the form of K when the Server sends this message.  Useful for
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   139
  Oops as well as main secrecy property.*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   140
goal thy 
3501
4ab477ffb4c6 Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents: 3466
diff changeset
   141
 "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   142
\            : set evs;                                                 \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   143
\           evs : yahalom lost |]                                       \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   144
\        ==> K ~: range shrK & A ~= B";
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   145
by (etac rev_mp 1);
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   146
by (etac yahalom.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   147
by (ALLGOALS Asm_simp_tac);
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   148
qed "Says_Server_message_form";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   149
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   150
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   151
(*For proofs involving analz.  We again instantiate the variable to "lost".*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   152
val analz_sees_tac = 
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   153
    dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   154
    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: 2451
diff changeset
   155
    assume_tac 7 THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   156
    REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   157
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   158
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   159
(****
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   160
 The following is to prove theorems of the form
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   161
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   162
          Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   163
          Key K : analz (sees lost Spy evs)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   164
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   165
 A more general formula must be proved inductively.
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   166
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   167
****)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   168
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   169
(** Session keys are not used to encrypt other session keys **)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   170
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   171
goal thy  
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   172
 "!!evs. evs : yahalom lost ==>                                  \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   173
\  ALL K KK. KK <= Compl (range shrK) -->                        \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   174
\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   175
\            (K : KK | Key K : analz (sees lost Spy evs))";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   176
by (etac yahalom.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   177
by analz_sees_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   178
by (REPEAT_FIRST (resolve_tac [allI, impI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   179
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   180
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   181
(*Fake*) 
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   182
by (spy_analz_tac 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   183
(*Base*)
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   184
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   185
qed_spec_mp "analz_image_freshK";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   186
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   187
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   188
 "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   189
\        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: 2451
diff changeset
   190
\        (K = KAB | Key K : analz (sees lost Spy evs))";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   191
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   192
qed "analz_insert_freshK";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   193
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   194
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   195
(*** The Key K uniquely identifies the Server's  message. **)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   196
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   197
goal thy 
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   198
 "!!evs. evs : yahalom lost ==>                                     \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   199
\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   200
\          Says Server A                                            \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   201
\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   202
\          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   203
by (etac yahalom.induct 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   204
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   205
by (Step_tac 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   206
(*Remaining case: YM3*)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   207
by (expand_case_tac "K = ?y" 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   208
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   209
(*...we assume X is a recent message and handle this case by contradiction*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   210
by (blast_tac (!claset addSEs sees_Spy_partsEs
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   211
                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   212
                      addss (!simpset addsimps [parts_insertI])) 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   213
val lemma = result();
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   214
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   215
goal thy 
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   216
"!!evs. [| Says Server A                                            \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   217
\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   218
\           : set evs;                                              \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   219
\          Says Server A'                                           \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   220
\           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   221
\           : set evs;                                              \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   222
\          evs : yahalom lost |]                                    \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   223
\       ==> A=A' & B=B' & na=na' & nb=nb'";
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2377
diff changeset
   224
by (prove_unique_tac lemma 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   225
qed "unique_session_keys";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   226
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   227
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   228
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   229
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   230
goal thy 
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   231
 "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   232
\           evs : yahalom lost |]                                    \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   233
\        ==> Says Server A                                           \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   234
\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   235
\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   236
\             : set evs -->                                          \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   237
\            Says A Spy {|na, nb, Key K|} ~: set evs -->             \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   238
\            Key K ~: analz (sees lost Spy evs)";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   239
by (etac yahalom.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   240
by analz_sees_tac;
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   241
by (ALLGOALS
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   242
    (asm_simp_tac 
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   243
     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   244
			 analz_insert_freshK]
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   245
               setloop split_tac [expand_if])));
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   246
(*Oops*)
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   247
by (blast_tac (!claset addDs [unique_session_keys]) 3);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   248
(*YM3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   249
by (blast_tac (!claset delrules [impCE]
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   250
                       addSEs sees_Spy_partsEs
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   251
                       addIs [impOfSubs analz_subset_parts]) 2);
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   252
(*Fake*) 
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   253
by (spy_analz_tac 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   254
val lemma = result() RS mp RS mp RSN(2,rev_notE);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   255
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   256
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   257
(*Final version*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   258
goal thy 
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   259
 "!!evs. [| Says Server A                                         \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   260
\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   261
\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   262
\           : set evs;                                            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   263
\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   264
\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   265
\        ==> Key K ~: analz (sees lost Spy evs)";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   266
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   267
by (blast_tac (!claset addSEs [lemma]) 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   268
qed "Spy_not_see_encrypted_key";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   269
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   270
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   271
(*And other agents don't see the key either.*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   272
goal thy 
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   273
 "!!evs. [| C ~: {A,B,Server};                                    \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   274
\           Says Server A                                         \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   275
\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   276
\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   277
\           : set evs;                                            \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   278
\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   279
\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   280
\        ==> Key K ~: analz (sees lost C evs)";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   281
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   282
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   283
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   284
by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   285
qed "Agent_not_see_encrypted_key";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   286
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   287
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   288
(** Security Guarantee for A upon receiving YM3 **)
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   289
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   290
(*If the encrypted message appears then it originated with the Server.
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   291
  May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   292
goal thy
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   293
 "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   294
\            : parts (sees lost Spy evs);                              \
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   295
\           A ~: lost;  evs : yahalom lost |]                          \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   296
\         ==> EX nb. Says Server A                                     \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   297
\                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   298
\                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   299
\                    : set evs";
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   300
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   301
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   302
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   303
by (Blast_tac 1);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   304
qed "A_trusts_YM3";
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   305
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   306
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   307
(** Security Guarantee for B upon receiving YM4 **)
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   308
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   309
(*B knows, by the first part of A's message, that the Server distributed 
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   310
  the key for A and B, and has associated it with NB. *)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   311
goal thy 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   312
 "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   313
\            : parts (sees lost Spy evs);                            \
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   314
\           B ~: lost;  evs : yahalom lost |]                        \
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   315
\        ==> EX NA. Says Server A                                    \
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   316
\                    {|Nonce NB,                                     \
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   317
\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2264
diff changeset
   318
\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   319
\                       : set evs";
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   320
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   321
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   322
by (Fake_parts_insert_tac 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   323
(*YM3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   324
by (Blast_tac 1);
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   325
qed "B_trusts_YM4_shrK";
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   326
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   327
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   328
(*With this protocol variant, we don't need the 2nd part of YM4 at all:
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   329
  Nonce NB is available in the first part.*)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   330
2155
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   331
(*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
dc85854810eb New version with simpler disambiguation in YM3,
paulson
parents: 2111
diff changeset
   332
  because we do not have to show that NB is secret. *)
2111
81c8d46edfa3 New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff changeset
   333
goal thy 
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   334
 "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   335
\             : set evs;                                                 \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   336
\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   337
\        ==> EX NA. Says Server A                                        \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   338
\                    {|Nonce NB,                                         \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   339
\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   340
\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   341
\                   : set evs";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   342
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   343
by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
2323
3ae9b0ccee21 Trivial renamings
paulson
parents: 2284
diff changeset
   344
qed "B_trusts_YM4";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   345
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   346
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   347
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   348
(*** Authenticating B to A ***)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   349
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   350
(*The encryption in message YM2 tells us it cannot be faked.*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   351
goal thy 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   352
 "!!evs. evs : yahalom lost                                            \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   353
\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) -->  \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   354
\      B ~: lost -->                                                   \
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   355
\      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   356
\                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   357
\         : set evs)";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   358
by parts_induct_tac;
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   359
by (Fake_parts_insert_tac 1);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   360
(*YM2*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   361
by (Blast_tac 1);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   362
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   363
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   364
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   365
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   366
 "!!evs. evs : yahalom lost                                              \
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   367
\  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   368
\         : set evs -->                                                  \
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   369
\      B ~: lost -->                                                     \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   370
\      (EX nb'. Says B Server {|Agent B, nb',                            \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   371
\                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   372
\                 : set evs)";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   373
by (etac yahalom.induct 1);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   374
by (ALLGOALS Asm_simp_tac);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   375
(*YM3*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   376
by (blast_tac (!claset addSDs [B_Said_YM2]
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   377
		       addSEs [MPair_parts]
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   378
		       addDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   379
(*Fake, YM2*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   380
by (ALLGOALS Blast_tac);
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   381
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   382
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   383
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   384
goal thy
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   385
 "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   386
\             : set evs;                                                    \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   387
\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   388
\   ==> EX nb'. Says B Server                                               \
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   389
\                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   390
\                 : set evs";
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   391
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   392
		       addEs sees_Spy_partsEs) 1);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   393
qed "YM3_auth_B_to_A";
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   394
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   395
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   396
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   397
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   398
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   399
  It simplifies the proof by discarding needless information about
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   400
	analz (insert X (sees lost Spy evs)) 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   401
*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   402
val analz_mono_parts_induct_tac = 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   403
    etac yahalom.induct 1 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   404
    THEN 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   405
    REPEAT_FIRST  
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   406
      (rtac impI THEN' 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   407
       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   408
       mp_tac)  
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   409
    THEN  parts_sees_tac;
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   410
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   411
(*Assuming the session key is secure, if both certificates are present then
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   412
  A has said NB.  We can't be sure about the rest of A's message, but only
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   413
  NB matters for freshness.*)  
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   414
goal thy 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   415
 "!!evs. evs : yahalom lost                                             \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   416
\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   417
\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   418
\            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   419
\              : parts (sees lost Spy evs) -->                          \
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   420
\            B ~: lost -->                                              \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   421
\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   422
by analz_mono_parts_induct_tac;
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   423
(*Fake*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   424
by (Fake_parts_insert_tac 1);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   425
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   426
by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   427
(*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   428
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   429
(*yes: apply unicity of session keys*)
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   430
by (not_lost_tac "Aa" 1);
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   431
by (blast_tac (!claset addSEs [MPair_parts]
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   432
                       addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   433
		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   434
			       unique_session_keys]) 1);
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   435
val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   436
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   437
(*If B receives YM4 then A has used nonce NB (and therefore is alive).
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   438
  Moreover, A associates K with NB (thus is talking about the same run).
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   439
  Other premises guarantee secrecy of K.*)
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   440
goal thy 
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   441
 "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   442
\                       Crypt K (Nonce NB)|} : set evs;                 \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   443
\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   444
\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3450
diff changeset
   445
\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   446
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   447
by (dtac B_trusts_YM4_shrK 1);
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   448
by (safe_tac (!claset));
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   449
by (rtac lemma 1);
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   450
by (rtac Spy_not_see_encrypted_key 2);
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   451
by (REPEAT_FIRST assume_tac);
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   452
by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts]
3450
cd73bc206d87 Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
paulson
parents: 3432
diff changeset
   453
			         addDs [Says_imp_sees_Spy' RS parts.Inj])));
3432
04412cfe6861 Strengthened and streamlined the Yahalom proofs
paulson
parents: 3121
diff changeset
   454
qed_spec_mp "YM4_imp_A_Said_YM3";