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