src/HOL/Auth/Kerberos_BAN.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8741 61bc5ed22b62
child 10833 c0844a30ea4e
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Kerberos_BAN
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     2
    ID:         $Id$
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     3
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     5
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     6
The Kerberos protocol, BAN version.
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     7
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     8
From page 251 of
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    10
  Proc. Royal Soc. 426 (1989)
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
    11
5223
4cb05273f764 Removal of obsolete "open" commands from heads of .ML files
paulson
parents: 5114
diff changeset
    12
  Confidentiality (secrecy) and authentication properties rely on 
4cb05273f764 Removal of obsolete "open" commands from heads of .ML files
paulson
parents: 5114
diff changeset
    13
  temporal checks: strong guarantees in a little abstracted - but
4cb05273f764 Removal of obsolete "open" commands from heads of .ML files
paulson
parents: 5114
diff changeset
    14
  very realistic - model (see .thy).
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    15
5223
4cb05273f764 Removal of obsolete "open" commands from heads of .ML files
paulson
parents: 5114
diff changeset
    16
Tidied by lcp.
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    17
*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    18
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    19
AddEs spies_partsEs;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    20
AddDs [impOfSubs analz_subset_parts];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    21
AddDs [impOfSubs Fake_parts_insert];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    22
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
    23
AddIffs [SesKeyLife_LB, AutLife_LB];
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    24
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    25
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    26
(*A "possibility property": there are traces that reach the end.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5421
diff changeset
    27
Goal "EX Timestamp K. EX evs: kerberos_ban.    \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    28
\            Says B A (Crypt K (Number Timestamp)) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    29
\                 : set evs";
5352
paulson
parents: 5223
diff changeset
    30
by (cut_facts_tac [SesKeyLife_LB] 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    31
by (REPEAT (resolve_tac [exI,bexI] 1));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    32
by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    33
          kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    34
by possibility_tac;
5352
paulson
parents: 5223
diff changeset
    35
by (ALLGOALS Asm_simp_tac);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    36
result();
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    37
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    38
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    39
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    40
(**** Inductive proofs about kerberos_ban ****)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    41
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    42
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    43
Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    44
\             ==> X : parts (spies evs)";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    45
by (Blast_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    46
qed "Kb3_msg_in_parts_spies";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    47
                              
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    48
Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    49
\        ==> K : parts (spies evs)";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    50
by (Blast_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    51
qed "Oops_parts_spies";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    52
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    53
(*For proving the easier theorems about X ~: parts (spies evs).*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    54
fun parts_induct_tac i = 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    55
    etac kerberos_ban.induct i  THEN 
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
    56
    ftac Oops_parts_spies (i+6)  THEN
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
    57
    ftac Kb3_msg_in_parts_spies (i+4)     THEN
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    58
    prove_simple_subgoals_tac i;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    59
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    60
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    61
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    62
Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    63
by (parts_induct_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    64
by (ALLGOALS Blast_tac);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    65
qed "Spy_see_shrK";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    66
Addsimps [Spy_see_shrK];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    67
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    68
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    69
Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    70
by Auto_tac;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    71
qed "Spy_analz_shrK";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    72
Addsimps [Spy_analz_shrK];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    73
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    74
Goal  "[| Key (shrK A) : parts (spies evs);       \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    75
\               evs : kerberos_ban |] ==> A:bad";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    76
by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    77
qed "Spy_see_shrK_D";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    78
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    79
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    80
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    81
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    82
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    83
(*Nobody can have used non-existent keys!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    84
Goal "evs : kerberos_ban ==>      \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    85
\      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    86
by (parts_induct_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    87
(*Fake*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    88
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    89
(*Kb2, Kb3, Kb4*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    90
by (ALLGOALS Blast_tac);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    91
qed_spec_mp "new_keys_not_used";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    92
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    93
bind_thm ("new_keys_not_analzd",
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    94
          [analz_subset_parts RS keysFor_mono,
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    95
           new_keys_not_used] MRS contra_subsetD);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    96
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    97
Addsimps [new_keys_not_used, new_keys_not_analzd];
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    98
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
    99
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   100
(** Lemmas concerning the form of items passed in messages **)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   101
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   102
(*Describes the form of K, X and K' when the Server sends this message.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   103
Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   104
\        : set evs; evs : kerberos_ban |]                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   105
\     ==> K ~: range shrK &                                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   106
\         X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &      \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   107
\         K' = shrK A";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   108
by (etac rev_mp 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   109
by (etac kerberos_ban.induct 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   110
by Auto_tac;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   111
qed "Says_Server_message_form";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   112
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   113
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   114
(*If the encrypted message appears then it originated with the Server
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   115
  PROVIDED that A is NOT compromised!
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   116
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   117
  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   118
*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   119
Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   120
\          : parts (spies evs);                          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   121
\        A ~: bad;  evs : kerberos_ban |]                \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   122
\      ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   123
\            : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   124
by (etac rev_mp 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   125
by (parts_induct_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   126
by (Blast_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   127
qed "A_trusts_K_by_Kb2";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   128
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   129
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   130
(*If the TICKET appears then it originated with the Server*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   131
(*FRESHNESS OF THE SESSION KEY to B*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   132
Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   133
\        B ~: bad;  evs : kerberos_ban |]                        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   134
\      ==> Says Server A                                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   135
\           (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   136
\                         Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   137
\          : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   138
by (etac rev_mp 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   139
by (parts_induct_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   140
by (Blast_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   141
qed "B_trusts_K_by_Kb3";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   142
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   143
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   144
(*EITHER describes the form of X when the following message is sent, 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   145
  OR     reduces it to the Fake case.
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   146
  Use Says_Server_message_form if applicable.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   147
Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   148
\           : set evs;                                                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   149
\        evs : kerberos_ban |]                                          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   150
\==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   151
\         | X : analz (spies evs)";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   152
by (case_tac "A : bad" 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   153
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   154
                      addss (simpset())) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   155
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   156
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   157
				Says_Server_message_form]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   158
qed "Says_S_message_form";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   159
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   160
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   161
(*For proofs involving analz.*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   162
val analz_spies_tac = 
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   163
    ftac Says_Server_message_form 7 THEN
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   164
    ftac Says_S_message_form 5 THEN 
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   165
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   166
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   167
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   168
(****
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   169
 The following is to prove theorems of the form
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   170
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   171
  Key K : analz (insert (Key KAB) (spies evs)) ==>
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   172
  Key K : analz (spies evs)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   173
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   174
 A more general formula must be proved inductively.
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   175
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   176
****)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   177
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   178
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   179
(** Session keys are not used to encrypt other session keys **)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   180
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   181
Goal "evs : kerberos_ban ==>                          \
5492
d9fc3457554e From Compl(A) to -A
paulson
parents: 5479
diff changeset
   182
\  ALL K KK. KK <= - (range shrK) -->                 \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   183
\         (Key K : analz (Key``KK Un (spies evs))) =  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   184
\         (K : KK | Key K : analz (spies evs))";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   185
by (etac kerberos_ban.induct 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   186
by analz_spies_tac;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   187
by (REPEAT_FIRST (resolve_tac [allI, impI]));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   188
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   189
(*Takes 5 secs*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   190
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   191
(*Fake*) 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   192
by (spy_analz_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   193
qed_spec_mp "analz_image_freshK";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   194
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   195
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   196
Goal "[| evs : kerberos_ban;  KAB ~: range shrK |] ==>     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   197
\     Key K : analz (insert (Key KAB) (spies evs)) =       \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   198
\     (K = KAB | Key K : analz (spies evs))";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   199
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   200
qed "analz_insert_freshK";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   201
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   202
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   203
(** The session key K uniquely identifies the message **)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   204
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   205
Goal "evs : kerberos_ban ==>                                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   206
\   EX A' Ts' B' X'. ALL A Ts B X.                                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   207
\    Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   208
\          : set evs \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   209
\    -->         A=A' & Ts=Ts' & B=B' & X=X'";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   210
by (etac kerberos_ban.induct 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   211
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   212
by Safe_tac;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   213
(*Kb2: it can't be a new key*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   214
by (expand_case_tac "K = ?y" 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   215
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   216
by (blast_tac (claset() delrules [conjI]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   217
val lemma = result();
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   218
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   219
(*In messages of this form, the session key uniquely identifies the rest*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   220
Goal "[| Says Server A                                    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   221
\          (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ 
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   222
\        Says Server A'                                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   223
\         (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   224
\        evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   225
by (prove_unique_tac lemma 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   226
qed "unique_session_keys";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   227
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   228
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   229
(** Lemma: the session key sent in msg Kb2 would be EXPIRED
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   230
    if the spy could see it!
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   231
**)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   232
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   233
Goal "[| A ~: bad;  B ~: bad;  evs : kerberos_ban |]           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   234
\ ==> Says Server A                                            \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   235
\         (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   236
\                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   237
\        : set evs -->                                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   238
\     Key K : analz (spies evs) --> Expired Ts evs"; 
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   239
by (etac kerberos_ban.induct 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   240
by analz_spies_tac;
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   241
by (ALLGOALS
8741
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   242
    (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, 
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   243
				       analz_insert_freshK]
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7499
diff changeset
   244
		                      @ pushes)));
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   245
(*Oops*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   246
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   247
(*Kb2*)
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   248
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   249
(*Fake*) 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   250
by (spy_analz_tac 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   251
(**LEVEL 6 **)
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   252
(*Kb3*)
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   253
by (case_tac "Aa : bad" 1);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   254
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   255
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   256
                               Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   257
                        addIs [less_SucI]) 1);
5479
5a5dfb0f0d7d fixed PROOF FAILED
paulson
parents: 5434
diff changeset
   258
qed_spec_mp "lemma2";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   259
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   260
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   261
(** CONFIDENTIALITY for the SERVER:
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   262
                     Spy does not see the keys sent in msg Kb2 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   263
                     as long as they have NOT EXPIRED
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   264
**)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   265
Goal "[| Says Server A                                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   266
\         (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   267
\        ~ Expired T evs;                                        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   268
\        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   269
\     |] ==> Key K ~: analz (spies evs)";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   270
by (ftac Says_Server_message_form 1 THEN assume_tac 1);
5479
5a5dfb0f0d7d fixed PROOF FAILED
paulson
parents: 5434
diff changeset
   271
by (blast_tac (claset() addIs [lemma2]) 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   272
qed "Confidentiality_S";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   273
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   274
(**** THE COUNTERPART OF CONFIDENTIALITY 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   275
      [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   276
      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   277
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   278
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   279
(** CONFIDENTIALITY for ALICE: **)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   280
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   281
Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   282
\        ~ Expired T evs;          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   283
\        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   284
\     |] ==> Key K ~: analz (spies evs)";
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   285
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   286
qed "Confidentiality_A";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   287
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   288
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   289
(** CONFIDENTIALITY for BOB: **)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   290
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   291
Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   292
\         : parts (spies evs);              \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   293
\       ~ Expired Tk evs;          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   294
\       A ~: bad;  B ~: bad;  evs : kerberos_ban                \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   295
\     |] ==> Key K ~: analz (spies evs)";             
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   296
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   297
                                Confidentiality_S]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   298
qed "Confidentiality_B";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   299
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   300
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   301
Goal "[| B ~: bad;  evs : kerberos_ban |]                        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   302
\     ==> Key K ~: analz (spies evs) -->                    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   303
\         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   304
\         : set evs -->                                             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   305
\         Crypt K (Number Ta) : parts (spies evs) -->        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   306
\         Says B A (Crypt K (Number Ta)) : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   307
by (etac kerberos_ban.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   308
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   309
by (dtac Kb3_msg_in_parts_spies 5);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   310
by (ftac Oops_parts_spies 7);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   311
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   312
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   313
(**LEVEL 6**)
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   314
by (Blast_tac 1);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   315
by (Clarify_tac 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   316
(*
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   317
Subgoal 1: contradiction from the assumptions  
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   318
Key K ~: used evs2  and Crypt K (Number Ta) : parts (spies evs2)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   319
*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   320
by (dtac Crypt_imp_invKey_keysFor 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   321
by (Asm_full_simp_tac 1);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   322
(* the two tactics above detect the contradiction*)
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   323
by (case_tac "Ba : bad" 1);  (*splits up the subgoal by the stated case*)
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   324
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   325
                              B_trusts_K_by_Kb3, 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   326
			      unique_session_keys]) 2);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   327
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   328
			      Crypt_Spy_analz_bad]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   329
val lemma_B = result();
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   330
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   331
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   332
(*AUTHENTICATION OF B TO A*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   333
Goal "[| Crypt K (Number Ta) : parts (spies evs);           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   334
\        Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   335
\        : parts (spies evs);                               \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   336
\        ~ Expired Ts evs;                                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   337
\        A ~: bad;  B ~: bad;  evs : kerberos_ban |]        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   338
\     ==> Says B A (Crypt K (Number Ta)) : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   339
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   340
                        addSIs [lemma_B RS mp RS mp RS mp]
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   341
                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   342
qed "Authentication_B";
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   343
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   344
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   345
Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |]      ==>         \ 
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   346
\        Key K ~: analz (spies evs) -->         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   347
\        Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   348
\        : set evs -->  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   349
\         Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   350
\        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   351
\            : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   352
by (etac kerberos_ban.induct 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   353
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   354
by (ftac Kb3_msg_in_parts_spies 5);
23e090051cb8 isatool expandshort;
wenzelm
parents: 5983
diff changeset
   355
by (ftac Oops_parts_spies 7);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   356
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   357
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   358
(**LEVEL 6**)
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   359
by (Blast_tac 1);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   360
by (Clarify_tac 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   361
by (dtac Crypt_imp_invKey_keysFor 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   362
by (Asm_full_simp_tac 1);
5064
77bd19f782e6 simplified and tidied the proofs
paulson
parents: 5053
diff changeset
   363
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   364
val lemma_A = result();
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   365
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   366
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   367
(*AUTHENTICATION OF A TO B*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   368
Goal "[| Crypt K {|Agent A, Number Ta|} : parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   369
\        Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   370
\        : parts (spies evs);                                 \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   371
\        ~ Expired Ts evs;                                    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   372
\        A ~: bad;  B ~: bad;  evs : kerberos_ban |]          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   373
\     ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \    
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   374
\                    Crypt K {|Agent A, Number Ta|}|} : set evs";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   375
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   376
                        addSIs [lemma_A RS mp RS mp RS mp]
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   377
                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents:
diff changeset
   378
qed "Authentication_A";