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