src/HOL/Auth/TLS.ML
author paulson
Thu, 02 Jul 1998 17:48:11 +0200
changeset 5114 c729d4c299c1
parent 5076 fbc9d95b62ba
child 5223 4cb05273f764
permissions -rw-r--r--
Deleted leading parameters thanks to new Goal command
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
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
    20
open TLS;
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
    21
4449
wenzelm
parents: 4423
diff changeset
    22
set proof_timing;
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    23
HOL_quantifiers := false;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    24
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    25
(*Automatically unfold the definition of "certificate"*)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    26
Addsimps [certificate_def];
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    27
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    28
(*Injectiveness of key-generating functions*)
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    29
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
    30
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    31
(* invKey(sessionK x) = sessionK x*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    32
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
    33
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    34
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    35
(*** 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
    36
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4831
diff changeset
    37
Goal "pubK A ~= sessionK arg";
4423
a129b817b58a expandshort;
wenzelm
parents: 4422
diff changeset
    38
by (rtac notI 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    39
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    40
by (Full_simp_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    41
qed "pubK_neq_sessionK";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    42
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4831
diff changeset
    43
Goal "priK A ~= sessionK arg";
4423
a129b817b58a expandshort;
wenzelm
parents: 4422
diff changeset
    44
by (rtac notI 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    45
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    46
by (Full_simp_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    47
qed "priK_neq_sessionK";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    48
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
    49
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
    50
AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    51
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    52
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    53
(**** Protocol Proofs ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    54
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    55
(*Possibility properties state that some traces run the protocol to the end.
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    56
  Four paths and 12 rules are considered.*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    57
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    58
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    59
(** These proofs assume that the Nonce_supply nonces 
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    60
	(which have the form  @ N. Nonce N ~: used evs)
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    61
    lie outside the range of PRF.  It seems reasonable, but as it is needed
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
    62
    only for the possibility theorems, it is not taken as an axiom.
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    63
**)
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    64
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    65
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    66
(*Possibility property ending with ClientAccepts.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    67
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    68
\        A ~= B |]            \
3760
77f71f650433 Strengthened the possibility property for resumption so that it could have
paulson
parents: 3758
diff changeset
    69
\  ==> EX SID M. EX evs: tls.    \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    70
\     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
    71
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    72
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
    73
	  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
    74
	  tls.ClientAccepts) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    75
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    76
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    77
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    78
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
    79
(*And one for ServerAccepts.  Either FINISHED message may come first.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    80
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    81
\        A ~= B |]                        \
3760
77f71f650433 Strengthened the possibility property for resumption so that it could have
paulson
parents: 3758
diff changeset
    82
\  ==> EX SID NA PA NB PB M. EX evs: tls.    \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    83
\     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
    84
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    85
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
    86
	  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
    87
	  tls.ServerAccepts) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    88
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
    89
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    90
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    91
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    92
(*Another one, for CertVerify (which is optional)*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    93
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    94
\        A ~= B |]                       \
3760
77f71f650433 Strengthened the possibility property for resumption so that it could have
paulson
parents: 3758
diff changeset
    95
\  ==> 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
    96
\  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
    97
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
    98
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
    99
	  tls.ClientKeyExch RS tls.CertVerify) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   100
by possibility_tac;
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   101
by (REPEAT (Blast_tac 1));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   102
result();
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   103
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   104
(*Another one, for session resumption (both ServerResume and ClientResume) *)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   105
Goal "[| evs0 : tls;     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   106
\        Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   107
\        Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   108
\        ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   109
\        A ~= B |] ==> EX NA PA NB PB X. EX evs: tls.    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   110
\   X = Hash{|Number SID, Nonce M,             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   111
\                    Nonce NA, Number PA, Agent A,      \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   112
\                    Nonce NB, Number PB, Agent B|}  &  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   113
\   Says A B (Crypt (clientK(NA,NB,M)) X) : set evs  &  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   114
\   Says B A (Crypt (serverK(NA,NB,M)) X) : set evs";
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   115
by (REPEAT (resolve_tac [exI,bexI] 1));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   116
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
   117
	  tls.ClientResume) 2);
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   118
by possibility_tac;
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   119
by (REPEAT (Blast_tac 1));
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   120
result();
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   121
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   122
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   123
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   124
(**** Inductive proofs about tls ****)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   125
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   126
(*Nobody sends themselves messages*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   127
Goal "evs : tls ==> ALL A X. Says A A X ~: set evs";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   128
by (etac tls.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4472
diff changeset
   129
by Auto_tac;
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   130
qed_spec_mp "not_Says_to_self";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   131
Addsimps [not_Says_to_self];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   132
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   133
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   134
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   135
(*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
   136
   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
   137
   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
   138
fun parts_induct_tac i = 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   139
    etac tls.induct i
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   140
    THEN 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   141
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   142
    THEN 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   143
    fast_tac (claset() addss (simpset())) i THEN
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4556
diff changeset
   144
    ALLGOALS Asm_simp_tac;
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   145
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   146
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   147
(** 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
   148
    sends messages containing X! **)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   149
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   150
(*Spy never sees another agent's private key! (unless it's bad at start)*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   151
Goal "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
   152
by (parts_induct_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   153
by (Fake_parts_insert_tac 1);
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   154
qed "Spy_see_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   155
Addsimps [Spy_see_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   156
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   157
Goal "evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   158
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   159
qed "Spy_analz_priK";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   160
Addsimps [Spy_analz_priK];
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   161
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   162
AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   163
	Spy_analz_priK RSN (2, rev_iffD1)];
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   164
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   165
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   166
(*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
   167
  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
   168
  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
   169
  breach of security.*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4831
diff changeset
   170
Goalw [certificate_def]
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   171
 "[| certificate B KB : parts (spies evs);  evs : tls |]  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   172
\     ==> pubK B = KB";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   173
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   174
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   175
by (Fake_parts_insert_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   176
qed "certificate_valid";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   177
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   178
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   179
(*Replace key KB in ClientKeyExch by (pubK B) *)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   180
val ClientKeyExch_tac = 
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   181
    forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid]
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   182
    THEN' assume_tac
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   183
    THEN' hyp_subst_tac;
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   184
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   185
fun analz_induct_tac i = 
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   186
    etac tls.induct i   THEN
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   187
    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
   188
    ALLGOALS (asm_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   189
              (simpset() addcongs [if_weak_cong]
4831
dae4d63a1318 Renamed expand_const -> split_const.
nipkow
parents: 4719
diff changeset
   190
                         addsimps (split_ifs@pushes)))  THEN
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   191
    (*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
   192
      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
   193
    ALLGOALS (asm_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   194
              (simpset() addcongs [if_weak_cong]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4556
diff changeset
   195
			 addsimps [insert_absorb]));
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   196
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   197
3758
188a4fbfaf55 Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents: 3745
diff changeset
   198
(*** Properties of items found in Notes ***)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   199
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   200
Goal "[| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   201
\             ==> 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
   202
by (etac rev_mp 1);
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   203
by (analz_induct_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   204
by (blast_tac (claset() addIs [parts_insertI]) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3677
diff changeset
   205
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
   206
3758
188a4fbfaf55 Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents: 3745
diff changeset
   207
(*C may be either A or B*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   208
Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   209
\        evs : tls     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   210
\     |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   211
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   212
by (parts_induct_tac 1);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   213
by (ALLGOALS Clarify_tac);
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   214
(*Fake*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   215
by (blast_tac (claset() addIs [parts_insertI]) 1);
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   216
(*Client, Server Accept*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   217
by (REPEAT (blast_tac (claset() addSEs spies_partsEs
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   218
                                addSDs [Notes_Crypt_parts_spies]) 1));
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   219
qed "Notes_master_imp_Crypt_PMS";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   220
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   221
(*Compared with the theorem above, both premise and conclusion are stronger*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   222
Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   223
\        evs : tls     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   224
\     |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   225
by (etac rev_mp 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   226
by (parts_induct_tac 1);
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   227
(*ServerAccepts*)
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   228
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
   229
qed "Notes_master_imp_Notes_PMS";
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   230
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   231
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   232
(*** Protocol goal: if B receives CertVerify, then A sent it ***)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   233
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   234
(*B can check A's signature if he has received A's certificate.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   235
Goal "[| X : parts (spies evs);                          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   236
\        X = Crypt (priK A) (Hash{|nb, Agent B, pms|});  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   237
\        evs : tls;  A ~: bad |]                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   238
\ ==> Says A B X : set evs";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   239
by (etac rev_mp 1);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   240
by (hyp_subst_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   241
by (parts_induct_tac 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   242
by (Fake_parts_insert_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   243
val lemma = result();
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   244
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   245
(*Final version: B checks X using the distributed KA instead of priK A*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   246
Goal "[| X : parts (spies evs);                            \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   247
\        X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   248
\        certificate A KA : parts (spies evs);             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   249
\        evs : tls;  A ~: bad |]                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   250
\ ==> Says A B X : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   251
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   252
qed "TrustCertVerify";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   253
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   254
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   255
(*If CertVerify is present then A has chosen PMS.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   256
Goal "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   257
\          : parts (spies evs);                          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   258
\        evs : tls;  A ~: bad |]                         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   259
\     ==> Notes A {|Agent B, Nonce PMS|} : set evs";
4423
a129b817b58a expandshort;
wenzelm
parents: 4422
diff changeset
   260
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   261
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
diff changeset
   262
by (Fake_parts_insert_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   263
val lemma = result();
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   264
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   265
(*Final version using the distributed KA instead of priK A*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   266
Goal "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   267
\          : parts (spies evs);                             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   268
\        certificate A KA : parts (spies evs);              \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   269
\        evs : tls;  A ~: bad |]                            \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   270
\     ==> Notes A {|Agent B, Nonce PMS|} : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   271
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   272
qed "UseCertVerify";
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   273
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   274
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   275
Goal "evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   276
by (parts_induct_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   277
(*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
   278
by (Blast_tac 1);
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   279
qed "no_Notes_A_PRF";
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   280
Addsimps [no_Notes_A_PRF];
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   281
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   282
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   283
Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   284
\                evs : tls |]  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   285
\             ==> Nonce PMS : parts (spies evs)";
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   286
by (etac rev_mp 1);
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   287
by (parts_induct_tac 1);
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   288
by (Fake_parts_insert_tac 1);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   289
(*Six others, all trivial or by freshness*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   290
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   291
                                addSEs spies_partsEs) 1));
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   292
qed "MS_imp_PMS";
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   293
AddSDs [MS_imp_PMS];
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   294
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   295
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   296
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   297
(*** 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
   298
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   299
(*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   300
Goal "[| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   301
\     ==> EX B'. ALL B.   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   302
\           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
   303
by (etac rev_mp 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);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3515
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
(*ClientKeyExch*)
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   307
by (ClientKeyExch_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   308
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
   309
by (expand_case_tac "PMS = ?y" 1 THEN
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   310
    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
   311
val lemma = result();
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   312
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   313
Goal "[| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   314
\        Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   315
\        Nonce PMS ~: analz (spies evs);                 \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   316
\        evs : tls |]                                          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   317
\     ==> B=B'";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   318
by (prove_unique_tac lemma 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   319
qed "Crypt_unique_PMS";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   320
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   321
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   322
(** 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
   323
    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
   324
    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
   325
    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
   326
**)
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   327
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   328
(*In A's internal Note, PMS determines A and B.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   329
Goal "evs : tls               \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   330
\             ==> EX A' B'. ALL A B.  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   331
\                 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
   332
by (parts_induct_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   333
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
   334
(*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
   335
by (expand_case_tac "PMS = ?y" 1 THEN
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   336
    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
   337
val lemma = result();
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   338
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   339
Goal "[| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   340
\        Notes A' {|Agent B', Nonce PMS|} : set evs;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   341
\        evs : tls |]                               \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   342
\     ==> A=A' & B=B'";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   343
by (prove_unique_tac lemma 1);
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   344
qed "Notes_unique_PMS";
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   345
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   346
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   347
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   348
(**** Secrecy Theorems ****)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   349
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   350
(*Key compromise lemma needed to prove analz_image_keys.
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   351
  No collection of keys can help the spy get new private keys.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   352
Goal "evs : tls ==>                                      \
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   353
\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   354
\       (priK B : KK | B : bad)";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   355
by (etac tls.induct 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   356
by (ALLGOALS
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   357
    (asm_simp_tac (analz_image_keys_ss
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   358
		   addsimps (certificate_def::keys_distinct))));
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   359
(*Fake*) 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   360
by (spy_analz_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   361
qed_spec_mp "analz_image_priK";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   362
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   363
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   364
(*slightly speeds up the big simplification below*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   365
Goal "KK <= range sessionK ==> priK B ~: KK";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   366
by (Blast_tac 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   367
val range_sessionkeys_not_priK = result();
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   368
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   369
(*Lemma for the trivial direction of the if-and-only-if*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   370
Goal "(X : analz (G Un H)) --> (X : analz H)  ==> \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   371
\     (X : analz (G Un H))  =  (X : analz H)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   372
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   373
val analz_image_keys_lemma = result();
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   374
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   375
(** Strangely, the following version doesn't work:
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   376
\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   377
\        (Nonce N : analz (spies evs))";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   378
**)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   379
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   380
Goal "evs : tls ==>                                    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   381
\ ALL KK. KK <= range sessionK -->                     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   382
\         (Nonce N : analz (Key``KK Un (spies evs))) = \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   383
\         (Nonce N : analz (spies evs))";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   384
by (etac tls.induct 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   385
by (ClientKeyExch_tac 7);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   386
by (REPEAT_FIRST (resolve_tac [allI, impI]));
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   387
by (REPEAT_FIRST (rtac analz_image_keys_lemma));
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4831
diff changeset
   388
by (ALLGOALS    (*4.5 seconds*)
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   389
    (asm_simp_tac (analz_image_keys_ss 
4831
dae4d63a1318 Renamed expand_const -> split_const.
nipkow
parents: 4719
diff changeset
   390
		   addsimps (split_ifs@pushes)
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   391
		   addsimps [range_sessionkeys_not_priK, 
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   392
                             analz_image_priK, certificate_def])));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   393
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   394
(*Fake*) 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   395
by (spy_analz_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   396
qed_spec_mp "analz_image_keys";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   397
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   398
(*Knowing some session keys is no help in getting new nonces*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   399
Goal "evs : tls ==>          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   400
\     Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   401
\     (Nonce N : analz (spies evs))";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   402
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   403
qed "analz_insert_key";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   404
Addsimps [analz_insert_key];
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   405
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   406
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   407
(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   408
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   409
(** Some lemmas about session keys, comprising clientK and serverK **)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   410
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   411
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   412
(*Lemma: session keys are never used if PMS is fresh.  
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   413
  Nonces don't have to agree, allowing session resumption.
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   414
  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   415
  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   416
Goal "[| Nonce PMS ~: parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   417
\        K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   418
\        evs : tls |]             \
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   419
\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   420
by (etac rev_mp 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   421
by (hyp_subst_tac 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   422
by (analz_induct_tac 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   423
(*SpyKeys*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   424
by (blast_tac (claset() addSEs spies_partsEs) 3);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   425
(*Fake*)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   426
by (Fake_parts_insert_tac 2);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   427
(** LEVEL 6 **)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   428
(*Oops*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   429
by (fast_tac (claset() addSEs [MPair_parts]
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   430
		       addDs  [Says_imp_spies RS parts.Inj]
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   431
		       addss (simpset())) 6);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   432
by (REPEAT 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   433
    (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   434
				 Notes_master_imp_Crypt_PMS]
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   435
                         addSEs spies_partsEs) 1));
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   436
val lemma = result();
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   437
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   438
Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   439
\        evs : tls |]             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   440
\     ==> Nonce PMS : parts (spies evs)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   441
by (blast_tac (claset() addDs [lemma]) 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   442
qed "PMS_sessionK_not_spied";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   443
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   444
Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   445
\          : parts (spies evs);  evs : tls |]             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   446
\     ==> Nonce PMS : parts (spies evs)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   447
by (blast_tac (claset() addDs [lemma]) 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   448
qed "PMS_Crypt_sessionK_not_spied";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   449
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   450
(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   451
  Converse doesn't hold; betraying M doesn't force the keys to be sent!
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   452
  The strong Oops condition can be weakened later by unicity reasoning, 
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   453
	with some effort.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   454
Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   455
\        Nonce M ~: analz (spies evs);  evs : tls |]   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   456
\     ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   457
by (etac rev_mp 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   458
by (etac rev_mp 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   459
by (analz_induct_tac 1);        (*17 seconds*)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   460
(*SpyKeys*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   461
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   462
(*Fake*) 
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   463
by (spy_analz_tac 2);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   464
(*Base*)
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   465
by (Blast_tac 1);
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   466
qed "sessionK_not_spied";
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   467
Addsimps [sessionK_not_spied];
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   468
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   469
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   470
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   471
Goal "[| evs : tls;  A ~: bad;  B ~: bad |]           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   472
\     ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   473
\         Nonce PMS ~: analz (spies evs)";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   474
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
   475
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   476
by (REPEAT (fast_tac (claset() addss (simpset())) 6));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   477
(*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   478
  mostly freshness reasoning*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   479
by (REPEAT (blast_tac (claset() addSEs partsEs
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   480
				addDs  [Notes_Crypt_parts_spies,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   481
					impOfSubs analz_subset_parts,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   482
					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
   483
(*SpyKeys*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   484
by (fast_tac (claset() addss (simpset())) 2);
3677
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   485
(*Fake*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   486
by (spy_analz_tac 1);
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   487
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
   488
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   489
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   490
(*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
   491
  will stay secret.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   492
Goal "[| evs : tls;  A ~: bad;  B ~: bad |]           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   493
\     ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   494
\         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
   495
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
   496
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   497
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   498
				       Says_imp_spies RS analz.Inj,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   499
				       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
   500
(*ClientHello*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   501
by (Blast_tac 3);
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   502
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   503
by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   504
				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
   505
(*Fake*)
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   506
by (spy_analz_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   507
(*ServerHello and ClientKeyExch: mostly freshness reasoning*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   508
by (REPEAT (blast_tac (claset() addSEs partsEs
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   509
				addDs  [Notes_Crypt_parts_spies,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   510
					impOfSubs analz_subset_parts,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   511
					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
   512
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
   513
f2569416d18b Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents: 3676
diff changeset
   514
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   515
(*** Weakening the Oops conditions for leakage of clientK ***)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   516
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   517
(*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
   518
  using a clientK generated from that PMS.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   519
Goal "[| evs : tls;  A' ~= Spy |]                \
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   520
\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   521
\   Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   522
\   A = A'";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   523
by (analz_induct_tac 1);	(*8 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   524
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   525
(*ClientFinished, ClientResume: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   526
by (REPEAT 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   527
    (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   528
     	 	         addIs  [Notes_unique_PMS RS conjunct1]) 2));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   529
(*ClientKeyExch*)
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   530
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied,
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   531
				Says_imp_spies RS parts.Inj]) 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   532
bind_thm ("Says_clientK_unique",
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   533
	  result() RSN(2,rev_mp) RSN(2,rev_mp));
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   534
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   535
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   536
(*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
   537
  then nobody has.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   538
Goal "evs : tls                         \
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   539
\  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   540
\   Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   541
\   (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   542
by (etac tls.induct 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   543
(*This roundabout proof sequence avoids looping in simplification*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   544
by (ALLGOALS Simp_tac);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   545
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   546
by (Fake_parts_insert_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   547
by (ALLGOALS Asm_simp_tac);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   548
(*Oops*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   549
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
   550
(*ClientKeyExch*)
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   551
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   552
			addSEs spies_partsEs) 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   553
qed_spec_mp "clientK_Oops_ALL";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   554
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   555
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   556
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   557
(*** Weakening the Oops conditions for leakage of serverK ***)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   558
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   559
(*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
   560
  send a message using a serverK generated from that PMS.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   561
Goal "[| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   562
\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   563
\   Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   564
\   B = B'";
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   565
by (analz_induct_tac 1);	(*9 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   566
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   567
(*ServerResume, ServerFinished: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   568
by (REPEAT
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   569
    (blast_tac (claset() addSEs [MPair_parts]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   570
			 addSDs [Notes_master_imp_Crypt_PMS, 
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   571
				 Says_imp_spies RS parts.Inj]
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   572
			 addDs  [Spy_not_see_PMS, 
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   573
				 Notes_Crypt_parts_spies,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   574
				 Crypt_unique_PMS]) 2));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   575
(*ClientKeyExch*)
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   576
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied,
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   577
				Says_imp_spies RS parts.Inj]) 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   578
bind_thm ("Says_serverK_unique",
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   579
	  result() RSN(2,rev_mp) RSN(2,rev_mp));
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   580
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   581
(*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
   582
  then nobody has.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   583
Goal "[| evs : tls;  A ~: bad;  B ~: bad |]                        \
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   584
\  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   585
\   Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   586
\   (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   587
by (etac tls.induct 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   588
(*This roundabout proof sequence avoids looping in simplification*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   589
by (ALLGOALS Simp_tac);
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   590
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   591
by (Fake_parts_insert_tac 1);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   592
by (ALLGOALS Asm_simp_tac);
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   593
(*Oops*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   594
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
   595
(*ClientKeyExch*)
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   596
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   597
			addSEs spies_partsEs) 1);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   598
qed_spec_mp "serverK_Oops_ALL";
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   599
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   600
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   601
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   602
(*** 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
   603
     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
   604
     to compare PA with what she originally sent.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   605
***)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   606
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   607
(*The mention of her name (A) in X assures A that B knows who she is.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   608
Goal "[| X = Crypt (serverK(Na,Nb,M))                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   609
\              (Hash{|Number SID, Nonce M,             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   610
\                     Nonce Na, Number PA, Agent A,    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   611
\                     Nonce Nb, Number PB, Agent B|}); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   612
\        M = PRF(PMS,NA,NB);                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   613
\        evs : tls;  A ~: bad;  B ~: bad |]            \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   614
\     ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   615
\         Notes A {|Agent B, Nonce PMS|} : set evs --> \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   616
\         X : parts (spies evs) --> Says B A X : set evs";
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   617
by (hyp_subst_tac 1);
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   618
by (analz_induct_tac 1);        (*10 seconds*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   619
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   620
by (ALLGOALS Clarify_tac);
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   621
(*ClientKeyExch*)
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   622
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   623
(*Fake: the Spy doesn't have the critical session key!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   624
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   625
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   626
				      not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   627
by (Fake_parts_insert_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   628
val lemma = normalize_thm [RSmp] (result());
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   629
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   630
(*Final version*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   631
Goal "[| X = Crypt (serverK(Na,Nb,M))                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   632
\              (Hash{|Number SID, Nonce M,             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   633
\                     Nonce Na, Number PA, Agent A,    \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   634
\                     Nonce Nb, Number PB, Agent B|}); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   635
\        M = PRF(PMS,NA,NB);                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   636
\        X : parts (spies evs);                        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   637
\        Notes A {|Agent B, Nonce PMS|} : set evs;     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   638
\        Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   639
\        evs : tls;  A ~: bad;  B ~: bad |]          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   640
\     ==> Says B A X : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   641
by (blast_tac (claset() addIs [lemma]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   642
                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   643
qed_spec_mp "TrustServerFinished";
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   644
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   645
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   646
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   647
(*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
   648
  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
   649
  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
   650
  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
   651
  to bind A's identity with PMS, then we could replace A' by A below.*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   652
Goal "[| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   653
\     ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   654
\         Notes A {|Agent B, Nonce PMS|} : set evs -->              \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   655
\         Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   656
\         (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
3672
56e4365a0c99 TLS now with a distinction between premaster secret and master secret
paulson
parents: 3519
diff changeset
   657
by (hyp_subst_tac 1);
3686
4b484805b4c4 First working version with Oops event for session keys
paulson
parents: 3685
diff changeset
   658
by (analz_induct_tac 1);	(*20 seconds*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   659
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   660
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   661
(*ServerResume, ServerFinished: by unicity of PMS*)
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   662
by (REPEAT
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   663
    (blast_tac (claset() addSEs [MPair_parts]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   664
			 addSDs [Notes_master_imp_Crypt_PMS, 
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   665
				 Says_imp_spies RS parts.Inj]
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   666
			 addDs  [Spy_not_see_PMS, 
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   667
				 Notes_Crypt_parts_spies,
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   668
				 Crypt_unique_PMS]) 3));
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   669
(*ClientKeyExch*)
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   670
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   671
(*Fake: the Spy doesn't have the critical session key!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   672
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   673
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   674
				      not_parts_not_analz]) 2);
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   675
by (Fake_parts_insert_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   676
val lemma = normalize_thm [RSmp] (result());
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   677
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   678
(*Final version*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   679
Goal "[| M = PRF(PMS,NA,NB);                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   680
\        Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   681
\        Notes A {|Agent B, Nonce PMS|} : set evs;     \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   682
\        Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   683
\        evs : tls;  A ~: bad;  B ~: bad |]          \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   684
\     ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   685
by (blast_tac (claset() addIs [lemma]
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   686
                        addEs [serverK_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
   687
qed_spec_mp "TrustServerMsg";
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   688
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   689
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   690
3515
d8a71f6eaf40 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents: 3506
diff changeset
   691
(*** 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
   692
     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
   693
     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
   694
     ClientFinished, then B can then check the quoted values PA, PB, etc.
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   695
***)
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   696
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   697
Goal "[| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   698
\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   699
\     Notes A {|Agent B, Nonce PMS|} : set evs -->               \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   700
\     Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   701
\     Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   702
by (hyp_subst_tac 1);
3745
4c5d3b1ddc75 Client, Server certificates now sent using the separate Certificate rule,
paulson
parents: 3729
diff changeset
   703
by (analz_induct_tac 1);	(*15 seconds*)
3711
2f86b403d975 Deleted an obsolete step in TrustServerFinished
paulson
parents: 3704
diff changeset
   704
by (ALLGOALS Clarify_tac);
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   705
(*ClientFinished, ClientResume: by unicity of PMS*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   706
by (REPEAT (blast_tac (claset() delrules [conjI]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   707
		                addSDs [Notes_master_imp_Notes_PMS]
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   708
	 	                addDs  [Notes_unique_PMS]) 3));
4472
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   709
(*ClientKeyExch*)
cfa3bd184bc1 Tidied using rev_iffD1, etc
paulson
parents: 4449
diff changeset
   710
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
   711
(*Fake: the Spy doesn't have the critical session key!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   712
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   713
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4201
diff changeset
   714
				      not_parts_not_analz]) 2);
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   715
by (Fake_parts_insert_tac 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   716
val lemma = normalize_thm [RSmp] (result());
3704
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   717
2f99d7a0dccc sessionK now indexed by nat instead of bool.
paulson
parents: 3687
diff changeset
   718
(*Final version*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   719
Goal "[| M = PRF(PMS,NA,NB);                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   720
\        Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   721
\        Notes A {|Agent B, Nonce PMS|} : set evs;        \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   722
\        Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   723
\        evs : tls;  A ~: bad;  B ~: bad |]                         \
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   724
\  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   725
by (blast_tac (claset() addIs [lemma]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   726
                        addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
3772
6ee707a73248 Routine tidying up
paulson
parents: 3760
diff changeset
   727
qed "TrustClientMsg";
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   728
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   729
3685
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   730
5b8c0c8f576e Full version of TLS including session resumption, but no Oops
paulson
parents: 3683
diff changeset
   731
(*** 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
   732
     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
   733
     values PA, PB, etc.  Even this one requires A to be uncompromised.
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   734
 ***)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   735
Goal "[| M = PRF(PMS,NA,NB);                           \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   736
\        Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   737
\        Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   738
\        certificate A KA : parts (spies evs);       \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   739
\        Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   740
\          : set evs;                                                  \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   741
\     evs : tls;  A ~: bad;  B ~: bad |]                             \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
   742
\  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 4006
diff changeset
   743
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify]
4201
858b3ec2c9db Fixed indentation
paulson
parents: 4091
diff changeset
   744
                        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
   745
qed "AuthClientFinished";
3687
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   746
fb7d096d7884 Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents: 3686
diff changeset
   747
(*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
   748
(*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
   749
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
3758
188a4fbfaf55 Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents: 3745
diff changeset
   750
(*30/9/97: loads in 476s, after removing unused theorems*)
3760
77f71f650433 Strengthened the possibility property for resumption so that it could have
paulson
parents: 3758
diff changeset
   751
(*30/9/97: loads in 448s, after fixing ServerResume*)