# HG changeset patch # User paulson # Date 868030495 -7200 # Node ID 0d8ad2f192d8f55816aa3bcc1d6a2f87afa09ba5 # Parent ce1664057431f6c4731f7de2d07d7f88d4ab7b84 New constant "certificate"--just an abbreviation diff -r ce1664057431 -r 0d8ad2f192d8 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Jul 04 14:37:30 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Fri Jul 04 17:34:55 1997 +0200 @@ -5,11 +5,12 @@ 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 he sends contains M encrypted with B's public key. -This message gives no evidence that the spy knows M, and yet the spy actually -chose M! So, in any property concerning the secrecy of some item, one must -establish that the spy didn't choose the item. Guarantees normally assume -that the other party is uncompromised (otherwise, one can prove little). +Client and invents M, then he encrypts M with B's public key before sending +it. This message gives no evidence that the spy knows M, and yet the spy +actually chose M! So, in any property concerning the secrecy of some item, +one must establish that the spy didn't choose the item. Guarantees normally +assume that the other party is uncompromised (otherwise, one can prove +little). Protocol goals: * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two @@ -23,17 +24,6 @@ * 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). - -A curious property found in these proofs is that CERTIFICATE VERIFY actually -gives weaker authentication than CLIENT FINISHED. The theorem for CERTIFICATE -VERIFY is subject to A~:lost, since if A's private key is known to the spy -then he can forge A's signature. But the theorem for CLIENT FINISHED merely -assumes that A is not the spy himself, since the model assumes that all other -agents tell the truth. - -In the real world, there are agents who are not active attackers, and yet -still cannot be trusted to identify themselves. There may well be more such -agents than there are compromised private keys. *) open TLS; @@ -42,6 +32,7 @@ HOL_quantifiers := false; AddIffs [Spy_in_lost, Server_not_lost]; +Addsimps [certificate_def]; goal thy "!!A. A ~: lost ==> A ~= Spy"; by (Blast_tac 1); @@ -110,7 +101,7 @@ \ (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)|}|})) \ +\ certificate B (pubK B)|})) \ \ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx @@ -124,7 +115,7 @@ \ 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)|}, \ +\ certificate A (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 @@ -136,9 +127,7 @@ 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"; +\ (Hash{|Nonce NB, certificate B (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; @@ -250,13 +239,13 @@ (*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. We must assume A~:lost; otherwise, the Spy can forge A's signature.*) -goal thy +goalw thy [certificate_def] "!!evs. [| X = Crypt (priK A) \ \ (Hash{|Nonce NB, \ -\ Crypt (priK Server) {|Agent B, Key KB|}|}); \ +\ certificate B 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 --> \ +\ certificate B KB|} : set evs --> \ \ X : parts (sees lost Spy evs) --> Says A B X : set evs"; by (hyp_subst_tac 1); by (etac tls.induct 1); @@ -272,9 +261,9 @@ 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 +goalw thy [certificate_def] "!!evs. evs : tls \ -\ ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \ +\ ==> certificate B KB : parts (sees lost Spy evs) \ \ --> KB = pubK B"; by (etac tls.induct 1); by (ALLGOALS Asm_simp_tac); @@ -369,9 +358,9 @@ (*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret. The assumption is A~=Spy, not A~:lost, since A doesn't use her private key here.*) -goal thy +goalw thy [certificate_def] "!!evs. [| evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ ==> Says A B {|certificate A (pubK A), \ \ Crypt KB (Nonce M)|} : set evs --> \ \ Nonce M ~: analz (sees lost Spy evs)"; by (analz_induct_tac 1); @@ -427,14 +416,14 @@ to compare XA with what she originally sent. ***) -goal thy +goalw thy [certificate_def] "!!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)|}|}); \ +\ certificate B (pubK B)|}); \ \ evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ ==> Says A B {|certificate A (pubK A), \ \ Crypt KB (Nonce M)|} : set evs --> \ \ X : parts (sees lost Spy evs) --> Says B A X : set evs"; by (hyp_subst_tac 1); @@ -453,20 +442,18 @@ 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 too strong: A need not have sent CERTIFICATE VERIFY. - But we assume (as always) that the other party is honest...*) -goal thy +(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the + quoted values XA, XB, etc., which B can then check. BUT NOTE: + B has no way of knowing that A is the sender of CERTIFICATE VERIFY + ***) +goalw thy [certificate_def] "!!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)|}, \ +\ certificate A (pubK A), \ \ Nonce NB, Agent XB, Agent B|}); \ \ evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ ==> Says A B {|certificate A (pubK A), \ \ Crypt KB (Nonce M)|} : set evs --> \ \ X : parts (sees lost Spy evs) --> Says A B X : set evs"; by (hyp_subst_tac 1); diff -r ce1664057431 -r 0d8ad2f192d8 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Fri Jul 04 14:37:30 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Fri Jul 04 17:34:55 1997 +0200 @@ -18,6 +18,13 @@ Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher Allen, Transport Layer Security Working Group, 21 May 1997, INTERNET-DRAFT draft-ietf-tls-protocol-03.txt + + +FOR CertVerify +; + Says A B {|certificate A (pubK A), + Crypt KB (Nonce M)|} : set evs + *) TLS = Public + @@ -25,6 +32,11 @@ consts (*Client, server write keys. They implicitly include the MAC secrets.*) clientK, serverK :: "nat*nat*nat => key" + certificate :: "[agent,key] => msg" + +defs + certificate_def + "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}" rules (*clientK is collision-free and makes symmetric keys*) @@ -77,7 +89,7 @@ "[| 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)|}|} + certificate B (pubK B)|} # evs : tls" ClientCertKeyEx @@ -85,8 +97,8 @@ 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)|}, + certificate B KB|} : set evs |] + ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} # evs : tls" @@ -97,10 +109,10 @@ 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 |] + certificate B KB|} : set evs |] ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, - Crypt (priK Server) {|Agent B, Key KB|}|})) + certificate B KB|})) # evs : tls" (*Finally come the FINISHED messages, confirming XA and XB among @@ -111,13 +123,13 @@ "[| 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)|}, + certificate B KB|} : set evs; + Says A B {|certificate A (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)|}, + certificate A (pubK A), Nonce NB, Agent XB, Agent B|})) # evs : tls" @@ -128,14 +140,14 @@ "[| 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)|}|} + certificate B (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)|}|})) + certificate B (pubK B)|})) # evs : tls" (**Oops message??**)