--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/TLS.ML Tue Jul 01 11:11:42 1997 +0200
@@ -0,0 +1,369 @@
+(* Title: HOL/Auth/TLS
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+The public-key model has a weakness, especially concerning anonymous sessions.
+The Spy's state is recorded as the trace of message. But if he himself is
+the Client and invents M, then the event he sends contains M encrypted with B's
+public key. From the trace there is no reason to believe that the spy knows
+M, and yet the spy actually chose M! So, in any property concerning the
+secrecy of some item, one must somehow establish that the spy didn't choose
+the item. In practice, this weakness does little harm, since one can expect
+few guarantees when communicating directly with an enemy.
+
+The model, at present, doesn't recognize that if the Spy has NA, NB and M then
+he also has clientK(NA,NB,M) and serverK(NA,NB,M). Maybe this doesn't really
+matter, since one can prove that he doesn't get M.
+*)
+
+open TLS;
+
+proof_timing:=true;
+HOL_quantifiers := false;
+
+AddIffs [Spy_in_lost, Server_not_lost];
+
+(*Injectiveness of key-generating functions*)
+AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
+
+(* invKey(clientK x) = clientK x and similarly for serverK*)
+Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
+ isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
+
+
+(*Replacing the variable by a constant improves search speed by 50%!*)
+val Says_imp_sees_Spy' =
+ read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
+
+
+(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
+
+goal thy "pubK A ~= clientK arg";
+br notI 1;
+by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
+by (Full_simp_tac 1);
+qed "pubK_neq_clientK";
+
+goal thy "pubK A ~= serverK arg";
+br notI 1;
+by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
+by (Full_simp_tac 1);
+qed "pubK_neq_serverK";
+
+goal thy "priK A ~= clientK arg";
+br notI 1;
+by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
+by (Full_simp_tac 1);
+qed "priK_neq_clientK";
+
+goal thy "priK A ~= serverK arg";
+br notI 1;
+by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
+by (Full_simp_tac 1);
+qed "priK_neq_serverK";
+
+val ths = [pubK_neq_clientK, pubK_neq_serverK,
+ priK_neq_clientK, priK_neq_serverK];
+AddIffs (ths @ (ths RL [not_sym]));
+
+
+(**** Protocol Proofs ****)
+
+(*A "possibility property": there are traces that reach the end.
+ This protocol has three end points and six messages to consider.*)
+
+(*Possibility property ending with ServerFinished.*)
+goal thy
+ "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
+\ Says B A (Crypt (serverK(NA,NB,M)) \
+\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
+\ Nonce NA, Agent XA, Agent A, \
+\ Nonce NB, Agent XB, \
+\ Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
+\ : set evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
+ RS tls.ServerFinished) 2);
+by possibility_tac;
+result();
+
+(*And one for ClientFinished. Either FINISHED message may come first.*)
+goal thy
+ "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \
+\ Says A B (Crypt (clientK(NA,NB,M)) \
+\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
+\ Nonce NA, Agent XA, \
+\ Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
+\ Nonce NB, Agent XB, Agent B|})) : set evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
+ RS tls.ClientFinished) 2);
+by possibility_tac;
+result();
+
+(*Another one, for CertVerify (which is optional)*)
+goal thy
+ "!!A B. A ~= B ==> EX NB. EX evs: tls. \
+\ Says A B (Crypt (priK A) \
+\ (Hash{|Nonce NB, \
+\ Crypt (priK Server) \
+\ {|Agent B, Key (pubK B)|}|})) : set evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
+by possibility_tac;
+result();
+
+
+(**** Inductive proofs about tls ****)
+
+(*Nobody sends themselves messages*)
+goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
+by (etac tls.induct 1);
+by (Auto_tac());
+qed_spec_mp "not_Says_to_self";
+Addsimps [not_Says_to_self];
+AddSEs [not_Says_to_self RSN (2, rev_notE)];
+
+
+(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees another agent's private key! (unless it's lost at start)*)
+goal thy
+ "!!evs. evs : tls \
+\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
+by (etac tls.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
+qed "Spy_see_priK";
+Addsimps [Spy_see_priK];
+
+goal thy
+ "!!evs. evs : tls \
+\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
+by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+qed "Spy_analz_priK";
+Addsimps [Spy_analz_priK];
+
+goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \
+\ evs : tls |] ==> A:lost";
+by (blast_tac (!claset addDs [Spy_see_priK]) 1);
+qed "Spy_see_priK_D";
+
+bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
+AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
+
+
+(*Every Nonce that's hashed is already in past traffic. *)
+goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs); \
+\ evs : tls |] \
+\ ==> Nonce N : parts (sees lost Spy evs)";
+by (etac rev_mp 1);
+by (etac tls.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs partsEs) 1);
+by (Fake_parts_insert_tac 1);
+qed "Hash_imp_Nonce1";
+
+(*Lemma needed to prove Hash_Hash_imp_Nonce*)
+goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|} \
+\ : parts (sees lost Spy evs); \
+\ evs : tls |] \
+\ ==> Nonce M : parts (sees lost Spy evs)";
+by (etac rev_mp 1);
+by (etac tls.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs partsEs) 1);
+by (Fake_parts_insert_tac 1);
+qed "Hash_imp_Nonce2";
+AddSDs [Hash_imp_Nonce2];
+
+goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \
+\ : parts (sees lost Spy evs); \
+\ evs : tls |] \
+\ ==> Nonce M : parts (sees lost Spy evs)";
+by (etac rev_mp 1);
+by (etac tls.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs partsEs) 1);
+by (Fake_parts_insert_tac 1);
+qed "Hash_Hash_imp_Nonce";
+
+
+(*NEEDED??
+ Every Nonce that's hashed is already in past traffic.
+ This general formulation is tricky to prove and hard to use, since the
+ 2nd premise is typically proved by simplification.*)
+goal thy "!!evs. [| Hash X : parts (sees lost Spy evs); \
+\ Nonce N : parts {X}; evs : tls |] \
+\ ==> Nonce N : parts (sees lost Spy evs)";
+by (etac rev_mp 1);
+by (etac tls.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSEs partsEs) 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
+(*ServerFinished*)
+by (Blast_tac 3);
+(*ClientFinished*)
+by (Blast_tac 2);
+by (Fake_parts_insert_tac 1);
+qed "Hash_imp_Nonce_seen";
+
+
+(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
+
+(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
+ message is Fake. We don't need guarantees for the Spy anyway.*)
+goal thy
+ "!!evs. [| X = Crypt (priK A) \
+\ (Hash{|Nonce NB, \
+\ Crypt (priK Server) {|Agent B, Key KB|}|}); \
+\ evs : tls; A ~: lost; B ~= Spy |] \
+\ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, \
+\ Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
+\ X : parts (sees lost Spy evs) --> Says A B X : set evs";
+by (Asm_simp_tac 1);
+by (etac tls.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fake_parts_insert_tac 1);
+(*ServerHello*)
+by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
+ addSEs sees_Spy_partsEs) 1);
+qed_spec_mp "TrustCertVerify";
+
+
+(*This lemma says that no false certificates exist. One might extend the
+ model to include bogus certificates for the lost agents, but there seems
+ little point in doing so: the loss of their private keys is a worse
+ breach of security.*)
+goal thy
+ "!!evs. evs : tls \
+\ ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
+\ --> KB = pubK B";
+by (etac tls.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fake_parts_insert_tac 2);
+by (Blast_tac 1);
+bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
+
+
+(*Replace key KB in ClientCertKeyEx by (pubK B) *)
+val ClientCertKeyEx_tac =
+ forward_tac [Says_imp_sees_Spy' RS parts.Inj RS
+ parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
+ THEN' assume_tac
+ THEN' hyp_subst_tac;
+
+fun analz_induct_tac i =
+ etac tls.induct i THEN
+ ClientCertKeyEx_tac (i+4) THEN
+ ALLGOALS (asm_simp_tac
+ (!simpset addsimps [not_parts_not_analz]
+ setloop split_tac [expand_if])) THEN
+ (*Remove instances of pubK B: the Spy already knows all public keys.
+ Combining the two simplifier calls makes them run extremely slowly.*)
+ ALLGOALS (asm_simp_tac
+ (!simpset addsimps [insert_absorb]
+ setloop split_tac [expand_if]));
+
+(*If A sends ClientCertKeyEx to an honest agent B, then M will stay secret.*)
+goal thy
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost |] ==> \
+\ Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
+\ Crypt KB (Nonce M)|} : set evs --> \
+\ Nonce M ~: analz (sees lost Spy evs)";
+by (analz_induct_tac 1);
+(*ClientHello*)
+by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+by (REPEAT (blast_tac (!claset addSEs partsEs
+ addDs [impOfSubs analz_subset_parts,
+ Says_imp_sees_Spy' RS analz.Inj]) 1));
+bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
+
+
+(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
+
+(*In fact, nothing of the form clientK(NA,NB,M) or serverK(NA,NB,M) is ever
+ sent! These two theorems are too strong: the Spy is quite capable of
+ forming many items of the form serverK(NA,NB,M).
+ Additional Fake rules could model this capability.*)
+
+goal thy
+ "!!evs. evs : tls ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+by (etac tls.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
+qed "clientK_notin_parts";
+
+goal thy
+ "!!evs. evs : tls ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
+by (etac tls.induct 1);
+by (prove_simple_subgoals_tac 1);
+by (Fake_parts_insert_tac 1);
+qed "serverK_notin_parts";
+
+(*We need a version of AddIffs that takes CONDITIONAL equivalences*)
+val ths = [clientK_notin_parts, clientK_notin_parts RS not_parts_not_analz,
+ serverK_notin_parts, serverK_notin_parts RS not_parts_not_analz];
+Addsimps ths;
+AddSEs (ths RLN (2, [rev_notE]));
+
+
+(*** Protocol goals: if A receives SERVER FINISHED, then B is present
+ and has used the quoted values XA, XB, etc. Note that it is up to A
+ to compare XA with what she originally sent.
+***)
+
+(*Perhaps A~=Spy is unnecessary, but there's no obvious proof if the first
+ message is Fake. We don't need guarantees for the Spy anyway.*)
+goal thy
+ "!!evs. [| X = Crypt (serverK(NA,NB,M)) \
+\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
+\ Nonce NA, Agent XA, Agent A, \
+\ Nonce NB, Agent XB, \
+\ Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
+\ evs : tls; A~=Spy; B ~: lost |] ==> \
+\ Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
+\ Crypt KB (Nonce M)|} : set evs --> \
+\ X : parts (sees lost Spy evs) --> Says B A X : set evs";
+by (Asm_simp_tac 1);
+by (etac tls.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fake_parts_insert_tac 1);
+(*ClientCertKeyEx*)
+by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
+ addSEs sees_Spy_partsEs) 1);
+qed_spec_mp "TrustServerFinished";
+
+
+(*** Protocol goal: if B receives CLIENT FINISHED, then A is present ??
+ and has used the quoted values XA, XB, etc. Note that it is up to B
+ to compare XB with what he originally sent. ***)
+
+(*This result seems far too strong--it may be provable because the current
+ model gives the Spy access to NO keys of the form clientK(NA,NB,M).*)
+goal thy
+ "!!evs. [| X = Crypt (clientK(NA,NB,M)) \
+\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
+\ Nonce NA, Agent XA, \
+\ Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
+\ Nonce NB, Agent XB, Agent B|}); \
+\ evs : tls |] ==> \
+\ X : parts (sees lost Spy evs) --> Says A B X : set evs";
+by (Asm_simp_tac 1);
+by (etac tls.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by (Fake_parts_insert_tac 1);
+qed_spec_mp "TrustClientFinished";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/TLS.thy Tue Jul 01 11:11:42 1997 +0200
@@ -0,0 +1,141 @@
+(* Title: HOL/Auth/TLS
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
+
+An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
+to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
+global signing authority.
+
+A is the client and B is the server, not to be confused with the constant
+Server, who is in charge of all public keys.
+
+The model assumes that no fraudulent certificates are present.
+
+Protocol goals:
+* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
+ parties (though A is not necessarily authenticated).
+
+* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
+ message is optional!)
+
+* A upon receiving SERVER FINISHED knows that B is present
+
+* Each party who has received a FINISHED message can trust that the other
+ party agrees on all message components, including XA and XB (thus foiling
+ rollback attacks).
+*)
+
+TLS = Public +
+
+consts
+ (*Client, server write keys. They implicitly include the MAC secrets.*)
+ clientK, serverK :: "nat*nat*nat => key"
+
+rules
+ (*clientK is collision-free and makes symmetric keys*)
+ inj_clientK "inj clientK"
+ isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*)
+
+ inj_serverK "inj serverK"
+ isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*)
+
+ (*Spy has access to his own key for spoof messages, but Server is secure*)
+ Spy_in_lost "Spy: lost"
+ Server_not_lost "Server ~: lost"
+
+
+consts lost :: agent set (*No need for it to be a variable*)
+ tls :: event list set
+
+inductive tls
+ intrs
+ Nil (*Initial trace is empty*)
+ "[]: tls"
+
+ Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
+ "[| evs: tls; B ~= Spy;
+ X: synth (analz (sees lost Spy evs)) |]
+ ==> Says Spy B X # evs : tls"
+
+ ClientHello
+ (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+ It is uninterpreted but will be confirmed in the FINISHED messages.
+ As an initial simplification, SESSION_ID is identified with NA
+ and reuse of sessions is not supported.*)
+ "[| evs: tls; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs : tls"
+
+ ServerHello
+ (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+ Na is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is
+ implied and a SERVER CERTIFICATE is always present.*)
+ "[| evs: tls; A ~= B; Nonce NB ~: used evs;
+ Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
+ ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
+ # evs : tls"
+
+ ClientCertKeyEx
+ (*CLIENT CERTIFICATE and KEY EXCHANGE. M is the pre-master-secret.
+ Note that A encrypts using the supplied KB, not pubK B.*)
+ "[| evs: tls; A ~= B; Nonce M ~: used evs;
+ Says B' A {|Nonce NA, Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
+ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
+ Crypt KB (Nonce M)|}
+ # evs : tls"
+
+ CertVerify
+ (*The optional CERTIFICATE VERIFY message contains the specific
+ components listed in the security analysis, Appendix F.1.1.2.
+ By checking the signature, B is assured of A's existence:
+ the only use of A's certificate.*)
+ "[| evs: tls; A ~= B;
+ Says B' A {|Nonce NA, Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
+ ==> Says A B (Crypt (priK A)
+ (Hash{|Nonce NB,
+ Crypt (priK Server) {|Agent B, Key KB|}|}))
+ # evs : tls"
+
+ (*Finally come the FINISHED messages, confirming XA and XB among
+ other things. The master-secret is the hash of NA, NB and M.
+ Either party may sent its message first.*)
+
+ ClientFinished
+ "[| evs: tls; A ~= B;
+ Says A B {|Agent A, Nonce NA, Agent XA|} : set evs;
+ Says B' A {|Nonce NA, Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
+ Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
+ Crypt KB (Nonce M)|} : set evs |]
+ ==> Says A B (Crypt (clientK(NA,NB,M))
+ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
+ Nonce NA, Agent XA,
+ Crypt (priK Server) {|Agent A, Key(pubK A)|},
+ Nonce NB, Agent XB, Agent B|}))
+ # evs : tls"
+
+ (*Keeping A' and A'' distinct means B cannot even check that the
+ two messages originate from the same source.*)
+
+ ServerFinished
+ "[| evs: tls; A ~= B;
+ Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs;
+ Says B A {|Nonce NA, Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
+ : set evs;
+ Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
+ ==> Says B A (Crypt (serverK(NA,NB,M))
+ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
+ Nonce NA, Agent XA, Agent A,
+ Nonce NB, Agent XB,
+ Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
+ # evs : tls"
+
+ (**Oops message??**)
+
+end