src/HOL/Auth/TLS.ML
author paulson
Tue, 30 Sep 1997 11:03:55 +0200
changeset 3745 4c5d3b1ddc75
parent 3729 6be7cf5086ab
child 3758 188a4fbfaf55
permissions -rw-r--r--
Client, Server certificates now sent using the separate Certificate rule, simplifying ServerHello and ClientKeyExch. Resumption no longer needs its own version of ServerHello. Proofs run nearly three minutes faster.
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
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
     6
Protocol goals: 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
     7
* 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
     8
     parties (though A is not necessarily authenticated).
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
     9
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    10
* B upon receiving CertVerify knows that A is present (But this
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    11
    message is optional!)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    12
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    13
* A upon receiving ServerFinished knows that B is present
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
* Each party who has received a FINISHED message can trust that the other
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
    16
  party agrees on all message components, including PA and PB (thus foiling
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    17
  rollback attacks).
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    18
*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    19
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
    20
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    21
open TLS;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    22
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    23
proof_timing:=true;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    24
HOL_quantifiers := false;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    25
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    26
(** We mostly DO NOT unfold the definition of "certificate".  The attached
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    27
    lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    28
    contexts.
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    29
**)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    30
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    31
goalw thy [certificate_def] 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    32
    "parts (insert (certificate B KB) H) =  \
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    33
\    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    34
by (rtac refl 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    35
qed "parts_insert_certificate";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    36
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    37
goalw thy [certificate_def] 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    38
    "analz (insert (certificate B KB) H) =  \
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    39
\    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    40
by (rtac refl 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    41
qed "analz_insert_certificate";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    42
Addsimps [parts_insert_certificate, analz_insert_certificate];
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    43
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    44
goalw thy [certificate_def] 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    45
    "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    46
by (Blast_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    47
qed "eq_certificate_iff";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    48
AddIffs [eq_certificate_iff];
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
    49
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    50
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    51
(*Injectiveness of key-generating functions*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    52
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    53
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    54
(* invKey(sessionK x) = sessionK x*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    55
Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    56
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    57
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    58
(*** 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
    59
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    60
goal thy "pubK A ~= sessionK arg";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    61
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    62
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    63
by (Full_simp_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    64
qed "pubK_neq_sessionK";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    65
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    66
goal thy "priK A ~= sessionK arg";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    67
br notI 1;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    68
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    69
by (Full_simp_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    70
qed "priK_neq_sessionK";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    71
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    72
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
    73
AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
3474
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
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    76
(**** Protocol Proofs ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    77
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    78
(*A "possibility property": there are traces that reach the end.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    79
  This protocol has three end points and six messages to consider.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    80
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    81
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    82
(** These proofs make the further assumption that the Nonce_supply nonces 
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    83
	(which have the form  @ N. Nonce N ~: used evs)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    84
    lie outside the range of PRF.  This assumption seems reasonable, but
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    85
    as it is needed only for the possibility theorems, it is not taken
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    86
    as an axiom.
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    87
**)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    88
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    89
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    90
(*Possibility property ending with ClientAccepts.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    91
goal thy 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    92
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    93
\           A ~= B |] ==> EX SID M. EX evs: tls.    \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    94
\  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    95
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    96
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    97
	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    98
	  tls.ClientAccepts) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    99
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   100
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   101
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   102
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   103
(*And one for ServerAccepts.  Either FINISHED message may come first.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   104
goal thy 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   105
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   106
\           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   107
\  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   108
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   109
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   110
	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   111
	  tls.ServerAccepts) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   112
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   113
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   114
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   115
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   116
(*Another one, for CertVerify (which is optional)*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   117
goal thy 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   118
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   119
\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   120
\  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   121
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   122
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   123
	  tls.ClientKeyExch RS tls.CertVerify) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   124
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   125
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   126
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   127
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   128
(*Another one, for session resumption (both ServerResume and ClientResume) *)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   129
goal thy 
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   130
 "!!A B. [| evs0 : tls;     \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   131
\           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   132
\           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   133
\           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   134
\           A ~= B |] ==> EX NA PA NB PB. EX evs: tls.    \
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   135
\  Says A B (Crypt (clientK(NA,NB,M))                           \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   136
\            (Hash{|Nonce M, Number SID,             \
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   137
\                   Nonce NA, Number PA, Agent A,      \
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   138
\                   Nonce NB, Number PB, Agent B|})) : set evs";
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   139
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   140
by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   141
	  tls.ClientResume) 2);
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   142
by possibility_tac;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   143
by (REPEAT (Blast_tac 1));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   144
result();
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   145
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   146
3474
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
(**** Inductive proofs about tls ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   149
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   150
(*Nobody sends themselves messages*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   151
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
   152
by (etac tls.induct 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   153
by (Auto_tac());
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   154
qed_spec_mp "not_Says_to_self";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   155
Addsimps [not_Says_to_self];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   156
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   157
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   158
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   159
(*Induction for regularity theorems.  If induction formula has the form
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   160
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   161
   needless information about analz (insert X (spies evs))  *)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   162
fun parts_induct_tac i = 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   163
    etac tls.induct i
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   164
    THEN 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   165
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   166
    THEN 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   167
    fast_tac (!claset addss (!simpset)) i THEN
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   168
    ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   169
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   170
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   171
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   172
    sends messages containing X! **)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   173
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   174
(*Spy never sees another agent's private key! (unless it's bad at start)*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   175
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   176
 "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   177
by (parts_induct_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   178
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   179
qed "Spy_see_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   180
Addsimps [Spy_see_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   181
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   182
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   183
 "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   184
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   185
qed "Spy_analz_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   186
Addsimps [Spy_analz_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   187
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   188
goal thy  "!!A. [| Key (priK A) : parts (spies evs);  evs : tls |] ==> A:bad";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   189
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   190
qed "Spy_see_priK_D";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   191
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   192
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
   193
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   194
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   195
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   196
(*This lemma says that no false certificates exist.  One might extend the
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   197
  model to include bogus certificates for the agents, but there seems
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   198
  little point in doing so: the loss of their private keys is a worse
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   199
  breach of security.*)
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   200
goalw thy [certificate_def]
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   201
 "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   202
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   203
by (Fake_parts_insert_tac 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   204
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   205
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   206
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   207
(*Replace key KB in ClientKeyExch by (pubK B) *)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   208
val ClientKeyExch_tac = 
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   209
    forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   210
    THEN' assume_tac
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   211
    THEN' hyp_subst_tac;
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   212
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   213
fun analz_induct_tac i = 
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   214
    etac tls.induct i   THEN
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   215
    ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   216
    ALLGOALS (asm_simp_tac 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   217
              (!simpset addcongs [if_weak_cong]
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   218
                        setloop split_tac [expand_if]))  THEN
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   219
    (*Remove instances of pubK B:  the Spy already knows all public keys.
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   220
      Combining the two simplifier calls makes them run extremely slowly.*)
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   221
    ALLGOALS (asm_simp_tac 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   222
              (!simpset addcongs [if_weak_cong]
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   223
			addsimps [insert_absorb]
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   224
                        setloop split_tac [expand_if]));
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   225
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   226
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   227
(*** Notes are made under controlled circumstances ***)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   228
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   229
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   230
\                ==> Crypt (pubK B) X : parts (spies evs)";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   231
by (etac rev_mp 1);
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   232
by (analz_induct_tac 1);
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   233
by (blast_tac (!claset addIs [parts_insertI]) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   234
qed "Notes_Crypt_parts_spies";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   235
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   236
(*C might be either A or B*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   237
goal thy
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   238
    "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce M|} : set evs;  \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   239
\              evs : tls     \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   240
\           |] ==> M : range PRF";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   241
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   242
by (parts_induct_tac 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   243
by (Auto_tac());
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   244
qed "Notes_master_range_PRF";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   245
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   246
(*C might be either A or B*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   247
goal thy
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   248
 "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   249
\             : set evs;     evs : tls     \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   250
\        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   251
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   252
by (parts_induct_tac 1);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   253
by (ALLGOALS Clarify_tac);
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   254
(*Fake*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   255
by (blast_tac (!claset addIs [parts_insertI]) 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   256
(*Client, Server Accept*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   257
by (REPEAT (blast_tac (!claset addSEs spies_partsEs
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   258
                               addSDs [Notes_Crypt_parts_spies]) 1));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   259
qed "Notes_master_imp_Crypt_PMS";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   260
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   261
(*Compared with the theorem above, both premise and conclusion are stronger*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   262
goal thy
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   263
 "!!evs. [| Notes A {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   264
\             : set evs;     evs : tls     \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   265
\        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   266
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   267
by (parts_induct_tac 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   268
(*ServerAccepts*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   269
by (Fast_tac 1);	(*Blast_tac's very slow here*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   270
qed "Notes_master_imp_Notes_PMS";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   271
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   272
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   273
(*Every Nonce that's hashed is already in past traffic; this event
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   274
  occurs in CertVerify.  The condition NB ~: range PRF excludes the 
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   275
  MASTER SECRET from consideration; it is created using PRF.*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   276
goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs);  \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   277
\                   NB ~: range PRF;  evs : tls |]  \
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   278
\                ==> Nonce NB : parts (spies evs)";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   279
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   280
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   281
by (parts_induct_tac 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   282
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   283
(*Server/Client Resume: wrong sort of nonce!*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   284
by (REPEAT (blast_tac (!claset addSDs [Notes_master_range_PRF]) 5));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   285
(*FINISHED messages are trivial because M : range PRF*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   286
by (REPEAT (Blast_tac 3));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   287
(*CertVerify is the only interesting case*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   288
by (blast_tac (!claset addSEs spies_partsEs) 2);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   289
by (Fake_parts_insert_tac 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   290
qed "Hash_Nonce_CV";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   291
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   292
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   293
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   294
(*** Protocol goal: if B receives CertVerify, then A sent it ***)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   295
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   296
(*B can check A's signature if he has received A's certificate.*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   297
goal thy
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   298
 "!!evs. [| X : parts (spies evs);          \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   299
\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});      \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   300
\           evs : tls;  A ~: bad |]                       \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   301
\    ==> Says A B X : set evs";
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   302
by (etac rev_mp 1);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   303
by (hyp_subst_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   304
by (parts_induct_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   305
by (Fake_parts_insert_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   306
val lemma = result();
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   307
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   308
(*Final version: B checks X using the distributed KA instead of priK A*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   309
goal thy
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   310
 "!!evs. [| X : parts (spies evs);          \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   311
\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});      \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   312
\           certificate A KA : parts (spies evs);       \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   313
\           evs : tls;  A ~: bad |]                       \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   314
\    ==> Says A B X : set evs";
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   315
by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   316
qed "TrustCertVerify";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   317
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   318
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   319
(*If CertVerify is present then A has chosen PMS.*)
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   320
goal thy
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   321
 "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|})  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   322
\             : parts (spies evs);                                \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   323
\           evs : tls;  A ~: bad |]                                      \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   324
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   325
be rev_mp 1;
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   326
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   327
by (Fake_parts_insert_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   328
val lemma = result();
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   329
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   330
(*Final version using the distributed KA instead of priK A*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   331
goal thy
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   332
 "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})  \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   333
\             : parts (spies evs);                                \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   334
\           certificate A KA : parts (spies evs);       \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   335
\           evs : tls;  A ~: bad |]                                      \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   336
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   337
by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   338
qed "UseCertVerify";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   339
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   340
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   341
(*Key compromise lemma needed to prove analz_image_keys.
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   342
  No collection of keys can help the spy get new private keys.*)
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   343
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   344
 "!!evs. evs : tls ==>                                    \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   345
\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   346
\          (priK B : KK | B : bad)";
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   347
by (etac tls.induct 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   348
by (ALLGOALS
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   349
    (asm_simp_tac (analz_image_keys_ss
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   350
		   addsimps (analz_insert_certificate::keys_distinct))));
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   351
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   352
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   353
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   354
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   355
qed_spec_mp "analz_image_priK";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   356
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   357
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   358
(*slightly speeds up the big simplification below*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   359
goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   360
by (Blast_tac 1);
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   361
val range_sessionkeys_not_priK = result();
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   362
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   363
(*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
   364
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   365
 "!!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
   366
\        (X : analz (G Un H))  =  (X : analz H)";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   367
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
   368
val lemma = result();
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   369
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   370
(** It is a mystery to me why the following formulation is actually slower
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   371
    in simplification:
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   372
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   373
\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   374
\           (Nonce N : analz (spies evs))";
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   375
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   376
More so as it can take advantage of unconditional rewrites such as 
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   377
     priK B ~: sessionK``Z
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   378
**)
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   379
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   380
goal thy  
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   381
 "!!evs. evs : tls ==>                                 \
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   382
\    ALL KK. KK <= range sessionK -->           \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   383
\            (Nonce N : analz (Key``KK Un (spies evs))) = \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   384
\            (Nonce N : analz (spies evs))";
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   385
by (etac tls.induct 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   386
by (ClientKeyExch_tac 7);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   387
by (REPEAT_FIRST (resolve_tac [allI, impI]));
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   388
by (REPEAT_FIRST (rtac lemma));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   389
by (ALLGOALS    (*23 seconds*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   390
    (asm_simp_tac (analz_image_keys_ss 
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   391
		   addsimps [range_sessionkeys_not_priK, 
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   392
			     analz_image_priK, analz_insert_certificate])));
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   393
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   394
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   395
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   396
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   397
by (Blast_tac 1);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   398
qed_spec_mp "analz_image_keys";
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   399
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   400
(*Knowing some session keys is no help in getting new nonces*)
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   401
goal thy
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   402
 "!!evs. evs : tls ==>          \
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   403
\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   404
\        (Nonce N : analz (spies evs))";
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   405
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   406
qed "analz_insert_key";
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   407
Addsimps [analz_insert_key];
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   408
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   409
goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   410
by (parts_induct_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   411
(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   412
by (Blast_tac 1);
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   413
qed "no_Notes_A_PRF";
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   414
Addsimps [no_Notes_A_PRF];
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   415
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   416
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   417
goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   418
\                   evs : tls |]  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   419
\                ==> Nonce PMS : parts (spies evs)";
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   420
by (etac rev_mp 1);
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   421
by (parts_induct_tac 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   422
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   423
by (Fake_parts_insert_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   424
(*Six others, all trivial or by freshness*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   425
by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   426
                               addSEs spies_partsEs) 1));
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   427
qed "MS_imp_PMS";
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   428
AddSDs [MS_imp_PMS];
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   429
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   430
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   431
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   432
(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   433
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   434
(** Some lemmas about session keys, comprising clientK and serverK **)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   435
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   436
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   437
(*Lemma: session keys are never used if PMS is fresh.  
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   438
  Nonces don't have to agree, allowing session resumption.
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   439
  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   440
  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   441
goal thy 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   442
 "!!evs. [| Nonce PMS ~: parts (spies evs);  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   443
\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   444
\           evs : tls |]             \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   445
\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   446
by (etac rev_mp 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   447
by (hyp_subst_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   448
by (analz_induct_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   449
(*SpyKeys*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   450
by (blast_tac (!claset addSEs spies_partsEs) 3);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   451
(*Fake*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   452
by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   453
by (Fake_parts_insert_tac 2);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   454
(** LEVEL 6 **)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   455
(*Oops*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   456
by (fast_tac (!claset addSEs [MPair_parts]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   457
		       addDs  [Says_imp_spies RS parts.Inj]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   458
		       addss (!simpset)) 6);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   459
by (REPEAT 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   460
    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   461
				Notes_master_imp_Crypt_PMS]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   462
                        addSEs spies_partsEs) 1));
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   463
val lemma = result();
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   464
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   465
goal thy 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   466
 "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   467
\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   468
by (blast_tac (!claset addDs [lemma]) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   469
qed "PMS_sessionK_not_spied";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   470
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   471
goal thy 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   472
 "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   473
\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   474
by (blast_tac (!claset addDs [lemma]) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   475
qed "PMS_Crypt_sessionK_not_spied";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   476
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   477
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   478
(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   479
  Converse doesn't hold; betraying M doesn't force the keys to be sent!
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   480
  The strong Oops condition can be weakened later by unicity reasoning, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   481
	with some effort.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   482
goal thy 
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   483
 "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   484
\           Nonce M ~: analz (spies evs);  evs : tls |]   \
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   485
\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   486
by (etac rev_mp 1);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   487
by (etac rev_mp 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   488
by (analz_induct_tac 1);        (*17 seconds*)
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   489
(*Oops*)
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   490
by (Blast_tac 4);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   491
(*SpyKeys*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   492
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   493
(*Fake*) 
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   494
by (spy_analz_tac 2);
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   495
(*Base*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   496
by (Blast_tac 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   497
qed "sessionK_not_spied";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   498
Addsimps [sessionK_not_spied];
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   499
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   500
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   501
(*NEEDED??*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   502
goal thy
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   503
 "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   504
\           A ~= Spy;  evs : tls |] ==> KB = pubK B";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   505
be rev_mp 1;
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   506
by (analz_induct_tac 1);
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   507
qed "A_Crypt_pubB";
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   508
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   509
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   510
(*** Unicity results for PMS, the pre-master-secret ***)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   511
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   512
(*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   513
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   514
 "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   515
\        ==> EX B'. ALL B.   \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   516
\              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   517
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   518
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   519
by (Fake_parts_insert_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   520
(*ClientKeyExch*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   521
by (ClientKeyExch_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   522
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   523
by (expand_case_tac "PMS = ?y" 1 THEN
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   524
    blast_tac (!claset addSEs partsEs) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   525
val lemma = result();
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   526
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   527
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   528
 "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   529
\           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   530
\           Nonce PMS ~: analz (spies evs);                 \
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   531
\           evs : tls |]                                          \
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   532
\        ==> B=B'";
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   533
by (prove_unique_tac lemma 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   534
qed "Crypt_unique_PMS";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   535
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   536
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   537
(** It is frustrating that we need two versions of the unicity results.
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   538
    But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   539
    we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   540
    determines B alone, and only if PMS is secret.
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   541
**)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   542
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   543
(*In A's internal Note, PMS determines A and B.*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   544
goal thy "!!evs. evs : tls               \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   545
\                ==> EX A' B'. ALL A B.  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   546
\                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   547
by (parts_induct_tac 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   548
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   549
(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   550
by (expand_case_tac "PMS = ?y" 1 THEN
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   551
    blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   552
val lemma = result();
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   553
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   554
goal thy 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   555
 "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   556
\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   557
\           evs : tls |]                               \
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   558
\        ==> A=A' & B=B'";
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   559
by (prove_unique_tac lemma 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   560
qed "Notes_unique_PMS";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   561
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   562
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   563
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   564
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   565
goal thy
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   566
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   567
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   568
\            Nonce PMS ~: analz (spies evs)";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   569
by (analz_induct_tac 1);   (*11 seconds*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   570
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   571
by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   572
(*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   573
  mostly freshness reasoning*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   574
by (REPEAT (blast_tac (!claset addSEs partsEs
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   575
			       addDs  [Notes_Crypt_parts_spies,
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   576
				       impOfSubs analz_subset_parts,
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   577
				       Says_imp_spies RS analz.Inj]) 3));
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   578
(*SpyKeys*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   579
by (fast_tac (!claset addss (!simpset)) 2);
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   580
(*Fake*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   581
by (spy_analz_tac 1);
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   582
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   583
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   584
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   585
(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   586
  will stay secret.*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   587
goal thy
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   588
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   589
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   590
\            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   591
by (analz_induct_tac 1);   (*13 seconds*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   592
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   593
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   594
				      Says_imp_spies RS analz.Inj,
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   595
				      Notes_imp_spies RS analz.Inj]) 6));
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   596
(*ClientHello*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   597
by (Blast_tac 3);
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   598
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   599
by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   600
			       Says_imp_spies RS analz.Inj]) 2);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   601
(*Fake*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   602
by (spy_analz_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   603
(*ServerHello and ClientKeyExch: mostly freshness reasoning*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   604
by (REPEAT (blast_tac (!claset addSEs partsEs
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   605
			       addDs  [Notes_Crypt_parts_spies,
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   606
				       impOfSubs analz_subset_parts,
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   607
				       Says_imp_spies RS analz.Inj]) 1));
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   608
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   609
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   610
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   611
(*** Weakening the Oops conditions for leakage of clientK ***)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   612
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   613
(*If A created PMS then nobody other than the Spy would send a message
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   614
  using a clientK generated from that PMS.*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   615
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   616
 "!!evs. [| evs : tls;  A' ~= Spy |]                \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   617
\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   618
\      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   619
\      A = A'";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   620
by (analz_induct_tac 1);	(*8 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   621
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   622
(*ClientFinished, ClientResume: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   623
by (REPEAT 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   624
    (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   625
     	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   626
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   627
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   628
	               addSDs [Says_imp_spies RS parts.Inj]) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   629
bind_thm ("Says_clientK_unique",
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   630
	  result() RSN(2,rev_mp) RSN(2,rev_mp));
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   631
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   632
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   633
(*If A created PMS and has not leaked her clientK to the Spy, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   634
  then nobody has.*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   635
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   636
 "!!evs. evs : tls                         \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   637
\  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   638
\      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   639
\      (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   640
by (etac tls.induct 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   641
(*This roundabout proof sequence avoids looping in simplification*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   642
by (ALLGOALS Simp_tac);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   643
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   644
by (Fake_parts_insert_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   645
by (ALLGOALS Asm_simp_tac);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   646
(*Oops*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   647
by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   648
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   649
by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   650
			       spies_partsEs)) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   651
qed_spec_mp "clientK_Oops_ALL";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   652
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   653
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   654
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   655
(*** Weakening the Oops conditions for leakage of serverK ***)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   656
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   657
(*If A created PMS for B, then nobody other than B or the Spy would
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   658
  send a message using a serverK generated from that PMS.*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   659
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   660
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   661
\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   662
\      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   663
\      B = B'";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   664
by (analz_induct_tac 1);	(*9 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   665
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   666
(*ServerResume, ServerFinished: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   667
by (REPEAT
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   668
    (blast_tac (!claset addSEs [MPair_parts]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   669
		        addSDs [Notes_master_imp_Crypt_PMS, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   670
				Says_imp_spies RS parts.Inj]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   671
                        addDs  [Spy_not_see_PMS, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   672
				Notes_Crypt_parts_spies,
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   673
				Crypt_unique_PMS]) 2));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   674
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   675
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   676
	               addSDs [Says_imp_spies RS parts.Inj]) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   677
bind_thm ("Says_serverK_unique",
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   678
	  result() RSN(2,rev_mp) RSN(2,rev_mp));
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   679
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   680
(*If A created PMS for B, and B has not leaked his serverK to the Spy, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   681
  then nobody has.*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   682
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   683
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   684
\  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   685
\      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   686
\      (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   687
by (etac tls.induct 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   688
(*This roundabout proof sequence avoids looping in simplification*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   689
by (ALLGOALS Simp_tac);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   690
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   691
by (Fake_parts_insert_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   692
by (ALLGOALS Asm_simp_tac);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   693
(*Oops*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   694
by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   695
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   696
by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   697
			       spies_partsEs)) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   698
qed_spec_mp "serverK_Oops_ALL";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   699
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   700
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   701
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   702
(*** Protocol goals: if A receives ServerFinished, then B is present 
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   703
     and has used the quoted values PA, PB, etc.  Note that it is up to A
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   704
     to compare PA with what she originally sent.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   705
***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   706
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   707
(*The mention of her name (A) in X assures A that B knows who she is.*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   708
goal thy
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   709
 "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   710
\           X = Crypt (serverK(Na,Nb,M))                  \
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   711
\                 (Hash{|Nonce M, Number SID,             \
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   712
\                        Nonce Na, Number PA, Agent A,    \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   713
\                        Nonce Nb, Number PB, Agent B|}); \
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   714
\           M = PRF(PMS,NA,NB);                           \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   715
\           evs : tls;  A ~: bad;  B ~: bad |]          \
3676
cbaec955056b Addition of SessionIDs to the Hello and Finished messages
paulson
parents: 3672
diff changeset
   716
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   717
\        X : parts (spies evs) --> Says B A X : set evs";
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   718
by (etac rev_mp 1);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   719
by (hyp_subst_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   720
by (analz_induct_tac 1);        (*22 seconds*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   721
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   722
(*proves ServerResume*)
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   723
by (ALLGOALS Clarify_tac);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   724
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   725
by (fast_tac  (*blast_tac gives PROOF FAILED*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   726
    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   727
(*Fake: the Spy doesn't have the critical session key!*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   728
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   729
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   730
				     not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   731
by (Fake_parts_insert_tac 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   732
val lemma = normalize_thm [RSspec, RSmp] (result());
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   733
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   734
(*Final version*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   735
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   736
 "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   737
\                 (Hash{|Nonce M, Number SID,             \
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   738
\                        Nonce Na, Number PA, Agent A,    \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   739
\                        Nonce Nb, Number PB, Agent B|}); \
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   740
\           M = PRF(PMS,NA,NB);                           \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   741
\           X : parts (spies evs);                        \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   742
\           Notes A {|Agent B, Nonce PMS|} : set evs;     \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   743
\           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   744
\           evs : tls;  A ~: bad;  B ~: bad |]          \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   745
\        ==> Says B A X : set evs";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   746
by (blast_tac (!claset addIs [lemma]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   747
                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   748
qed_spec_mp "TrustServerFinished";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   749
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   750
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   751
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   752
(*This version refers not to ServerFinished but to any message from B.
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   753
  We don't assume B has received CertVerify, and an intruder could
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   754
  have changed A's identity in all other messages, so we can't be sure
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   755
  that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   756
  to bind A's identity with PMS, then we could replace A' by A below.*)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   757
goal thy
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   758
 "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   759
\           evs : tls;  A ~: bad;  B ~: bad;                 \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   760
\           M = PRF(PMS,NA,NB) |]            \
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   761
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   762
\            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   763
\            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   764
by (etac rev_mp 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   765
by (hyp_subst_tac 1);
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   766
by (analz_induct_tac 1);	(*20 seconds*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   767
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   768
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   769
(*ServerResume, ServerFinished: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   770
by (REPEAT
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   771
    (blast_tac (!claset addSEs [MPair_parts]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   772
		        addSDs [Notes_master_imp_Crypt_PMS, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   773
				Says_imp_spies RS parts.Inj]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   774
                        addDs  [Spy_not_see_PMS, 
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   775
				Notes_Crypt_parts_spies,
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   776
				Crypt_unique_PMS]) 3));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   777
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   778
by (blast_tac
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   779
    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   780
(*Fake: the Spy doesn't have the critical session key!*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   781
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   782
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   783
				     not_parts_not_analz]) 2);
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   784
by (Fake_parts_insert_tac 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   785
val lemma = normalize_thm [RSspec, RSmp] (result());
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   786
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   787
(*Final version*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   788
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   789
 "!!evs. [| M = PRF(PMS,NA,NB);                           \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   790
\           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   791
\           Notes A {|Agent B, Nonce PMS|} : set evs;     \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   792
\           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   793
\           evs : tls;  A ~: bad;  B ~: bad |]          \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   794
\        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   795
by (blast_tac (!claset addIs [lemma]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   796
                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   797
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   798
qed_spec_mp "TrustServerMsg";
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   799
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   800
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   801
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   802
(*** Protocol goal: if B receives any message encrypted with clientK
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   803
     then A has sent it, ASSUMING that A chose PMS.  Authentication is
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   804
     assumed here; B cannot verify it.  But if the message is
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   805
     ClientFinished, then B can then check the quoted values PA, PB, etc.
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   806
***)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   807
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   808
goal thy
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   809
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   810
\  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   811
\      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   812
\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   813
\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   814
by (analz_induct_tac 1);	(*15 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   815
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   816
(*ClientFinished, ClientResume: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   817
by (REPEAT (blast_tac (!claset delrules [conjI]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   818
		               addSDs [Notes_master_imp_Notes_PMS]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   819
	 	               addDs  [Notes_unique_PMS]) 3));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   820
(*ClientKeyExch*)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   821
by (fast_tac  (*blast_tac gives PROOF FAILED*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   822
    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   823
(*Fake: the Spy doesn't have the critical session key!*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   824
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   825
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   826
				     not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   827
by (Fake_parts_insert_tac 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   828
val lemma = normalize_thm [RSspec, RSmp] (result());
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   829
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   830
(*Final version*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   831
goal thy
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   832
 "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs);  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   833
\           Notes A {|Agent B, Nonce PMS|} : set evs;        \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   834
\           Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;  \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   835
\           evs : tls;  A ~: bad;  B ~: bad |]                         \
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   836
\  ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   837
by (blast_tac (!claset addIs [lemma]
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   838
                       addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   839
qed_spec_mp "TrustClientMsg";
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   840
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   841
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   842
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   843
(*** Protocol goal: if B receives ClientFinished, and if B is able to
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   844
     check a CertVerify from A, then A has used the quoted
3729
6be7cf5086ab Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents: 3711
diff changeset
   845
     values PA, PB, etc.  Even this one requires A to be uncompromised.
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   846
 ***)
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   847
goal thy
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   848
 "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   849
\           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   850
\           certificate A KA : parts (spies evs);       \
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   851
\           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   852
\             : set evs;                                                  \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   853
\        evs : tls;  A ~: bad;  B ~: bad |]                             \
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   854
\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   855
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   856
                       addDs  [Says_imp_spies RS parts.Inj]) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   857
qed "AuthClientFinished";
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   858
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   859
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   860
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   861
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)