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