src/HOL/Auth/KerberosIV.ML
author paulson
Wed, 14 Mar 2001 08:50:55 +0100
changeset 11204 bb01189f0565
parent 11185 1b737b4c2108
child 11222 72c5997e1145
permissions -rw-r--r--
minor tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/KerberosIV
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     2
    ID:         $Id$
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     3
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     5
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     6
The Kerberos protocol, version IV.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     7
*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     8
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
     9
Pretty.setdepth 20;
9000
c20d58286a51 cleaned up;
wenzelm
parents: 8954
diff changeset
    10
set timing;
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    11
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    12
AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    13
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    14
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    15
(** Reversed traces **)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    16
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    17
Goal "spies (evs @ [Says A B X]) = insert X (spies evs)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    18
by (induct_tac "evs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    19
by (induct_tac "a" 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    20
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    21
qed "spies_Says_rev";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    22
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    23
Goal "spies (evs @ [Gets A X]) = spies evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    24
by (induct_tac "evs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    25
by (induct_tac "a" 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    26
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    27
qed "spies_Gets_rev";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    28
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    29
Goal "spies (evs @ [Notes A X]) = \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    30
\         (if A:bad then insert X (spies evs) else spies evs)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    31
by (induct_tac "evs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    32
by (induct_tac "a" 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    33
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    34
qed "spies_Notes_rev";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    35
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    36
Goal "spies evs = spies (rev evs)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    37
by (induct_tac "evs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    38
by (induct_tac "a" 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    39
by (ALLGOALS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    40
    (asm_simp_tac (simpset() addsimps [spies_Says_rev, spies_Gets_rev, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    41
				       spies_Notes_rev])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    42
qed "spies_evs_rev";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    43
bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    44
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    45
Goal "spies (takeWhile P evs)  <=  spies evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    46
by (induct_tac "evs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    47
by (induct_tac "a" 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    48
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    49
(* Resembles "used_subset_append" in Event.ML*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    50
qed "spies_takeWhile";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    51
bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    52
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    53
Goal "~P(x) --> takeWhile P (xs @ [x]) = takeWhile P xs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    54
by (induct_tac "xs" 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    55
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    56
qed "takeWhile_tail";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    57
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    58
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    59
(*****************LEMMAS ABOUT AuthKeys****************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    60
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    61
Goalw [AuthKeys_def] "AuthKeys [] = {}";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    62
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    63
qed "AuthKeys_empty";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    64
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    65
Goalw [AuthKeys_def] 
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    66
 "(\\<forall>A Tk akey Peer.              \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    67
\  ev \\<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,      \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    68
\             (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))\ 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    69
\      ==> AuthKeys (ev # evs) = AuthKeys evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    70
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    71
qed "AuthKeys_not_insert";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    72
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    73
Goalw [AuthKeys_def] 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    74
  "AuthKeys \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    75
\    (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    76
\     (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs) \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    77
\      = insert K (AuthKeys evs)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    78
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    79
qed "AuthKeys_insert";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    80
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    81
Goalw [AuthKeys_def] 
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    82
   "K \\<in> AuthKeys \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    83
\   (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    84
\    (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    85
\       ==> K = K' | K \\<in> AuthKeys evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    86
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    87
qed "AuthKeys_simp";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    88
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    89
Goalw [AuthKeys_def]  
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    90
   "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk, \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    91
\    (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \\<in> set evs \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    92
\       ==> K \\<in> AuthKeys evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    93
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    94
qed "AuthKeysI";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    95
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
    96
Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    97
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    98
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
    99
qed "AuthKeys_used";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   100
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   101
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   102
(**** FORWARDING LEMMAS ****)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   103
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   104
(*--For reasoning about the encrypted portion of message K3--*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   105
Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   106
\              \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   107
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   108
qed "K3_msg_in_parts_spies";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   109
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   110
Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   111
\              \\<in> set evs ==> AuthKey \\<in> parts (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   112
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   113
qed "Oops_parts_spies1";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   114
                              
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   115
Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   116
\          \\<in> set evs ;\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   117
\        evs \\<in> kerberos |] ==> AuthKey \\<notin> range shrK";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   118
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   119
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   120
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   121
qed "Oops_range_spies1";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   122
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   123
(*--For reasoning about the encrypted portion of message K5--*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   124
Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   125
 \             \\<in> set evs ==> ServTicket \\<in> parts (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   126
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   127
qed "K5_msg_in_parts_spies";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   128
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   129
Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   130
\                  \\<in> set evs ==> ServKey \\<in> parts (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   131
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   132
qed "Oops_parts_spies2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   133
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   134
Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   135
\          \\<in> set evs ;\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   136
\        evs \\<in> kerberos |] ==> ServKey \\<notin> range shrK";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   137
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   138
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   139
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   140
qed "Oops_range_spies2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   141
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   142
Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \\<in> set evs \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   143
\     ==> Ticket \\<in> parts (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   144
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   145
qed "Says_ticket_in_parts_spies";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   146
(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   147
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   148
fun parts_induct_tac i = 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   149
    etac kerberos.induct i  THEN 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   150
    REPEAT (FIRSTGOAL analz_mono_contra_tac)  THEN
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   151
    ftac K3_msg_in_parts_spies (i+4)  THEN
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   152
    ftac K5_msg_in_parts_spies (i+6)  THEN
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   153
    ftac Oops_parts_spies1 (i+8)  THEN
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   154
    ftac Oops_parts_spies2 (i+9) THEN
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   155
    prove_simple_subgoals_tac 1;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   156
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   157
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   158
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   159
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   160
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   161
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   162
by (ALLGOALS Blast_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   163
qed "Spy_see_shrK";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   164
Addsimps [Spy_see_shrK];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   165
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   166
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   167
by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset()));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   168
qed "Spy_analz_shrK";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   169
Addsimps [Spy_analz_shrK];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   170
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   171
Goal "[| Key (shrK A) \\<in> parts (spies evs);  evs \\<in> kerberos |] ==> A:bad";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   172
by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   173
qed "Spy_see_shrK_D";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   174
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   175
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   176
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   177
(*Nobody can have used non-existent keys!*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   178
Goal "evs \\<in> kerberos ==>      \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   179
\     Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   180
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   181
(*Fake*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   182
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   183
(*Others*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   184
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   185
qed_spec_mp "new_keys_not_used";
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   186
Addsimps [new_keys_not_used];
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   187
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   188
(*Earlier, all protocol proofs declared this theorem.  
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   189
  But few of them actually need it! (Another is Yahalom) *)
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   190
bind_thm ("new_keys_not_analzd",
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   191
          [analz_subset_parts RS keysFor_mono,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   192
           new_keys_not_used] MRS contra_subsetD);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   193
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   194
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   195
(*********************** REGULARITY LEMMAS ***********************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   196
(*       concerning the form of items passed in messages         *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   197
(*****************************************************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   198
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   199
(*Describes the form of AuthKey, AuthTicket, and K sent by Kas*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   200
Goal "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   201
\          \\<in> set evs;                 \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   202
\        evs \\<in> kerberos |]             \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   203
\     ==> AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs & \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   204
\ AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|} ) &\
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   205
\            K = shrK A  & Peer = Tgs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   206
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   207
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   208
by (ALLGOALS (simp_tac (simpset() addsimps [AuthKeys_def, AuthKeys_insert])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   209
by (ALLGOALS Blast_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   210
qed "Says_Kas_message_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   211
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   212
(*This lemma is essential for proving Says_Tgs_message_form: 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   213
  
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   214
  the session key AuthKey
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   215
  supplied by Kas in the authentication ticket
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   216
  cannot be a long-term key!
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   217
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   218
  Generalised to any session keys (both AuthKey and ServKey).
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   219
*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   220
Goal "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   221
\           \\<in> parts (spies evs); Tgs_B \\<notin> bad;\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   222
\        evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   223
\     ==> SesKey \\<notin> range shrK";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   224
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   225
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   226
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   227
qed "SesKey_is_session_key";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   228
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   229
Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   230
\          \\<in> parts (spies evs);                              \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   231
\        evs \\<in> kerberos |]                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   232
\     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   233
\                Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   234
\           \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   235
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   236
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   237
(*Fake*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   238
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   239
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   240
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   241
qed "A_trusts_AuthTicket";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   242
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   243
Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   244
\          \\<in> parts (spies evs);\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   245
\        evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   246
\     ==> AuthKey \\<in> AuthKeys evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   247
by (ftac A_trusts_AuthTicket 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   248
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   249
by (simp_tac (simpset() addsimps [AuthKeys_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   250
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   251
qed "AuthTicket_crypt_AuthKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   252
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   253
(*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   254
Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   255
\          \\<in> set evs; \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   256
\        evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   257
\  ==> B \\<noteq> Tgs & ServKey \\<notin> range shrK & ServKey \\<notin> AuthKeys evs &\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   258
\      ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|} ) & \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   259
\      AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   260
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   261
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   262
by (ALLGOALS
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   263
    (asm_full_simp_tac
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   264
     (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   265
			  AuthKeys_empty, AuthKeys_simp])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   266
by (blast_tac (claset() addEs  spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   267
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   268
by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   269
by (blast_tac (claset() addSDs [SesKey_is_session_key]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   270
                        addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   271
by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey] 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   272
                        addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   273
qed "Says_Tgs_message_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   274
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   275
(*If a certain encrypted message appears then it originated with Kas*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   276
Goal "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   277
\          \\<in> parts (spies evs);                              \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   278
\        A \\<notin> bad;  evs \\<in> kerberos |]                        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   279
\     ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   280
\           \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   281
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   282
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   283
(*Fake*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   284
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   285
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   286
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   287
			       A_trusts_AuthTicket RS Says_Kas_message_form])
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   288
    1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   289
qed "A_trusts_AuthKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   290
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   291
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   292
(*If a certain encrypted message appears then it originated with Tgs*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   293
Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   294
\          \\<in> parts (spies evs);                                     \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   295
\        Key AuthKey \\<notin> analz (spies evs);           \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   296
\        AuthKey \\<notin> range shrK;                      \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   297
\        evs \\<in> kerberos |]         \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   298
\==> \\<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   299
\      \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   300
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   301
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   302
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   303
(*Fake*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   304
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   305
(*K2*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   306
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   307
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   308
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   309
qed "A_trusts_K4";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   310
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   311
Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   312
\          \\<in> parts (spies evs);          \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   313
\        A \\<notin> bad;                       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   314
\        evs \\<in> kerberos |]                \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   315
\   ==> AuthKey \\<notin> range shrK &               \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   316
\       AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   317
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   318
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   319
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   320
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   321
qed "AuthTicket_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   322
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   323
(* This form holds also over an AuthTicket, but is not needed below.     *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   324
Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   325
\             \\<in> parts (spies evs); \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   326
\           Key AuthKey \\<notin> analz (spies evs);  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   327
\           evs \\<in> kerberos |]                                       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   328
\        ==> ServKey \\<notin> range shrK &  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   329
\   (\\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   330
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   331
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   332
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   333
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   334
qed "ServTicket_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   335
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   336
Goal "[| Says Kas' A (Crypt (shrK A) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   337
\             {|Key AuthKey, Agent Tgs, Tk, AuthTicket|} ) \\<in> set evs; \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   338
\        evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   339
\     ==> AuthKey \\<notin> range shrK & \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   340
\         AuthTicket = \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   341
\                 Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   342
\         | AuthTicket \\<in> analz (spies evs)";
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   343
by (case_tac "A \\<in> bad" 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   344
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   345
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   346
by (blast_tac (claset() addSDs [AuthTicket_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   347
qed "Says_kas_message_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   348
(* Essentially the same as AuthTicket_form *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   349
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   350
Goal "[| Says Tgs' A (Crypt AuthKey \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   351
\             {|Key ServKey, Agent B, Tt, ServTicket|} ) \\<in> set evs; \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   352
\        evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   353
\     ==> ServKey \\<notin> range shrK & \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   354
\         (\\<exists>A. ServTicket = \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   355
\                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   356
\          | ServTicket \\<in> analz (spies evs)";
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   357
by (case_tac "Key AuthKey \\<in> analz (spies evs)" 1);
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   358
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   359
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   360
by (blast_tac (claset() addSDs [ServTicket_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   361
qed "Says_tgs_message_form";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   362
(* This form MUST be used in analz_sees_tac below *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   363
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   364
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   365
(*****************UNICITY THEOREMS****************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   366
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   367
(* The session key, if secure, uniquely identifies the Ticket
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   368
   whether AuthTicket or ServTicket. As a matter of fact, one can read
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   369
   also Tgs in the place of B.                                     *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   370
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   371
Goal "[| Crypt (shrK B)  {|Agent A,  Agent B,  Key SesKey, T|}        \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   372
\          \\<in> parts (spies evs);            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   373
\        Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   374
\          \\<in> parts (spies evs);  Key SesKey \\<notin> analz (spies evs);   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   375
\        evs \\<in> kerberos |]  \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   376
\     ==> A=A' & B=B' & T=T'";
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   377
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   378
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   379
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   380
by (parts_induct_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   381
(*Fake, K2, K4*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   382
by (Fake_parts_insert_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   383
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   384
qed "unique_CryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   385
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   386
(*An AuthKey is encrypted by one and only one Shared key.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   387
  A ServKey is encrypted by one and only one AuthKey.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   388
*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   389
Goal "[| Crypt K  {|Key SesKey,  Agent B, T, Ticket|}        \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   390
\          \\<in> parts (spies evs);            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   391
\        Crypt K' {|Key SesKey,  Agent B', T', Ticket'|}     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   392
\          \\<in> parts (spies evs);  Key SesKey \\<notin> analz (spies evs);            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   393
\        evs \\<in> kerberos |]  \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   394
\     ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   395
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   396
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   397
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   398
by (parts_induct_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   399
(*Fake, K2, K4*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   400
by (Fake_parts_insert_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   401
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   402
qed "Key_unique_SesKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   403
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   404
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   405
(*
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   406
  At reception of any message mentioning A, Kas associates shrK A with
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   407
  a new AuthKey. Realistic, as the user gets a new AuthKey at each login.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   408
  Similarly, at reception of any message mentioning an AuthKey
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   409
  (a legitimate user could make several requests to Tgs - by K3), Tgs 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   410
  associates it with a new ServKey.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   411
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   412
  Therefore, a goal like
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   413
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   414
   "evs \\<in> kerberos \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   415
  \  ==> Key Kc \\<notin> analz (spies evs) -->   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   416
  \        (\\<exists>K' B' T' Ticket'. \\<forall>K B T Ticket.                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   417
  \         Crypt Kc {|Key K, Agent B, T, Ticket|}    \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   418
  \          \\<in> parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   419
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   420
  would fail on the K2 and K4 cases.
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   421
*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   422
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   423
Goal "[| Says Kas A                                          \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   424
\             (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \\<in> set evs;     \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   425
\        Says Kas A'                                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   426
\             (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \\<in> set evs;   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   427
\        evs \\<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   428
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   429
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   430
by (parts_induct_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   431
(*K2*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   432
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   433
qed "unique_AuthKeys";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   434
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   435
(* ServKey uniquely identifies the message from Tgs *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   436
Goal "[| Says Tgs A                                             \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   437
\             (Crypt K {|Key ServKey, Agent B, Tt, X|}) \\<in> set evs; \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   438
\        Says Tgs A'                                                 \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   439
\             (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \\<in> set evs; \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   440
\        evs \\<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   441
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   442
by (etac rev_mp 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   443
by (parts_induct_tac 1);
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   444
(*K4*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   445
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   446
qed "unique_ServKeys";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   447
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   448
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   449
(*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   450
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   451
Goalw [KeyCryptKey_def] "~ KeyCryptKey AuthKey ServKey []";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   452
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   453
qed "not_KeyCryptKey_Nil";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   454
AddIffs [not_KeyCryptKey_Nil];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   455
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   456
Goalw [KeyCryptKey_def]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   457
 "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   458
\             \\<in> set evs;    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   459
\           evs \\<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   460
by (ftac Says_Tgs_message_form 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   461
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   462
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   463
qed "KeyCryptKeyI";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   464
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   465
Goalw [KeyCryptKey_def]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   466
   "KeyCryptKey AuthKey ServKey (Says S A X # evs) =                       \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   467
\    (Tgs = S &                                                            \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   468
\     (\\<exists>B tt. X = Crypt AuthKey        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   469
\               {|Key ServKey, Agent B, tt,  \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   470
\                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |}) \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   471
\    | KeyCryptKey AuthKey ServKey evs)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   472
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   473
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   474
qed "KeyCryptKey_Says";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   475
Addsimps [KeyCryptKey_Says];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   476
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   477
(*A fresh AuthKey cannot be associated with any other
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   478
  (with respect to a given trace). *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   479
Goalw [KeyCryptKey_def]
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   480
 "[| Key AuthKey \\<notin> used evs; evs \\<in> kerberos |] \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   481
\        ==> ~ KeyCryptKey AuthKey ServKey evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   482
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   483
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   484
by (Asm_full_simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   485
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   486
qed "Auth_fresh_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   487
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   488
(*A fresh ServKey cannot be associated with any other
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   489
  (with respect to a given trace). *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   490
Goalw [KeyCryptKey_def]
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   491
 "Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   492
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   493
qed "Serv_fresh_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   494
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   495
Goal
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   496
 "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   497
\             \\<in> parts (spies evs);  evs \\<in> kerberos |] \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   498
\        ==> ~ KeyCryptKey K AuthKey evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   499
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   500
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   501
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   502
by (blast_tac (claset() addEs spies_partsEs) 3);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   503
(*K2: by freshness*)
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   504
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   505
by (blast_tac (claset() addEs spies_partsEs) 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   506
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   507
qed "AuthKey_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   508
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   509
(*A secure serverkey cannot have been used to encrypt others*)
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   510
Goal
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   511
 "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   512
\    Key SK \\<notin> analz (spies evs);             \
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   513
\    B \\<noteq> Tgs;  evs \\<in> kerberos |] \
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   514
\ ==> ~ KeyCryptKey SK K evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   515
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   516
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   517
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   518
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   519
(*K4 splits into distinct subcases*)
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   520
by Auto_tac;  
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   521
(*ServKey can't have been enclosed in two certificates*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   522
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   523
                       addSEs [MPair_parts]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   524
                       addDs  [unique_CryptKey]) 4);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   525
(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   526
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   527
				Crypt_imp_invKey_keysFor],
11204
bb01189f0565 minor tuning
paulson
parents: 11185
diff changeset
   528
	       simpset() addsimps [KeyCryptKey_def]) 2); 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   529
(*Others by freshness*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   530
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   531
qed "ServKey_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   532
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   533
(*Long term keys are not issued as ServKeys*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   534
Goalw [KeyCryptKey_def]
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   535
 "evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   536
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   537
qed "shrK_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   538
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   539
(*The Tgs message associates ServKey with AuthKey and therefore not with any 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   540
  other key AuthKey.*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   541
Goalw [KeyCryptKey_def]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   542
 "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   543
\      \\<in> set evs;                                         \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   544
\    AuthKey' \\<noteq> AuthKey;  evs \\<in> kerberos |]                      \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   545
\ ==> ~ KeyCryptKey AuthKey' ServKey evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   546
by (blast_tac (claset() addDs [unique_ServKeys]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   547
qed "Says_Tgs_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   548
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   549
Goal "[| KeyCryptKey AuthKey ServKey evs;  evs \\<in> kerberos |] \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   550
\     ==> ~ KeyCryptKey ServKey K evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   551
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   552
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   553
by (Step_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   554
by (ALLGOALS Asm_full_simp_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   555
(*K4 splits into subcases*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   556
by (blast_tac (claset() addEs spies_partsEs 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   557
                       addSDs [AuthKey_not_KeyCryptKey]) 4);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   558
(*ServKey is fresh and so could not have been used, by new_keys_not_used*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   559
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   560
				Crypt_imp_invKey_keysFor],
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   561
                      simpset() addsimps [KeyCryptKey_def]) 2); 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   562
(*Others by freshness*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   563
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   564
qed "KeyCryptKey_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   565
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   566
(*The only session keys that can be found with the help of session keys are
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   567
  those sent by Tgs in step K4.  *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   568
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   569
(*We take some pains to express the property
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   570
  as a logical equivalence so that the simplifier can apply it.*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   571
Goal "P --> (Key K \\<in> analz (Key`KK Un H)) --> (K:KK | Key K \\<in> analz H)  \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   572
\     ==>       \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   573
\     P --> (Key K \\<in> analz (Key`KK Un H)) = (K:KK | Key K \\<in> analz H)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   574
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   575
qed "Key_analz_image_Key_lemma";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   576
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   577
Goal "[| KeyCryptKey K K' evs; evs \\<in> kerberos |] \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   578
\     ==> Key K' \\<in> analz (insert (Key K) (spies evs))";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   579
by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   580
by (Clarify_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   581
by (dresolve_tac [Says_imp_spies RS analz.Inj RS analz_insertI] 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   582
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   583
qed "KeyCryptKey_analz_insert";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   584
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   585
Goal "[| K \\<in> AuthKeys evs Un range shrK;  evs \\<in> kerberos |]  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   586
\     ==> \\<forall>SK. ~ KeyCryptKey SK K evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   587
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   588
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   589
qed "AuthKeys_are_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   590
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   591
Goal "[| K \\<notin> AuthKeys evs; \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   592
\        K \\<notin> range shrK; evs \\<in> kerberos |]  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   593
\     ==> \\<forall>SK. ~ KeyCryptKey K SK evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   594
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   595
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   596
qed "not_AuthKeys_not_KeyCryptKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   597
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   598
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   599
(*****************SECRECY THEOREMS****************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   600
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   601
(*For proofs involving analz.*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   602
val analz_sees_tac = 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   603
  EVERY 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   604
   [REPEAT (FIRSTGOAL analz_mono_contra_tac),
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   605
    ftac Oops_range_spies2 10, 
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   606
    ftac Oops_range_spies1 9, 
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   607
    ftac Says_tgs_message_form 7,
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   608
    ftac Says_kas_message_form 5, 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   609
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   610
		  ORELSE' hyp_subst_tac)];
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   611
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   612
(*For the Oops2 case of the next theorem*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   613
Goal "[| evs \\<in> kerberos;  \
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   614
\        Says Tgs A (Crypt AuthKey \
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   615
\                    {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   616
\          \\<in> set evs |] \
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   617
\     ==> ~ KeyCryptKey ServKey SK evs";
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   618
by (blast_tac (claset() addDs [KeyCryptKeyI, KeyCryptKey_not_KeyCryptKey]) 1);
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   619
qed "Oops2_not_KeyCryptKey";
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   620
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   621
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   622
(* Big simplification law for keys SK that are not crypted by keys in KK   *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   623
(* It helps prove three, otherwise hard, facts about keys. These facts are *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   624
(* exploited as simplification laws for analz, and also "limit the damage" *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   625
(* in case of loss of a key to the spy. See ESORICS98.                     *)
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   626
(* [simplified by LCP]                                                     *)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   627
Goal "evs \\<in> kerberos ==>                                         \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   628
\     (\\<forall>SK KK. KK <= -(range shrK) -->                   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   629
\     (\\<forall>K \\<in> KK. ~ KeyCryptKey K SK evs)   -->           \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   630
\     (Key SK \\<in> analz (Key`KK Un (spies evs))) =        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   631
\     (SK \\<in> KK | Key SK \\<in> analz (spies evs)))";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   632
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   633
by analz_sees_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   634
by (REPEAT_FIRST (rtac allI));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   635
by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   636
(*Case-splits for Oops1 & 5: the negated case simplifies using the ind hyp*)
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   637
by (case_tac "KeyCryptKey AuthKey SK evsO1" 11); 
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   638
by (case_tac "KeyCryptKey ServKey SK evs5" 8);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   639
by (ALLGOALS  
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   640
    (asm_simp_tac 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   641
     (analz_image_freshK_ss addsimps
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   642
        [KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey,
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   643
	 Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   644
	 Says_Tgs_KeyCryptKey, Spy_analz_shrK])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   645
(*Fake*) 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   646
by (spy_analz_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   647
(* Base + K2 done by the simplifier! *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   648
(*K3*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   649
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   650
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   651
by (blast_tac (claset() addEs spies_partsEs 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   652
                        addSDs [AuthKey_not_KeyCryptKey]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   653
(*K5*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   654
by (case_tac "Key ServKey \\<in> analz (spies evs5)" 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   655
(*If ServKey is compromised then the result follows directly...*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   656
by (asm_simp_tac 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   657
     (simpset() addsimps [analz_insert_eq, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   658
			 impOfSubs (Un_upper2 RS analz_mono)]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   659
(*...therefore ServKey is uncompromised.*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   660
(*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   661
by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   662
		        addEs spies_partsEs delrules [allE, ballE]) 1);
8954
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   663
(** Level 13: Oops1 **)
4fbdda40bb5f rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents: 8741
diff changeset
   664
by (Asm_full_simp_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   665
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   666
qed_spec_mp "Key_analz_image_Key";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   667
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   668
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   669
(* First simplification law for analz: no session keys encrypt  *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   670
(* authentication keys or shared keys.                          *)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   671
Goal "[| evs \\<in> kerberos;  K \\<in> (AuthKeys evs) Un range shrK;      \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   672
\        SesKey \\<notin> range shrK |]                                 \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   673
\     ==> Key K \\<in> analz (insert (Key SesKey) (spies evs)) = \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   674
\         (K = SesKey | Key K \\<in> analz (spies evs))";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   675
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   676
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   677
qed "analz_insert_freshK1";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   678
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   679
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   680
(* Second simplification law for analz: no service keys encrypt *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   681
(* any other keys.					        *)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   682
Goal "[| evs \\<in> kerberos;  ServKey \\<notin> (AuthKeys evs); ServKey \\<notin> range shrK|]\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   683
\     ==> Key K \\<in> analz (insert (Key ServKey) (spies evs)) = \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   684
\         (K = ServKey | Key K \\<in> analz (spies evs))";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   685
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   686
    THEN assume_tac 1
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   687
    THEN assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   688
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   689
qed "analz_insert_freshK2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   690
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   691
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   692
(* Third simplification law for analz: only one authentication key *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   693
(* encrypts a certain service key.                                 *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   694
Goal  
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   695
 "[| Says Tgs A    \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   696
\           (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   697
\             \\<in> set evs;          \ 
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   698
\           AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   699
\       ==> Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs)) =  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   700
\               (ServKey = AuthKey' | Key ServKey \\<in> analz (spies evs))";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   701
by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   702
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   703
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   704
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   705
qed "analz_insert_freshK3";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   706
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   707
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   708
(*a weakness of the protocol*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   709
Goal "[| Says Tgs A    \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   710
\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   711
\          \\<in> set evs;          \ 
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   712
\        Key AuthKey \\<in> analz (spies evs); evs \\<in> kerberos |]    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   713
\     ==> Key ServKey \\<in> analz (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   714
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   715
			       analz.Decrypt RS analz.Fst],
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   716
	       simpset()) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   717
qed "AuthKey_compromises_ServKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   718
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   719
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   720
(********************** Guarantees for Kas *****************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   721
Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   722
\                     Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   723
\          \\<in> parts (spies evs); \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   724
\        Key ServKey \\<notin> analz (spies evs);                          \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   725
\        B \\<noteq> Tgs; evs \\<in> kerberos |]                            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   726
\     ==> ServKey \\<notin> AuthKeys evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   727
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   728
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   729
by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   730
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   731
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   732
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   733
bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   734
bind_thm ("ServKey_notin_AuthKeysD", result());
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   735
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   736
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   737
(** If Spy sees the Authentication Key sent in msg K2, then 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   738
    the Key has expired  **)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   739
Goal "[| A \\<notin> bad;  evs \\<in> kerberos |]           \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   740
\     ==> Says Kas A                             \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   741
\              (Crypt (shrK A)                      \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   742
\                 {|Key AuthKey, Agent Tgs, Number Tk,     \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   743
\         Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   744
\           \\<in> set evs -->                 \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   745
\         Key AuthKey \\<in> analz (spies evs) -->                       \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   746
\         ExpirAuth Tk evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   747
by (etac kerberos.induct 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   748
by analz_sees_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   749
by (ALLGOALS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   750
    (asm_simp_tac 
8741
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   751
     (simpset() addsimps ([Says_Kas_message_form, less_SucI,
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   752
			   analz_insert_eq, not_parts_not_analz, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   753
			   analz_insert_freshK1] @ pushes))));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   754
(*Fake*) 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   755
by (spy_analz_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   756
(*K2*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   757
by (blast_tac (claset() addSEs spies_partsEs
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   758
            addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   759
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   760
by (blast_tac (claset() addSEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   761
(*Level 8: K5*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   762
by (blast_tac (claset() addEs [ServKey_notin_AuthKeys]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   763
                        addDs [Says_Kas_message_form, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   764
	       		       Says_imp_spies RS parts.Inj]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   765
                        addIs [less_SucI]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   766
(*Oops1*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   767
by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   768
(*Oops2*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   769
by (blast_tac (claset() addDs [Says_Tgs_message_form,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   770
                               Says_Kas_message_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   771
val lemma = result() RS mp RS mp RSN(1,rev_notE);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   772
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   773
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   774
Goal "[| Says Kas A                                             \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   775
\             (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   776
\          \\<in> set evs;                                \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   777
\        ~ ExpirAuth Tk evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   778
\        A \\<notin> bad;  evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   779
\     ==> Key AuthKey \\<notin> analz (spies evs)";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   780
by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   781
by (blast_tac (claset() addSDs [lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   782
qed "Confidentiality_Kas";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   783
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   784
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   785
(********************** Guarantees for Tgs *****************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   786
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   787
(** If Spy sees the Service Key sent in msg K4, then 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   788
    the Key has expired  **)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   789
Goal "[| A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]           \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   790
\  ==> Key AuthKey \\<notin> analz (spies evs) --> \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   791
\      Says Tgs A            \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   792
\        (Crypt AuthKey                      \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   793
\           {|Key ServKey, Agent B, Number Tt,     \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   794
\             Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   795
\        \\<in> set evs -->                 \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   796
\      Key ServKey \\<in> analz (spies evs) -->                       \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   797
\      ExpirServ Tt evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   798
by (etac kerberos.induct 1);
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   799
(*The Oops1 case is unusual: must simplify Authkey \\<notin> analz (spies (ev#evs))
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   800
  rather than weakening it to Authkey \\<notin> analz (spies evs), for we then
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   801
  conclude AuthKey \\<noteq> AuthKeya.*)
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   802
by (Clarify_tac 9);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   803
by analz_sees_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   804
by (rotate_tac ~1 11);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   805
by (ALLGOALS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   806
    (asm_full_simp_tac 
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   807
     (simpset() addsimps [less_SucI, new_keys_not_analzd,
8741
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   808
			  Says_Kas_message_form, Says_Tgs_message_form,
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   809
			  analz_insert_eq, not_parts_not_analz, 
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   810
			  analz_insert_freshK1, analz_insert_freshK2] 
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   811
			 @ pushes)));
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   812
(*Fake*) 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   813
by (spy_analz_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   814
(*K2*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   815
by (blast_tac (claset() addSEs spies_partsEs
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   816
            addIs [parts_insertI, less_SucI]) 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   817
(*K4*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   818
by (case_tac "A \\<noteq> Aa" 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   819
by (blast_tac (claset() addSEs spies_partsEs
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   820
                        addIs [less_SucI]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   821
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   822
                               A_trusts_AuthTicket, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   823
                               Confidentiality_Kas,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   824
                               impOfSubs analz_subset_parts]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   825
by (ALLGOALS Clarify_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   826
(*Oops2*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   827
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   828
                               Key_unique_SesKey] addIs [less_SucI]) 3);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   829
(** Level 12 **)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   830
(*Oops1*)
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   831
by (ftac Says_Kas_message_form 2);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   832
by (assume_tac 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   833
by (blast_tac (claset() addDs [analz_insert_freshK3,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   834
			       Says_Kas_message_form, Says_Tgs_message_form] 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   835
                        addIs  [less_SucI]) 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   836
(** Level 16 **)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   837
by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   838
by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   839
by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   840
by (rotate_tac ~1 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   841
by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   842
by (etac disjE 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   843
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   844
                               Key_unique_SesKey]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   845
by (blast_tac (claset() addIs [less_SucI]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   846
val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   847
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   848
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   849
(* In the real world Tgs can't check wheter AuthKey is secure! *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   850
Goal 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   851
 "[| Says Tgs A      \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   852
\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   853
\             \\<in> set evs;              \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   854
\           Key AuthKey \\<notin> analz (spies evs);        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   855
\           ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   856
\           A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   857
\        ==> Key ServKey \\<notin> analz (spies evs)";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   858
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   859
by (blast_tac (claset() addDs [lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   860
qed "Confidentiality_Tgs1";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   861
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   862
(* In the real world Tgs CAN check what Kas sends! *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   863
Goal 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   864
 "[| Says Kas A                                             \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   865
\              (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   866
\             \\<in> set evs;                                \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   867
\           Says Tgs A      \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   868
\             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   869
\             \\<in> set evs;              \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   870
\           ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   871
\           A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   872
\        ==> Key ServKey \\<notin> analz (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   873
by (blast_tac (claset() addSDs [Confidentiality_Kas,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   874
                                Confidentiality_Tgs1]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   875
qed "Confidentiality_Tgs2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   876
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   877
(*Most general form*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   878
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   879
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   880
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   881
(********************** Guarantees for Alice *****************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   882
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   883
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   884
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   885
Goal
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   886
 "[| Says Kas A \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   887
\      (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \\<in> set evs;\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   888
\    Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   889
\      \\<in> parts (spies evs);                                       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   890
\    Key AuthKey \\<notin> analz (spies evs);            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   891
\    evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   892
\==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   893
\      \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   894
by (ftac Says_Kas_message_form 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   895
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   896
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   897
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   898
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   899
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   900
(*K2 and K4 remain*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   901
by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   902
                        addSDs [unique_CryptKey]) 2);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   903
by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   904
				AuthKeys_used]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   905
qed "A_trusts_K4_bis";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   906
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   907
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   908
Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   909
\          \\<in> parts (spies evs);                              \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   910
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   911
\          \\<in> parts (spies evs);                                       \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   912
\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   913
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   914
\     ==> Key ServKey \\<notin> analz (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   915
by (dtac A_trusts_AuthKey 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   916
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   917
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   918
by (blast_tac (claset() addDs [Confidentiality_Kas, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   919
                               Says_Kas_message_form,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   920
                               A_trusts_K4_bis, Confidentiality_Tgs2]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   921
qed "Confidentiality_Serv_A";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   922
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   923
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   924
(********************** Guarantees for Bob *****************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   925
(* Theorems for the refined model have suffix "refined"                *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   926
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   927
Goal
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   928
"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   929
\            \\<in> set evs; evs \\<in> kerberos|]  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   930
\  ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   931
\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   932
\            \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   933
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   934
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   935
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   936
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   937
                               A_trusts_AuthTicket]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   938
qed "K4_imp_K2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   939
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   940
Goal
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   941
"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   942
\     \\<in> set evs; evs \\<in> kerberos|]  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   943
\  ==> \\<exists>Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   944
\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   945
\            \\<in> set evs   \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   946
\         & ServLife + Tt <= AuthLife + Tk)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   947
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   948
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   949
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   950
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   951
                               A_trusts_AuthTicket]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   952
qed "K4_imp_K2_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   953
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   954
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   955
\          \\<in> parts (spies evs);  B \\<noteq> Tgs;  B \\<notin> bad;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   956
\        evs \\<in> kerberos |]                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   957
\==> \\<exists>AuthKey. \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   958
\      Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt,  \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   959
\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   960
\      \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   961
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   962
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   963
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   964
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   965
qed "B_trusts_ServKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   966
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   967
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   968
\          \\<in> parts (spies evs);  B \\<noteq> Tgs;  B \\<notin> bad;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   969
\        evs \\<in> kerberos |]                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   970
\  ==> \\<exists>AuthKey Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   971
\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   972
\            \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   973
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   974
qed "B_trusts_ServTicket_Kas";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   975
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   976
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   977
\          \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   978
\        evs \\<in> kerberos |]                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   979
\  ==> \\<exists>AuthKey Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   980
\          Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   981
\            \\<in> set evs            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   982
\          & ServLife + Tt <= AuthLife + Tk)";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   983
by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   984
qed "B_trusts_ServTicket_Kas_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   985
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   986
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   987
\          \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad;        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   988
\        evs \\<in> kerberos |]                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   989
\==> \\<exists>Tk AuthKey.        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   990
\    Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   991
\                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   992
\      \\<in> set evs         \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   993
\    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   994
\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
   995
\      \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   996
by (ftac B_trusts_ServKey 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   997
by (etac exE 4);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
   998
by (ftac K4_imp_K2 4);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
   999
by (Blast_tac 5);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1000
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1001
qed "B_trusts_ServTicket";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1002
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1003
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1004
\          \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad;        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1005
\        evs \\<in> kerberos |]                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1006
\==> \\<exists>Tk AuthKey.        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1007
\    (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1008
\                  Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1009
\      \\<in> set evs         \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1010
\    & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt,  \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1011
\                  Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1012
\      \\<in> set evs         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1013
\    & ServLife + Tt <= AuthLife + Tk)";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1014
by (ftac B_trusts_ServKey 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1015
by (etac exE 4);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1016
by (ftac K4_imp_K2_refined 4);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1017
by (Blast_tac 5);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1018
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1019
qed "B_trusts_ServTicket_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1020
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1021
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1022
Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |]        \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1023
\  ==> ~ ExpirAuth Tk evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1024
by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1025
qed "NotExpirServ_NotExpirAuth_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1026
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1027
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1028
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1029
\          \\<in> parts (spies evs);                                        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1030
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1031
\          \\<in> parts (spies evs);                                         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1032
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1033
\          \\<in> parts (spies evs);                     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1034
\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;     \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1035
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1036
\     ==> Key ServKey \\<notin> analz (spies evs)";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1037
by (ftac A_trusts_AuthKey 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1038
by (ftac Confidentiality_Kas 3);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1039
by (ftac B_trusts_ServTicket 6);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1040
by (etac exE 9);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1041
by (etac exE 9);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1042
by (ftac Says_Kas_message_form 9);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1043
by (blast_tac (claset() addDs [A_trusts_K4, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1044
                               unique_ServKeys, unique_AuthKeys,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1045
                               Confidentiality_Tgs2]) 10);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1046
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1047
(*
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1048
The proof above executes in 8 secs. It can be done in one command in 50 secs:
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1049
by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1050
                               Says_Kas_message_form, B_trusts_ServTicket,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1051
                               unique_ServKeys, unique_AuthKeys,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1052
                               Confidentiality_Kas, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1053
                               Confidentiality_Tgs2]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1054
*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1055
qed "Confidentiality_B";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1056
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1057
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1058
(*Most general form -- only for refined model! *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1059
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1060
\          \\<in> parts (spies evs);                      \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1061
\        ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1062
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1063
\     ==> Key ServKey \\<notin> analz (spies evs)";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1064
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1065
			       NotExpirServ_NotExpirAuth_refined, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1066
                               Confidentiality_Tgs2]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1067
qed "Confidentiality_B_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1068
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1069
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1070
(********************** Authenticity theorems *****************************)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1071
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1072
(***1. Session Keys authenticity: they originated with servers.***)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1073
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1074
(*Authenticity of AuthKey for A: "A_trusts_AuthKey"*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1075
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1076
(*Authenticity of ServKey for A: "A_trusts_ServKey"*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1077
Goal "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1078
\          \\<in> parts (spies evs);                                     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1079
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1080
\          \\<in> parts (spies evs);                                        \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1081
\        ~ ExpirAuth Tk evs; A \\<notin> bad; evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1082
\==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1083
\      \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1084
by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1085
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1086
qed "A_trusts_ServKey"; 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1087
(*Note: requires a temporal check*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1088
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1089
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1090
(*Authenticity of ServKey for B: "B_trusts_ServKey"*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1091
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1092
(***2. Parties authenticity: each party verifies "the identity of
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1093
       another party who generated some data" (quoted from Neuman & Ts'o).***)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1094
       
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1095
       (*These guarantees don't assess whether two parties agree on 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1096
         the same session key: sending a message containing a key
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1097
         doesn't a priori state knowledge of the key.***)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1098
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1099
(*B checks authenticity of A: theorems "A_Authenticity", 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1100
                                       "A_authenticity_refined" *)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1101
Goal "[| Crypt ServKey {|Agent A, Number Ta|} \\<in> parts (spies evs);  \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1102
\        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1103
\                                    ServTicket|}) \\<in> set evs;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1104
\        Key ServKey \\<notin> analz (spies evs);                \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1105
\        A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos |]   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1106
\==> Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1107
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1108
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1109
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1110
by (etac kerberos.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1111
by (ftac Says_ticket_in_parts_spies 5);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1112
by (ftac Says_ticket_in_parts_spies 7);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1113
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1114
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1115
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1116
(*K3*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1117
by (blast_tac (claset() addEs spies_partsEs
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1118
                        addDs [A_trusts_AuthKey,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1119
                               Says_Kas_message_form, 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1120
                               Says_Tgs_message_form]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1121
(*K4*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1122
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1123
(*K5*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1124
by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1125
qed "Says_Auth";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1126
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1127
(*The second assumption tells B what kind of key ServKey is.*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1128
Goal "[| Crypt ServKey {|Agent A, Number Ta|} \\<in> parts (spies evs);     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1129
\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1130
\          \\<in> parts (spies evs);                                         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1131
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1132
\          \\<in> parts (spies evs);                                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1133
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1134
\          \\<in> parts (spies evs);                                            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1135
\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1136
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1137
\  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1138
\                 Crypt ServKey {|Agent A, Number Ta|} |} \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1139
by (ftac Confidentiality_B 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1140
by (ftac B_trusts_ServKey 9);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1141
by (etac exE 12);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1142
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1143
                        addSIs [Says_Auth]) 12);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1144
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1145
qed "A_Authenticity";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1146
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1147
(*Stronger form in the refined model*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1148
Goal "[| Crypt ServKey {|Agent A, Number Ta2|} \\<in> parts (spies evs);     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1149
\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1150
\          \\<in> parts (spies evs);                                         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1151
\        ~ ExpirServ Tt evs;                                        \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1152
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1153
\  ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1154
\                 Crypt ServKey {|Agent A, Number Ta2|} |} \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1155
by (ftac Confidentiality_B_refined 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1156
by (ftac B_trusts_ServKey 6);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1157
by (etac exE 9);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1158
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1159
                        addSIs [Says_Auth]) 9);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1160
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1161
qed "A_Authenticity_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1162
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1163
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1164
(*A checks authenticity of B: theorem "B_authenticity"*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1165
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1166
Goal "[| Crypt ServKey (Number Ta) \\<in> parts (spies evs);  \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1167
\        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1168
\                                    ServTicket|}) \\<in> set evs;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1169
\        Key ServKey \\<notin> analz (spies evs);                \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1170
\        A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos |]   \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1171
\     ==> Says B A (Crypt ServKey (Number Ta)) \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1172
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1173
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1174
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1175
by (etac kerberos.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1176
by (ftac Says_ticket_in_parts_spies 5);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1177
by (ftac Says_ticket_in_parts_spies 7);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1178
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1179
by (ALLGOALS Asm_simp_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1180
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1181
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1182
by (Clarify_tac 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1183
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1184
by (Clarify_tac 1);  (*PROOF FAILED if omitted*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1185
by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1186
qed "Says_K6";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1187
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1188
Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|}   \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1189
\          \\<in> parts (spies evs);    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1190
\        Key AuthKey \\<notin> analz (spies evs); AuthKey \\<notin> range shrK;  \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1191
\        evs \\<in> kerberos |]              \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1192
\ ==> \\<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1193
\             \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1194
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1195
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1196
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1197
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1198
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1199
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1200
qed "K4_trustworthy";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1201
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1202
Goal "[| Crypt ServKey (Number Ta) \\<in> parts (spies evs);           \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1203
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1204
\          \\<in> parts (spies evs);                                        \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1205
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1206
\          \\<in> parts (spies evs);                                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1207
\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1208
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1209
\     ==> Says B A (Crypt ServKey (Number Ta)) \\<in> set evs";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1210
by (ftac A_trusts_AuthKey 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1211
by (ftac Says_Kas_message_form 3);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1212
by (ftac Confidentiality_Kas 4);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1213
by (ftac K4_trustworthy 7);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1214
by (Blast_tac 8);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1215
by (etac exE 9);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1216
by (ftac K4_imp_K2 9);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1217
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1218
                        addSIs [Says_K6]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1219
                        addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1220
by (ALLGOALS assume_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1221
qed "B_Authenticity";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1222
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1223
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1224
(***3. Parties' knowledge of session keys. A knows a session key if she
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1225
       used it to build a cipher.***)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1226
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1227
Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs;           \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1228
\        Key ServKey \\<notin> analz (spies evs);                          \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1229
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1230
\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1231
by (simp_tac (simpset() addsimps [Issues_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1232
by (rtac exI 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1233
by (rtac conjI 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1234
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1235
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1236
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1237
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1238
by (etac kerberos.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1239
by (ftac Says_ticket_in_parts_spies 5);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1240
by (ftac Says_ticket_in_parts_spies 7);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1241
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1242
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1243
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1244
(*K6 requires numerous lemmas*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1245
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1246
by (blast_tac (claset() addDs [B_trusts_ServTicket,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1247
                               impOfSubs parts_spies_takeWhile_mono,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1248
                               impOfSubs parts_spies_evs_revD2]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1249
                        addIs [Says_K6]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1250
                        addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1251
qed "B_Knows_B_Knows_ServKey_lemma";
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1252
(*Key ServKey \\<notin> analz (spies evs) could be relaxed by Confidentiality_B
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1253
  but this is irrelevant because B knows what he knows!                  *)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1254
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1255
Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs;           \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1256
\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1257
\           \\<in> parts (spies evs);\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1258
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1259
\           \\<in> parts (spies evs);\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1260
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1261
\          \\<in> parts (spies evs);     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1262
\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;              \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1263
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1264
\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1265
by (blast_tac (claset() addSDs [Confidentiality_B,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1266
	                       B_Knows_B_Knows_ServKey_lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1267
qed "B_Knows_B_Knows_ServKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1268
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1269
Goal "[| Says B A (Crypt ServKey (Number Ta)) \\<in> set evs;           \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1270
\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1271
\           \\<in> parts (spies evs);\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1272
\        ~ ExpirServ Tt evs;            \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1273
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1274
\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1275
by (blast_tac (claset() addSDs [Confidentiality_B_refined,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1276
	                       B_Knows_B_Knows_ServKey_lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1277
qed "B_Knows_B_Knows_ServKey_refined";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1278
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1279
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1280
Goal "[| Crypt ServKey (Number Ta) \\<in> parts (spies evs);           \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1281
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1282
\          \\<in> parts (spies evs);                                        \ 
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1283
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1284
\          \\<in> parts (spies evs);                                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1285
\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;                         \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1286
\        A \\<notin> bad;  B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos |]            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1287
\     ==> B Issues A with (Crypt ServKey (Number Ta)) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1288
by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1289
                                B_Knows_B_Knows_ServKey_lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1290
qed "A_Knows_B_Knows_ServKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1291
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1292
Goal "[| Says A Tgs     \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1293
\            {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta|}, Agent B|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1294
\          \\<in> set evs;      \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1295
\        A \\<notin> bad;  evs \\<in> kerberos |]         \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1296
\     ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1297
\                     {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1298
\                  \\<in> set evs";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1299
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1300
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1301
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1302
by (Blast_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1303
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1304
			       A_trusts_AuthKey]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1305
qed "K3_imp_K2";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1306
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1307
Goal "[| Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}   \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1308
\          \\<in> parts (spies evs);                    \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1309
\        Says Kas A (Crypt (shrK A) \
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1310
\                    {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1311
\        \\<in> set evs;    \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1312
\        Key AuthKey \\<notin> analz (spies evs);       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1313
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1314
\  ==> Says Tgs A (Crypt AuthKey        \ 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1315
\                    {|Key ServKey, Agent B, Number Tt, ServTicket|})  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1316
\        \\<in> set evs";      
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1317
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1318
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1319
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1320
by (parts_induct_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1321
by (Fake_parts_insert_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1322
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1323
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1324
                               A_trusts_AuthTicket, unique_AuthKeys]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1325
qed "K4_trustworthy'";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1326
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1327
Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1328
\          \\<in> set evs;       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1329
\        Key ServKey \\<notin> analz (spies evs);       \
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1330
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1331
\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1332
by (simp_tac (simpset() addsimps [Issues_def]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1333
by (rtac exI 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1334
by (rtac conjI 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1335
by (assume_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1336
by (Simp_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1337
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1338
by (etac rev_mp 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1339
by (etac kerberos.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1340
by (ftac Says_ticket_in_parts_spies 5);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7494
diff changeset
  1341
by (ftac Says_ticket_in_parts_spies 7);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1342
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1343
by (ALLGOALS Asm_simp_tac);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1344
by (Clarify_tac 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1345
(*K6*)
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1346
by Auto_tac;
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1347
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1348
(*Level 15: case study necessary because the assumption doesn't state
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1349
  the form of ServTicket. The guarantee becomes stronger.*)
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1350
by (case_tac "Key AuthKey \\<in> analz (spies evs5)" 1);
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1351
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1352
			       analz.Decrypt RS analz.Fst],
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1353
	       simpset()) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1354
by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy',
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1355
                               impOfSubs parts_spies_takeWhile_mono,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1356
                               impOfSubs parts_spies_evs_revD2]
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1357
                        addIs [Says_Auth] 
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1358
                        addEs spies_partsEs) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1359
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1360
qed "A_Knows_A_Knows_ServKey_lemma";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1361
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1362
Goal "[| Says A B {|ServTicket, Crypt ServKey {|Agent A, Number Ta|}|} \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1363
\          \\<in> set evs;       \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1364
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1365
\          \\<in> parts (spies evs);\
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1366
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1367
\          \\<in> parts (spies evs);                                        \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1368
\        ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1369
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1370
\  ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1371
by (blast_tac (claset() addSDs [Confidentiality_Serv_A,
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1372
	                       A_Knows_A_Knows_ServKey_lemma]) 1);
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1373
qed "A_Knows_A_Knows_ServKey";
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1374
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1375
Goal "[| Crypt ServKey {|Agent A, Number Ta|} \\<in> parts (spies evs);     \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1376
\        Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}       \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1377
\          \\<in> parts (spies evs);                                         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1378
\        Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}  \ 
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1379
\          \\<in> parts (spies evs);                                          \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1380
\        Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1381
\          \\<in> parts (spies evs);                                            \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff changeset
  1382
\        ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;  \
11185
1b737b4c2108 Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents: 11104
diff changeset
  1383
\        B \\<noteq> Tgs; A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos |]         \
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents:
diff