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