src/HOL/Auth/TLS.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3506 a36e0a49d2cd
child 3515 d8a71f6eaf40
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/TLS
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     2
    ID:         $Id$
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     5
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     6
The public-key model has a weakness, especially concerning anonymous sessions.
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
     7
The Spy's state is recorded as the trace of message.  But if he himself is the
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
     8
Client and invents M, then he encrypts M with B's public key before sending
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
     9
it.  This message gives no evidence that the spy knows M, and yet the spy
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    10
actually chose M!  So, in any property concerning the secrecy of some item,
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    11
one must establish that the spy didn't choose the item.  Guarantees normally
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    12
assume that the other party is uncompromised (otherwise, one can prove
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    13
little).
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    14
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    15
Protocol goals: 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    16
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    17
     parties (though A is not necessarily authenticated).
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    18
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    19
* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    20
    message is optional!)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    21
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    22
* A upon receiving SERVER FINISHED knows that B is present
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    23
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    24
* Each party who has received a FINISHED message can trust that the other
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    25
  party agrees on all message components, including XA and XB (thus foiling
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    26
  rollback attacks).
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    27
*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    28
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    29
open TLS;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    30
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    31
proof_timing:=true;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    32
HOL_quantifiers := false;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    33
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    34
AddIffs [Spy_in_lost, Server_not_lost];
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    35
Addsimps [certificate_def];
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    36
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    37
goal thy "!!A. A ~: lost ==> A ~= Spy";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    38
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    39
qed "not_lost_not_eq_Spy";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    40
Addsimps [not_lost_not_eq_Spy];
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    41
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    42
(*Injectiveness of key-generating functions*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    43
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    44
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    45
(* invKey(clientK x) = clientK x  and similarly for serverK*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    46
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    47
	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    48
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    49
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    50
(*Replacing the variable by a constant improves search speed by 50%!*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    51
val Says_imp_sees_Spy' = 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    52
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    53
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    54
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    55
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    56
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    57
goal thy "pubK A ~= clientK arg";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    58
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    59
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    60
by (Full_simp_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    61
qed "pubK_neq_clientK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    62
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    63
goal thy "pubK A ~= serverK arg";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    64
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    65
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    66
by (Full_simp_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    67
qed "pubK_neq_serverK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    68
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    69
goal thy "priK A ~= clientK arg";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    70
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    71
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    72
by (Full_simp_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    73
qed "priK_neq_clientK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    74
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    75
goal thy "priK A ~= serverK arg";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    76
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    77
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    78
by (Full_simp_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    79
qed "priK_neq_serverK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    80
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    81
(*clientK and serverK have disjoint ranges*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    82
goal thy "clientK arg ~= serverK arg'";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    83
by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    84
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    85
qed "clientK_neq_serverK";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    86
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    87
val ths = [pubK_neq_clientK, pubK_neq_serverK, 
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    88
	   priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    89
AddIffs (ths @ (ths RL [not_sym]));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    90
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    91
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    92
(**** Protocol Proofs ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    93
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    94
(*A "possibility property": there are traces that reach the end.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    95
  This protocol has three end points and six messages to consider.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    96
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    97
(*Possibility property ending with ServerFinished.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    98
goal thy 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    99
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   100
\  Says B A (Crypt (serverK(NA,NB,M))                 \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   101
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   102
\                   Nonce NA, Agent XA, Agent A,      \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   103
\                   Nonce NB, Agent XB,               \
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   104
\                   certificate B (pubK B)|})) \
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   105
\    : set evs";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   106
by (REPEAT (resolve_tac [exI,bexI] 1));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   107
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   108
	  RS tls.ServerFinished) 2);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   109
by possibility_tac;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   110
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   111
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   112
(*And one for ClientFinished.  Either FINISHED message may come first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   113
goal thy 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   114
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   115
\  Says A B (Crypt (clientK(NA,NB,M))                 \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   116
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   117
\                   Nonce NA, Agent XA,               \
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   118
\                   certificate A (pubK A),      \
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   119
\                   Nonce NB, Agent XB, Agent B|})) : set evs";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   120
by (REPEAT (resolve_tac [exI,bexI] 1));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   121
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   122
	  RS tls.ClientFinished) 2);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   123
by possibility_tac;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   124
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   125
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   126
(*Another one, for CertVerify (which is optional)*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   127
goal thy 
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   128
 "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   129
\  Says A B (Crypt (priK A)                 \
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   130
\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   131
by (REPEAT (resolve_tac [exI,bexI] 1));
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   132
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   133
	  RS tls.CertVerify) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   134
by possibility_tac;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   135
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   136
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   137
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   138
(**** Inductive proofs about tls ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   139
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   140
(*Nobody sends themselves messages*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   141
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   142
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   143
by (Auto_tac());
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   144
qed_spec_mp "not_Says_to_self";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   145
Addsimps [not_Says_to_self];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   146
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   147
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   148
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   149
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   150
    sends messages containing X! **)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   151
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   152
(*Spy never sees another agent's private key! (unless it's lost at start)*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   153
goal thy 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   154
 "!!evs. evs : tls \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   155
\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   156
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   157
by (prove_simple_subgoals_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   158
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   159
qed "Spy_see_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   160
Addsimps [Spy_see_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   161
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   162
goal thy 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   163
 "!!evs. evs : tls \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   164
\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   165
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   166
qed "Spy_analz_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   167
Addsimps [Spy_analz_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   168
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   169
goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   170
\                  evs : tls |] ==> A:lost";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   171
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   172
qed "Spy_see_priK_D";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   173
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   174
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   175
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   176
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   177
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   178
(*Every Nonce that's hashed is already in past traffic. *)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   179
goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   180
\                   evs : tls |]  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   181
\                ==> Nonce N : parts (sees lost Spy evs)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   182
by (etac rev_mp 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   183
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   184
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   185
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   186
		      addSEs partsEs) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   187
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   188
qed "Hash_imp_Nonce1";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   189
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   190
(*Lemma needed to prove Hash_Hash_imp_Nonce*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   191
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   192
\                       : parts (sees lost Spy evs);     \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   193
\                   evs : tls |]  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   194
\                ==> Nonce M : parts (sees lost Spy evs)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   195
by (etac rev_mp 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   196
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   197
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   198
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   199
		      addSEs partsEs) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   200
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   201
qed "Hash_imp_Nonce2";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   202
AddSDs [Hash_imp_Nonce2];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   203
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   204
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   205
\                      : parts (sees lost Spy evs);      \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   206
\                   evs : tls |]                         \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   207
\                ==> Nonce M : parts (sees lost Spy evs)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   208
by (etac rev_mp 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   209
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   210
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   211
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   212
		      addSEs partsEs) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   213
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   214
qed "Hash_Hash_imp_Nonce";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   215
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   216
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   217
(*NEEDED??
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   218
  Every Nonce that's hashed is already in past traffic. 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   219
  This general formulation is tricky to prove and hard to use, since the
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   220
  2nd premise is typically proved by simplification.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   221
goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   222
\                   Nonce N : parts {X};  evs : tls |]  \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   223
\                ==> Nonce N : parts (sees lost Spy evs)";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   224
by (etac rev_mp 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   225
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   226
by (ALLGOALS Asm_simp_tac);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   227
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   228
		      addSEs partsEs) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   229
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   230
by (Fake_parts_insert_tac 1);
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   231
(*CertVerify, ClientFinished, ServerFinished (?)*)
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   232
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   233
qed "Hash_imp_Nonce_seen";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   234
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   235
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   236
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   237
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   238
(*B can check A's signature if he has received A's certificate.
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   239
  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   240
  message is Fake.  We don't need guarantees for the Spy anyway.  We must
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   241
  assume A~:lost; otherwise, the Spy can forge A's signature.*)
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   242
goalw thy [certificate_def]
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   243
 "!!evs. [| X = Crypt (priK A)                                        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   244
\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   245
\           evs : tls;  A ~: lost;  B ~= Spy |]                       \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   246
\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   247
\          : set evs --> \
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   248
\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   249
by (hyp_subst_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   250
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   251
by (ALLGOALS Asm_simp_tac);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   252
by (Fake_parts_insert_tac 1);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   253
(*ServerHello: nonce NB cannot be in X because it's fresh!*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   254
by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   255
	               addSEs sees_Spy_partsEs) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   256
qed_spec_mp "TrustCertVerify";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   257
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   258
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   259
goal thy
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   260
 "!!evs. [| evs : tls;  A ~= Spy |]                                      \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   261
\ ==> Says A B (Crypt (priK A)                                           \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   262
\               (Hash{|Nonce NB, certificate B KB, Nonce M|})) : set evs \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   263
\     --> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} : set evs";
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   264
by (etac tls.induct 1);
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   265
by (ALLGOALS Asm_full_simp_tac);
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   266
bind_thm ("UseCertVerify", result() RSN (2, rev_mp));
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   267
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   268
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   269
(*This lemma says that no false certificates exist.  One might extend the
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   270
  model to include bogus certificates for the lost agents, but there seems
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   271
  little point in doing so: the loss of their private keys is a worse
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   272
  breach of security.*)
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   273
goalw thy [certificate_def]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   274
 "!!evs. evs : tls     \
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   275
\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   276
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   277
by (ALLGOALS Asm_simp_tac);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   278
by (Fake_parts_insert_tac 2);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   279
by (Blast_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   280
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   281
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   282
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   283
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   284
val ClientCertKeyEx_tac = 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   285
    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   286
		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   287
    THEN' assume_tac
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   288
    THEN' hyp_subst_tac;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   289
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   290
fun analz_induct_tac i = 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   291
    etac tls.induct i   THEN
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   292
    ClientCertKeyEx_tac  (i+5)  THEN
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   293
    ALLGOALS (asm_simp_tac 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   294
              (!simpset addsimps [not_parts_not_analz]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   295
                        setloop split_tac [expand_if]))  THEN
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   296
    (*Remove instances of pubK B:  the Spy already knows all public keys.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   297
      Combining the two simplifier calls makes them run extremely slowly.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   298
    ALLGOALS (asm_simp_tac 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   299
              (!simpset addsimps [insert_absorb]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   300
                        setloop split_tac [expand_if]));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   301
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   302
(*** Specialized rewriting for the analz_image_... theorems ***)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   303
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   304
goal thy "insert (Key K) H = Key `` {K} Un H";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   305
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   306
qed "insert_Key_singleton";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   307
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   308
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   309
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   310
qed "insert_Key_image";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   311
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   312
(*Reverse the normal simplification of "image" to build up (not break down)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   313
  the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   314
val analz_image_keys_ss = 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   315
     !simpset delsimps [image_insert, image_Un]
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   316
              addsimps [image_insert RS sym, image_Un RS sym,
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   317
			rangeI, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   318
			insert_Key_singleton, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   319
			insert_Key_image, Un_assoc RS sym]
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   320
              setloop split_tac [expand_if];
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   321
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   322
(*No collection of keys can help the spy get new private keys*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   323
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   324
 "!!evs. evs : tls ==>                                    \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   325
\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   326
\            (priK B : KK | B : lost)";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   327
by (etac tls.induct 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   328
by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   329
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   330
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   331
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   332
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   333
qed_spec_mp "analz_image_priK";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   334
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   335
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   336
(*Lemma for the trivial direction of the if-and-only-if*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   337
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   338
 "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   339
\        (X : analz (G Un H))  =  (X : analz H)";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   340
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   341
val lemma = result();
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   342
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   343
(*Knowing some clientKs and serverKs is no help in getting new nonces*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   344
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   345
 "!!evs. evs : tls ==>                                 \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   346
\    ALL KK. KK <= (range clientK Un range serverK) -->           \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   347
\            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   348
\            (Nonce N : analz (sees lost Spy evs))";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   349
by (etac tls.induct 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   350
by (ClientCertKeyEx_tac 6);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   351
by (REPEAT_FIRST (resolve_tac [allI, impI]));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   352
by (REPEAT_FIRST (rtac lemma ));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   353
	(*SLOW: 30s!*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   354
by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   355
by (ALLGOALS (asm_simp_tac
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   356
	      (!simpset addsimps [analz_image_priK, insert_absorb])));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   357
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   358
by (Blast_tac 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   359
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   360
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   361
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   362
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   363
qed_spec_mp "analz_image_keys";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   364
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   365
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   366
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   367
  The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   368
  here.*)
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   369
goalw thy [certificate_def]
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   370
 "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   371
\        ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   372
\              : set evs  -->  Nonce M ~: analz (sees lost Spy evs)";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   373
by (analz_induct_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   374
(*ClientHello*)
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   375
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   376
(*SpyKeys*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   377
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   378
(*Fake*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   379
by (spy_analz_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   380
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   381
by (REPEAT (blast_tac (!claset addSEs partsEs
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   382
			       addDs  [impOfSubs analz_subset_parts,
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   383
				       Says_imp_sees_Spy' RS analz.Inj]) 1));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   384
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   385
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   386
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   387
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   388
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   389
(*The two proofs are identical*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   390
goal thy 
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   391
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   392
\           evs : tls |]                           \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   393
\        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   394
by (etac rev_mp 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   395
by (analz_induct_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   396
(*SpyKeys*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   397
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   398
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   399
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   400
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   401
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   402
by (Blast_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   403
qed "clientK_notin_parts";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   404
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   405
goal thy 
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   406
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   407
\           evs : tls |]                           \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   408
\        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   409
by (etac rev_mp 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   410
by (analz_induct_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   411
(*SpyKeys*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   412
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   413
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   414
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   415
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   416
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   417
by (Blast_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   418
qed "serverK_notin_parts";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   419
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   420
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   421
(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   422
     and has used the quoted values XA, XB, etc.  Note that it is up to A
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   423
     to compare XA with what she originally sent.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   424
***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   425
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   426
goalw thy [certificate_def]
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   427
 "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   428
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   429
\                        Nonce NA, Agent XA, Agent A,               \
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   430
\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   431
\           evs : tls;  A~=Spy;  B ~: lost |]                       \
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   432
\    ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   433
\          : set evs -->              \
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   434
\        X : parts (sees lost Spy evs) --> Says B A X : set evs";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   435
by (hyp_subst_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   436
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   437
by (ALLGOALS Asm_simp_tac);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   438
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   439
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   440
                       addSEs sees_Spy_partsEs) 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   441
(*Fake: the Spy doesn't have the critical session key!*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   442
by (REPEAT (rtac impI 1));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   443
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   444
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   445
				     serverK_notin_parts, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   446
				     not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   447
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   448
qed_spec_mp "TrustServerFinished";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   449
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   450
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   451
(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   452
     quoted values XA, XB, etc., which B can then check.  BUT NOTE:
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   453
     B has no way of knowing that A is the sender of CLIENT CERTIFICATE!
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   454
***)
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   455
goalw thy [certificate_def]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   456
 "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   457
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   458
\                        Nonce NA, Agent XA,                    \
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   459
\                        certificate A (pubK A),                \
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   460
\                        Nonce NB, Agent XB, Agent B|});        \
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   461
\           evs : tls;  A~=Spy;  B ~: lost |]                   \
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   462
\     ==> Says A B {|certificate A (pubK A),                    \
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   463
\                    Crypt KB (Nonce M)|} : set evs -->         \
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   464
\         X : parts (sees lost Spy evs) --> Says A B X : set evs";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   465
by (hyp_subst_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   466
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   467
by (ALLGOALS Asm_simp_tac);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   468
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   469
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   470
                       addSEs sees_Spy_partsEs) 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   471
(*Fake: the Spy doesn't have the critical session key!*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   472
by (REPEAT (rtac impI 1));
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   473
by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   474
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   475
				     clientK_notin_parts, 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   476
				     not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   477
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   478
qed_spec_mp "TrustClientFinished";
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   479
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   480
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   481
(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   482
     check a CERTIFICATE VERIFY from A, then A has used the quoted
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   483
     values XA, XB, etc.  Even this one requires A to be uncompromised.
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   484
 ***)
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   485
goal thy
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   486
 "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   487
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   488
\                        Nonce NA, Agent XA,                    \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   489
\                        certificate A (pubK A),                \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   490
\                        Nonce NB, Agent XB, Agent B|});        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   491
\           Says A' B X : set evs;                              \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   492
\           Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   493
\             : set evs;                                        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   494
\           Says A'' B (Crypt (priK A)                                   \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   495
\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))   \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   496
\             : set evs;                                        \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   497
\        evs : tls;  A ~: lost;  B ~: lost |]                   \
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   498
\     ==> Says A B X : set evs";
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   499
br TrustClientFinished 1;
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   500
br (TrustCertVerify RS UseCertVerify) 5;
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   501
by (REPEAT_FIRST (ares_tac [refl]));
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   502
by (ALLGOALS 
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   503
    (asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj])));
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   504
qed_spec_mp "AuthClientFinished";