src/HOL/Auth/Recur.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3483 6988394a6008
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:
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Recur
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     2
    ID:         $Id$
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     5
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     6
Inductive relation "recur" for the Recursive Authentication protocol.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     7
*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     8
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     9
open Recur;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    10
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    11
proof_timing:=true;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    12
HOL_quantifiers := false;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    13
Pretty.setdepth 30;
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    14
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    15
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    16
(** Possibility properties: traces that reach the end 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    17
        ONE theorem would be more elegant and faster!
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    18
        By induction on a list of agents (no repetitions)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    19
**)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    20
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    21
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    22
(*Simplest case: Alice goes directly to the server*)
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
    23
goal thy
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    24
 "!!A. A ~= Server                                                      \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    25
\ ==> EX K NA. EX evs: recur lost.                                      \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    26
\     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    27
\                     Agent Server|}  : set evs";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    28
by (REPEAT (resolve_tac [exI,bexI] 1));
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
    29
by (rtac (recur.Nil RS recur.RA1 RS 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    30
          (respond.One RSN (4,recur.RA3))) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    31
by possibility_tac;
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    32
result();
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    33
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    34
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    35
(*Case two: Alice, Bob and the server*)
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
    36
goal thy
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    37
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    38
\ ==> EX K. EX NA. EX evs: recur lost.                          \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    39
\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    40
\                  Agent Server|}  : set evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    41
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    42
by (REPEAT (eresolve_tac [exE, conjE] 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    43
by (REPEAT (resolve_tac [exI,bexI] 1));
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
    44
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    45
          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    46
          recur.RA4) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    47
by basic_possibility_tac;
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    48
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    49
			       less_not_refl2 RS not_sym] 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    50
result();
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    51
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    52
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    53
(*Case three: Alice, Bob, Charlie and the server
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
    54
  TOO SLOW to run every time!
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
    55
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    56
 "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    57
\ ==> EX K. EX NA. EX evs: recur lost.                                 \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
    58
\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    59
\                  Agent Server|}  : set evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    60
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    61
by (REPEAT (eresolve_tac [exE, conjE] 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    62
by (REPEAT (resolve_tac [exI,bexI] 1));
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
    63
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    64
          (respond.One RS respond.Cons RS respond.Cons RSN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    65
           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    66
(*SLOW: 70 seconds*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    67
by basic_possibility_tac;
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    68
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    69
		 ORELSE
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    70
		 eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    71
			       less_not_refl2 RS not_sym] 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    72
result();
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    73
****************)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    74
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    75
(**** Inductive proofs about recur ****)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    76
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    77
(*Monotonicity*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    78
goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    79
by (rtac subsetI 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    80
by (etac recur.induct 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    81
by (REPEAT_FIRST
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    82
    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    83
                              :: recur.intrs))));
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    84
qed "recur_mono";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    85
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    86
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
    87
goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    88
by (etac recur.induct 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    89
by (Auto_tac());
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    90
qed_spec_mp "not_Says_to_self";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    91
Addsimps [not_Says_to_self];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    92
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    93
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    94
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    95
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    96
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    97
by (etac respond.induct 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    98
by (ALLGOALS Simp_tac);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    99
qed "respond_Key_in_parts";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   100
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   101
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   102
by (etac respond.induct 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   103
by (REPEAT (assume_tac 1));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   104
qed "respond_imp_not_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   105
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   106
goal thy
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   107
 "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   108
\        ==> Key K ~: used evs";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   109
by (etac rev_mp 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   110
by (etac respond.induct 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   111
by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   112
             !simpset));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   113
qed_spec_mp "Key_in_parts_respond";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   114
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   115
(*Simple inductive reasoning about responses*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   116
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   117
by (etac respond.induct 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   118
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   119
qed "respond_imp_responses";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   120
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   121
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   122
(** For reasoning about the encrypted portion of messages **)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   123
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   124
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   125
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3451
diff changeset
   126
goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   127
\                ==> RA : analz (sees lost Spy evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   128
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   129
qed "RA4_analz_sees_Spy";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   130
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   131
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   132
  argument as for the Fake case.  This is possible for most, but not all,
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   133
  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   134
  messages originate from the Spy. *)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   135
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   136
bind_thm ("RA2_parts_sees_Spy",
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   137
          RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   138
bind_thm ("RA4_parts_sees_Spy",
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   139
          RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   140
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   141
(*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
   142
  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
   143
  interfere with simplification.*)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   144
val parts_induct_tac = 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   145
    let val tac = forw_inst_tac [("lost","lost")] 
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   146
    in  etac recur.induct      1	      THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   147
	tac RA2_parts_sees_Spy 4              THEN
2485
c4368c967c56 Simplification of some proofs, especially by eliminating
paulson
parents: 2481
diff changeset
   148
        etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   149
        forward_tac [respond_imp_responses] 5 THEN
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   150
        tac RA4_parts_sees_Spy 6	      THEN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   151
	prove_simple_subgoals_tac 1
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   152
    end;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   153
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   154
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   155
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   156
    sends messages containing X! **)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   157
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   158
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   159
(** Spy never sees another agent's long-term key (unless initially lost) **)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   160
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   161
goal thy 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   162
 "!!evs. evs : recur lost \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   163
\        ==> (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
   164
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   165
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   166
by (ALLGOALS 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   167
    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   168
(*RA3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   169
by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   170
(*RA2*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   171
by (blast_tac (!claset addSEs partsEs  addDs [parts_cut]) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   172
qed "Spy_see_shrK";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   173
Addsimps [Spy_see_shrK];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   174
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   175
goal thy 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   176
 "!!evs. evs : recur lost \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   177
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   178
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   179
qed "Spy_analz_shrK";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   180
Addsimps [Spy_analz_shrK];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   181
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   182
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   183
\                  evs : recur lost |] ==> A:lost";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   184
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   185
qed "Spy_see_shrK_D";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   186
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   187
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   188
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   189
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   190
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   191
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   192
(** Nobody can have used non-existent keys! **)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   193
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   194
goal thy
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   195
 "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   196
\        ==> K : range shrK";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   197
by (etac rev_mp 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   198
by (etac (respond_imp_responses RS responses.induct) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   199
by (Auto_tac());
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   200
qed_spec_mp "Key_in_keysFor_parts";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   201
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   202
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   203
goal thy "!!evs. evs : recur lost ==>          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   204
\       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
   205
by parts_induct_tac;
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   206
(*RA3*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   207
by (best_tac (!claset addDs  [Key_in_keysFor_parts]
3207
fe79ad367d77 renamed unsafe_addss to addss
oheimb
parents: 3121
diff changeset
   208
	      addss  (!simpset addsimps [parts_insert_sees])) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   209
(*Fake*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   210
by (best_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   211
      (!claset addIs [impOfSubs analz_subset_parts]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   212
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   213
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
3207
fe79ad367d77 renamed unsafe_addss to addss
oheimb
parents: 3121
diff changeset
   214
               addss (!simpset)) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   215
qed_spec_mp "new_keys_not_used";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   216
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   217
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   218
bind_thm ("new_keys_not_analzd",
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   219
          [analz_subset_parts RS keysFor_mono,
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   220
           new_keys_not_used] MRS contra_subsetD);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   221
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   222
Addsimps [new_keys_not_used, new_keys_not_analzd];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   223
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   224
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   225
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   226
(*** Proofs involving analz ***)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   227
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   228
(*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
   229
val analz_sees_tac = 
2485
c4368c967c56 Simplification of some proofs, especially by eliminating
paulson
parents: 2481
diff changeset
   230
    etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   231
    dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   232
    forward_tac [respond_imp_responses] 5                THEN
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   233
    dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   234
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   235
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   236
(** Session keys are not used to encrypt other session keys **)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   237
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   238
(*Version for "responses" relation.  Handles case RA3 in the theorem below.  
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   239
  Note that it holds for *any* set H (not just "sees lost Spy evs")
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   240
  satisfying the inductive hypothesis.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   241
goal thy  
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   242
 "!!evs. [| RB : responses evs;                             \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   243
\           ALL K KK. KK <= Compl (range shrK) -->          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   244
\                     (Key K : analz (Key``KK Un H)) =      \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   245
\                     (K : KK | Key K : analz H) |]         \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   246
\       ==> ALL K KK. KK <= Compl (range shrK) -->          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   247
\                     (Key K : analz (insert RB (Key``KK Un H))) = \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   248
\                     (K : KK | Key K : analz (insert RB H))";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   249
by (etac responses.induct 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   250
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   251
qed "resp_analz_image_freshK_lemma";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   252
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   253
(*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   254
goal thy  
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   255
 "!!evs. evs : recur lost ==>                                   \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   256
\  ALL K KK. KK <= Compl (range shrK) -->                       \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   257
\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   258
\            (K : KK | Key K : analz (sees lost Spy evs))";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   259
by (etac recur.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   260
by analz_sees_tac;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   261
by (REPEAT_FIRST (resolve_tac [allI, impI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   262
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   263
by (ALLGOALS 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   264
    (asm_simp_tac
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   265
     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   266
(*Base*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   267
by (Blast_tac 1);
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   268
(*Fake*) 
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3207
diff changeset
   269
by (spy_analz_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   270
val raw_analz_image_freshK = result();
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   271
qed_spec_mp "analz_image_freshK";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   272
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   273
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   274
(*Instance of the lemma with H replaced by (sees lost Spy evs):
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   275
   [| RB : responses evs;  evs : recur lost; |]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   276
   ==> KK <= Compl (range shrK) --> 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   277
       Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   278
       (K : KK | Key K : analz (insert RB (sees lost Spy evs))) 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   279
*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   280
bind_thm ("resp_analz_image_freshK",
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   281
          raw_analz_image_freshK RSN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   282
            (2, resp_analz_image_freshK_lemma) RS spec RS spec);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   283
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   284
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   285
 "!!evs. [| evs : recur lost;  KAB ~: range shrK |] ==>              \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   286
\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =      \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   287
\        (K = KAB | Key K : analz (sees lost Spy evs))";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   288
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: 2485
diff changeset
   289
qed "analz_insert_freshK";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   290
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   291
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   292
(*Everything that's hashed is already in past traffic. *)
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   293
goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees lost Spy evs);  \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   294
\                   evs : recur lost;  A ~: lost |]                       \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   295
\                ==> X : parts (sees lost Spy evs)";
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   296
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   297
by parts_induct_tac;
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   298
(*RA3 requires a further induction*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   299
by (etac responses.induct 2);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   300
by (ALLGOALS Asm_simp_tac);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   301
(*Fake*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   302
by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   303
by (Fake_parts_insert_tac 1);
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   304
qed "Hash_imp_body";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   305
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   306
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   307
(** The Nonce NA uniquely identifies A's message. 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   308
    This theorem applies to steps RA1 and RA2!
2455
9c4444bfd44e Simplification and generalization of the guarantees.
paulson
parents: 2451
diff changeset
   309
9c4444bfd44e Simplification and generalization of the guarantees.
paulson
parents: 2451
diff changeset
   310
  Unicity is not used in other proofs but is desirable in its own right.
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   311
**)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   312
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   313
goal thy 
2560
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   314
 "!!evs. [| evs : recur lost; A ~: lost |]                   \
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   315
\ ==> EX B' P'. ALL B P.                                     \
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   316
\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   317
\          -->  B=B' & P=P'";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   318
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   319
by (Fake_parts_insert_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   320
by (etac responses.induct 3);
2485
c4368c967c56 Simplification of some proofs, especially by eliminating
paulson
parents: 2481
diff changeset
   321
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   322
by (step_tac (!claset addSEs partsEs) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   323
(*RA1,2: creation of new Nonce.  Move assertion into global context*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   324
by (ALLGOALS (expand_case_tac "NA = ?y"));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   325
by (REPEAT_FIRST (ares_tac [exI]));
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   326
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   327
                               addSEs sees_Spy_partsEs) 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   328
val lemma = result();
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   329
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   330
goalw thy [HPair_def]
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   331
 "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(sees lost Spy evs); \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   332
\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees lost Spy evs); \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   333
\        evs : recur lost;  A ~: lost |]                                     \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   334
\      ==> B=B' & P=P'";
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   335
by (REPEAT (eresolve_tac partsEs 1));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   336
by (prove_unique_tac lemma 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   337
qed "unique_NA";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   338
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   339
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   340
(*** Lemmas concerning the Server's response
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   341
      (relations "respond" and "responses") 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   342
***)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   343
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   344
goal thy
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   345
 "!!evs. [| RB : responses evs;  evs : recur lost |] \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   346
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   347
by (etac responses.induct 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   348
by (ALLGOALS
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   349
    (asm_simp_tac 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   350
     (analz_image_freshK_ss addsimps [Spy_analz_shrK,
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   351
                                      resp_analz_image_freshK])));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   352
qed "shrK_in_analz_respond";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   353
Addsimps [shrK_in_analz_respond];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   354
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   355
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   356
goal thy  
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   357
 "!!evs. [| RB : responses evs;                             \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   358
\           ALL K KK. KK <= Compl (range shrK) -->          \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   359
\                     (Key K : analz (Key``KK Un H)) =      \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   360
\                     (K : KK | Key K : analz H) |]         \
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   361
\       ==> (Key K : analz (insert RB H)) -->               \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   362
\           (Key K : parts{RB} | Key K : analz H)";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   363
by (etac responses.induct 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   364
by (ALLGOALS
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   365
    (asm_simp_tac 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   366
     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   367
(*Simplification using two distinct treatments of "image"*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   368
by (simp_tac (!simpset addsimps [parts_insert2]) 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   369
by (blast_tac (!claset delrules [allE]) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   370
qed "resp_analz_insert_lemma";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   371
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   372
bind_thm ("resp_analz_insert",
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   373
          raw_analz_image_freshK RSN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   374
            (2, resp_analz_insert_lemma) RSN(2, rev_mp));
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   375
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   376
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   377
(*The Server does not send such messages.  This theorem lets us avoid
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   378
  assuming B~=Server in RA4.*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   379
goal thy 
3483
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   380
 "!!evs. evs : recur lost \
6988394a6008 Tidying; also simplified the lemma Says_Server_not
paulson
parents: 3466
diff changeset
   381
\        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   382
by (etac recur.induct 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   383
by (etac (respond.induct) 5);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   384
by (Auto_tac());
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   385
qed_spec_mp "Says_Server_not";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   386
AddSEs [Says_Server_not RSN (2,rev_notE)];
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   387
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   388
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   389
(*The last key returned by respond indeed appears in a certificate*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   390
goal thy 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   391
 "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   392
\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   393
by (etac respond.elim 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   394
by (ALLGOALS Asm_full_simp_tac);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   395
qed "respond_certificate";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   396
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   397
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   398
goal thy 
2560
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   399
 "!!K'. (PB,RB,KXY) : respond evs                          \
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   400
\  ==> EX A' B'. ALL A B N.                                \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   401
\        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   402
\          -->   (A'=A & B'=B) | (A'=B & B'=A)";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   403
by (etac respond.induct 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   404
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   405
(*Base case*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   406
by (Blast_tac 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   407
by (Step_tac 1);
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   408
by (expand_case_tac "K = KBC" 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   409
by (dtac respond_Key_in_parts 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   410
by (blast_tac (!claset addSIs [exI]
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   411
                      addSEs partsEs
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   412
                      addDs [Key_in_parts_respond]) 1);
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   413
by (expand_case_tac "K = KAB" 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   414
by (REPEAT (ares_tac [exI] 2));
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   415
by (ex_strip_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   416
by (dtac respond_certificate 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   417
by (Fast_tac 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   418
val lemma = result();
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   419
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   420
goal thy 
2560
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   421
 "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   422
\          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
2560
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   423
\          (PB,RB,KXY) : respond evs |]                            \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   424
\ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
2560
c57b585eecd9 Tidied unicity theorems
paulson
parents: 2550
diff changeset
   425
by (prove_unique_tac lemma 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   426
qed "unique_session_keys";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   427
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   428
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   429
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   430
    Does not in itself guarantee security: an attack could violate 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   431
    the premises, e.g. by having A=Spy **)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   432
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   433
goal thy 
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   434
 "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur lost |]         \
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   435
\        ==> ALL A A' N. A ~: lost & A' ~: lost -->                 \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   436
\            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   437
\            Key K ~: analz (insert RB (sees lost Spy evs))";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   438
by (etac respond.induct 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   439
by (forward_tac [respond_imp_responses] 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   440
by (forward_tac [respond_imp_not_used] 2);
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   441
by (ALLGOALS (*23 seconds*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   442
    (asm_simp_tac 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   443
     (analz_image_freshK_ss addsimps 
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   444
       [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   445
by (ALLGOALS Simp_tac);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   446
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   447
by (step_tac (!claset addSEs [MPair_parts]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   448
(** LEVEL 7 **)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   449
by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   450
                      addDs  [impOfSubs analz_subset_parts]) 4);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   451
by (blast_tac (!claset addSDs [respond_certificate]) 3);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   452
by (blast_tac (!claset addSEs partsEs
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   453
                       addDs [Key_in_parts_respond]) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   454
by (dtac unique_session_keys 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   455
by (etac respond_certificate 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   456
by (assume_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   457
by (Blast_tac 1);
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   458
qed_spec_mp "respond_Spy_not_see_session_key";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   459
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   460
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   461
goal thy
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   462
 "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}          \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   463
\              : parts (sees lost Spy evs);                \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   464
\           A ~: lost;  A' ~: lost;  evs : recur lost |]   \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   465
\        ==> Key K ~: analz (sees lost Spy evs)";
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   466
by (etac rev_mp 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   467
by (etac recur.induct 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   468
by analz_sees_tac;
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   469
by (ALLGOALS
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   470
    (asm_simp_tac
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   471
     (!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   472
               setloop split_tac [expand_if])));
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   473
(*RA4*)
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   474
by (spy_analz_tac 5);
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   475
(*RA2*)
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   476
by (spy_analz_tac 3);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   477
(*Fake*)
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   478
by (spy_analz_tac 2);
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   479
(*Base*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   480
by (Blast_tac 1);
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   481
(*RA3 remains*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   482
by (step_tac (!claset delrules [impCE]) 1);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   483
(*RA3, case 2: K is an old key*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   484
by (blast_tac (!claset addSDs [resp_analz_insert]
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   485
                       addSEs partsEs
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   486
                       addDs [Key_in_parts_respond]) 2);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   487
(*RA3, case 1: use lemma previously proved by induction*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   488
by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   489
			       (2,rev_notE)]) 1);
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   490
qed "Spy_not_see_session_key";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   491
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   492
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   493
goal thy 
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   494
 "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}         \
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   495
\              : parts(sees lost Spy evs);                \
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   496
\           C ~: {A,A',Server};                           \
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   497
\           A ~: lost;  A' ~: lost;  evs : recur lost |]  \
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   498
\        ==> Key K ~: analz (sees lost C evs)";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   499
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   500
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   501
by (FIRSTGOAL (rtac Spy_not_see_session_key));
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   502
by (REPEAT_FIRST
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   503
    (blast_tac
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   504
     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   505
qed "Agent_not_see_session_key";
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   506
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   507
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   508
(**** Authenticity properties for Agents ****)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   509
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   510
(*The response never contains Hashes*)
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   511
goal thy
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   512
 "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   513
\           (PB,RB,K) : respond evs |]                      \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   514
\        ==> Hash {|Key (shrK B), M|} : parts H";
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   515
by (etac rev_mp 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   516
by (etac (respond_imp_responses RS responses.induct) 1);
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   517
by (Auto_tac());
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   518
qed "Hash_in_parts_respond";
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   519
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   520
(*Only RA1 or RA2 can have caused such a part of a message to appear.
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   521
  This result is of no use to B, who cannot verify the Hash.  Moreover,
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   522
  it can say nothing about how recent A's message is.  It might later be
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   523
  used to prove B's presence to A at the run's conclusion.*)
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2455
diff changeset
   524
goalw thy [HPair_def]
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   525
 "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   526
\             : parts (sees lost Spy evs);                        \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   527
\            A ~: lost;  evs : recur lost |]                      \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   528
\     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   529
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   530
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   531
by (Fake_parts_insert_tac 1);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   532
(*RA3*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   533
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   534
qed_spec_mp "Hash_auth_sender";
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   535
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
   536
(** These two results subsume (for all agents) the guarantees proved
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   537
    separately for A and B in the Otway-Rees protocol.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   538
**)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   539
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   540
2533
2d5604a51562 Simplified proofs
paulson
parents: 2516
diff changeset
   541
(*Certificates can only originate with the Server.*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   542
goal thy 
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   543
 "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   544
\           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   545
\        ==> EX C RC. Says Server C RC : set evs  &          \
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   546
\                     Crypt (shrK A) Y : parts {RC}";
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   547
by (etac rev_mp 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   548
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   549
by (Fake_parts_insert_tac 1);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   550
(*RA4*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   551
by (Blast_tac 4);
2455
9c4444bfd44e Simplification and generalization of the guarantees.
paulson
parents: 2451
diff changeset
   552
(*RA3*)
9c4444bfd44e Simplification and generalization of the guarantees.
paulson
parents: 2451
diff changeset
   553
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   554
    THEN Blast_tac 3);
2455
9c4444bfd44e Simplification and generalization of the guarantees.
paulson
parents: 2451
diff changeset
   555
(*RA1*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   556
by (Blast_tac 1);
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2449
diff changeset
   557
(*RA2: it cannot be a new Nonce, contradiction.*)
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   558
by (Blast_tac 1);
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2533
diff changeset
   559
qed "Cert_imp_Server_msg";