2
$\begingroup$

Background

For my dissertation I am working on an application protocol for which I require a TLS session. I am looking to achieve Perfect Forward Secrecy, which means I have selected ephemeral Diffie-Hellman cipher suites. I intend to favor elliptic curve cryptography over regular DHE when I finish the model. I expect this to be easily interchangable in my model. I have found a model written in Pi calculus that makes use of RSA, which I have adapted to incorporate DH. Following RFC 5246 closely I have come to the model below.

Problem

Somehow large parts appear to be dead code. I have added a comment to the lines before which the dead code check fails. Please help me understand what is going wrong and causes ProVerif to report "cannot be proved".

Model

(**************************************************************************
 * DEFINITIONS                                                            *
 **************************************************************************)

param verboseClauses = explained.
param traceDisplay = long.

(* A public channel *)
free net.

(* Message tags *)
free ClientHello, ClientKeyExchange, ClientCertificate, ServerHello, ServerCertificate, CertificateVerify, ServerKeyExchange.

(* Agent initialization is done over a private channel *)
private free initialClientData, initialServerData.

(* The cryptographic constructors *)
fun hash/1.     (* hashing *)
fun encrypt/2.  (* symmetric key encryption *)
fun pencrypt/2. (* Public key encryption *)
fun sign/2.     (* Public key signing *)
fun enc/1.      (* Extracts encryption key from a keypair *)
fun dec/1.      (* Extracts decryption key from a keypair *)

(* The cryptographic destructors *)
reduc decrypt(encrypt(x, y), y) = x.
reduc pdecrypt(pencrypt(x, enc(y)), dec(y)) = x.
reduc unsign(sign(x, enc(y)), dec(y)) = x.

(* A constructor that maps agents to their secret keypairs *)
private fun signkeypair/1.

(* Pseudo−random−number function *)
fun PRF/1.

(* Symmetric key construction *)
fun clientK/3.
fun serverK/3.

(* Certificates *)
private fun cert/2.

(* If cert(x, y) establishes x as owner of key y, y is returned *)
reduc verify(cert(x, y), x) = y.

(* Diffie-Hellman functions *)
fun f/2.
fun g/1.
equation f(x, g(y)) = f(y, g(x)).

(**************************************************************************
 * QUERIES                                                                *
 **************************************************************************)

(* secrecy Pre Master secret *)
query attacker: PMS.

(* secrecy Master secret *)
query attacker: MSa.
query attacker: MSb.

(* secrecy Finished message from the client *)
query attacker: FinishedAFlag.

(* secrecy Finished message from the server *)
query attacker: FinishedBFlag.

(* authenticity of the server *)
query evinj: endServerAuth(x, y, z) ==> evinj: beginServerAuth(x, y, z).

(* authenticity of the client *)
query evinj: endClientAuth(x, y, z) ==> evinj: beginClientAuth(x, y, z).

(* Dead code check *)
query attacker: clientFinished.
query attacker: serverFinished.

(**************************************************************************
 * CLIENT PROCESS, this client is the initiator of the protocol.          *
 **************************************************************************)
let client =
    (** Initial agent data from a trusted channel **)
    in(initialClientData, (A, keypair, clientCert));

    let SKc = enc(keypair) in
    let PKc = dec(keypair) in

    (** Replication to model arbitrary sessions **)
    !

    (** Get the server’s name, perhaps as user input **)
    in(net, B);

    (* A generates fresh nonce Na *)
    new Na;

    (* A determines Sid, session is randomly generated in basic model *)
    new Sid;

    (* A chooses options Pa, options are just random data for our model *)
    new Pa;

    (* A −> B : ClientHello *)
    let CH = (ClientHello, A, Na, Sid, Pa) in out(net, CH);

    (* B −> A : ServerHello *)
    in(net, SH); let (=ServerHello, Nb, =Sid, Pb) = SH in

    (* B −> A : ServerCertificate *)
    in(net, SC); let (=ServerCertificate, serverCert) = SC in

    (* Receiving Server DH Key Parameters and checking integrity *)
    in(net, SKE); let (=ServerKeyExchange, G, N, GY, DHSignature) = SKE in
    let unsignKey = verify(serverCert, B) in

    (** THE LINE BELOW CAUSES PROVERIF TO CLAIM "CANNOT BE PROVED" WHEN CHECKING DEAD CODE **)
    let (=Na, =Nb, =G, =N, =GY) = unsign(DHSignature, unsignKey) in

    (** dead code check **)
    new clientFinished; out(net, clientFinished);

    (* A −> B: ClientCertificate *)
    let CC = (ClientCertificate, clientCert) in out(net, CC);

    (* A −> B : ClientKeyExchange *)
    new X;
    let CKE = (ClientKeyExchange, g(X)) in out(net, CKE);

    let cvHash = hash((CH, SH, SC, SKE, CC, CKE)) in

    (** begin client authentication **)
    event beginClientAuth(A, B, cvHash);

    (* A −> B: CertificateVerify *)
    let CV = sign((CertificateVerify, cvHash), SKc) in out(net, CV);

    (* Compute the pre-master secret (g^xy) *)
    let PMS = f(GY, g(X)) in

    (* A calculates the Master secret M *)
    let M = PRF((PMS, Na, Nb)) in

    (* A calculates Finished *)
    let Finished = hash((CH, SH, SC, CC, CKE, CV, M)) in

    (* A −> B : Finished *)
    out(net, encrypt(Finished, clientK(Na, Nb, M)));

    (* B −> A : Finished *)
    in(net, FB);

    (* A verifies received finished *)
    let =Finished = decrypt(FB, serverK(Na, Nb, M)) in

    (** end server authentication **)
    event endServerAuth(A, B, PMS);

    (** secrecy check on the Master secret **)
    new MSa; out(M, MSa) |

    (** secrecy check on the Finished message **)
    new FinishedAFlag; out(Finished, FinishedAFlag).

(**************************************************************************
 * THE SERVER PROCESS                                                     *
 **************************************************************************)
let server =
    (** THE LINE BELOW CAUSES PROVERIF TO CLAIM "CANNOT BE PROVED" WHEN CHECKING DEAD CODE **)
    (** Initial agent data from a trusted channel **)
    in(initialServerData, (B, keypair, serverCert));

    (** dead code check **)
    new serverFinished; out(net, serverFinished);

    let PKs = dec(keypair) in
    let SKs = enc(keypair) in

    (** Replication to model arbitrary sessions **)
    !

    (* A −> B : ClientHello *)
    in(net, CH); let (=ClientHello, A, Na, Sid, Pa) = CH in

    (* B generates fresh nonce Nb *)
    new Nb;

    (* B chooses options Pb, just some random data in our model *)
    new Pb;

    (* B −> A : ServerHello *)
    let SH = (ServerHello, Nb, Sid, Pb) in out(net, SH);

    (* B −> A : ServerCertificate *)
    let SC = (ServerCertificate, serverCert) in out(net, SC);

    (* Generate Diffie-Hellman Key Exchange parameters *)
    new G; (* Generator, public *)
    new N; (* Modulus (prime), public *)
    new Y; (* Server's secret exponent *)

    (* B -> A: ServerKeyExchange *)
    let SKE = (ServerKeyExchange, G, N, g(Y), sign((Na, Nb, G, N, g(Y)), SKs)) in out(net, SKE);

    (* A −> B : ClientCertificate *)
    in(net, CC); let (=ClientCertificate, clientCert) = CC in

    (* A −> B : ClientKeyExchange *)
    in(net, CKE); let(=ClientKeyExchange, GX) = CKE in

    (* A −> B : CertificateVerify *)
    let unsignKey = verify(clientCert, A) in
    in(net, CV); let (=CertificateVerify, cvHash) = unsign(CV, unsignKey) in

    (* B verifies client signature *)
    let =cvHash = hash((CH, SH, SC, SKE, CC, CKE)) in

    (** end client authentication **)
    event endClientAuth(A, B, cvHash);

    (* Calculating the Pre-Master Secret *)
    let PMS = f(GX, g(Y)) in

    (* A −> B : Finished *)
    in(net, FA);

    (* B calculates M *)
    let M = PRF((PMS, Na, Nb)) in

    (* B calculates Finished *)
    let Finished = hash((CH, SH, SC, SKE, CC, CKE, CV, M)) in

    (** server authentication **)
    event beginServerAuth(A, B, PMS);

    (* B −> A : Finished *)
    out(net, encrypt(Finished, serverK(Na, Nb, M)));

    (* B verifies received Finished *)
    let =Finished = decrypt(FA, clientK(Na, Nb, M)) in

    (** secrecy check on the Master secret **)
    new MSb; out(M, MSb) |

    (** secrecy check on the finished **)
    new FinishedBFlag; out(Finished, FinishedBFlag).

(**************************************************************************
 * THE INITIALIZER PROCESS                                                *
 **************************************************************************)
let initializer =
    new C; (* Generate agent name *)
    new S; (* Generate agent name *)
    let clientKeyPair = signkeypair(C) in (* Generate client key *)
    let serverKeyPair = signkeypair(S) in (* Generate server key *)
    let clientCert = cert(C, dec(clientKeyPair)) in
    let serverCert = cert(S, dec(serverKeyPair)) in
    out(initialClientData, (C, clientKeyPair, clientCert));
    out(initialServerData, (S, serverKeyPair, serverCert));
    out(net, S).

(**************************************************************************
 * THE SYSTEM                                                             *
 **************************************************************************)
process
    !initializer | !client | !server
$\endgroup$
  • $\begingroup$ Have you posted to the ProVerif mailing list? I don't know everyone's skill sets on this site, but we haven't had any other ProVerif questions in the past and I'm not sure how much this community uses the tool. $\endgroup$ – mikeazo Aug 10 '15 at 12:33
  • $\begingroup$ No I haven't, thanks for the tip. I didn't even know they had one. I'm leaving this question open on the off chance someone still might know the cause of the issue. $\endgroup$ – Geert Smelt Aug 10 '15 at 13:04
  • $\begingroup$ Definitely if you get a response on the mailing list, post it here. FYI, there was some chatter in The Side Channel about whether or not this question is on topic since it is about a specific tool and the problems relate to the tool and not cryptography. It doesn't have any close votes yet, so we'll see. $\endgroup$ – mikeazo Aug 10 '15 at 13:10
  • $\begingroup$ I've added the reply like you asked. Hopefully it will serve someone else too someday. $\endgroup$ – Geert Smelt Aug 18 '15 at 14:03
1
$\begingroup$

I have sent this question to the ProVerif mailing list as suggested in the comments. The response I obtained from Bruno Blanchet was as follows.

Actually, ProVerif does not say that the code is dead, it just says that it cannot prove that it is not dead. (It says "RESULT not attacker:serverFinished_96[...] cannot be proved.") If it said "RESULT not attacker:serverFinished_96[...] is true." then the code would definitely be dead.

The code really is not dead. The reason why ProVerif does not manage to prove this property comes from abstractions made in the internal representation of the protocol by Horn clauses. More precisely, you have

let initializer =
   ...
   out(initialClientData, (C, clientKeyPair, clientCert));
   out(initialServerData, (S, serverKeyPair, serverCert));
   ...

let server =
   (** Initial agent data from a trusted channel **)
   in(initialServerData, (B, keypair, serverCert));
   (** dead code check **)
   new serverFinished; out(net, serverFinished);
   ...

let client =
   (** Initial agent data from a trusted channel **)
   in(initialClientData, (A, keypair, clientCert));
   ...

At the Horn clause level, ProVerif manages to output serverFinished, as it explains in the following text:

  1. The message (S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356)))) may be sent on channel initialServerData[] at output {9}. mess:initialServerData[],(S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356)))).
  2. The message (S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356)))) that may be sent on channel initialServerData[] by 1 may be received at input {53}. So the message serverFinished_12357 may be sent to the attacker at output {55}. attacker:serverFinished_12357.

ProVerif believes that it just needs to run the initializer to send the message on initialServerData (step 1 above), and the server to receive it in order to output serverFinished (step 2 above). ProVerif then tries to reconstruct a trace at the pi calculus level. However, to run the output on initialServerData in the initializer, it first needs to output a message on initialClientData. Since initialClientData is a private channel, it needs an input to receive this message. This input is located in the client. However it does not appear at all in the Horn clause derivation above. That is why the trace reconstruction fails, and ProVerif says that it cannot prove that the code is not dead.

More generally, the Horn clause representation introduces more abstractions in the presence of private channels, and that sometimes causes the failure of trace reconstruction even in fairly simple cases, such as the one above.

In your example, one way to avoid the problem is to rewrite the initializer process so that it performs the final outputs in parallel instead of in sequence:

(out(initialClientData, (C, clientKeyPair, clientCert)) | out(initialServerData, (S, serverKeyPair, serverCert)) | out(net, S)).
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.