ProVerif Handshake Model

[jschneider-bensch]

This PR includes the latest extracted model for the TLS handshake, as well as a set of patches for lib.pvl (the bulk of the extraction) and analysis.pv (where the the top-level processes are set up and analysis queries are specified).

The patches inlcude changes to the extracted model (described below), which allow us to show

• that the modeled handshake can fully complete for both parties (as a baseline for further analysis)
• Server authenticity, assuming neither the certificate signing key nor a potential pre-shared key have been compromised
• Secrecy of the resulting session key under the same assumptions

The intended flow using the driver is to run

• ./hax-driver.py extract-proverif to extract the ProVerif model to proofs/proverif/extraction.
• ./hax-driver.py patch-proverif to apply the patches on the extracted model.
• ./hax-driver.py typecheck-proverif to run the analysis on the patched model.

The patches are necessary for parts of the model that we cannot currently generate (properly, or at all):

• a top-level process structure which instantiates Client and Server with ciphersuites and psk-mode configuration,
• event definitions and analysis queries,
• cryptographic operations and their semantics
• tls13formats related code, especially anything that relates to concatenation primitives

Additionally, the patches introduce the following modifications:

• A mock certificate validation, checking that the name in the certificate agrees with the name of the expected peer from the top-level process. This is because Bertie does not include full certificate validation at this time, but some binding between the name and the certificate is necessary for showing server authentication.
• A model-side fix for the issue that is fixed on the Rust side in Correct argument order for process_psk_binder_zero_rtt #101 (until that is fixed on the Rust side).
• The removal of all automatically generated events, since that leads to poor performance from ProVerif and is not necessary at all for the analysis (cf. [ProVerif] Emitting events unnecessarily blows up the extracted model hax#581)

---

Original PR message

This PR attempts to address some parts of #15, namely it includes a typechecking model where the number of handwritten functions was reduced to under 25.

It also includes handwritten models for these functions which have been inserted at the appropriate place in the extraction.

The model included here can be typechecked using the driver, i.e. hax-driver.py typecheck-proverif. One more extraction will reset the model to a state before the handwritten parts were included. I'm working on a mechanism to automatically include these parts during the extraction by the driver.

Before this PR can be merged, cryspen/hax#561 must be merged into hax, since this depends on my branch of hax until that PR is in hax.

[karthikbhargavan]

After following the instructions in this PR, I get the following results from ProVerif, which is what is expected. Great work. I am leaving other comments in the PR to be addressed, either in this PR or in a follow-up.

--------------------------------------------------------------
Verification summary:

Query not event(Reachable_simple) is false.

Query not event(ClientFinished(server_name_24,cipher_30,st_6)) is false.

Query not event(ServerFinished(server_name_24,cipher_30,st_6)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) ==> event(ServerFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_22),sst)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) ==> event(ServerFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_22),sst)) || event(CompromisedServerCertSK(server_name_24)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) ==> event(ServerFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_22),sst)) || event(CompromisedServerPSK(server_name_24)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) ==> event(ServerFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_22),sst)) || event(CompromisedServerCertSK(server_name_24)) || event(CompromisedServerPSK(server_name_24)) is true.

Query not (event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) && attacker(s2ckiv)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) && attacker(s2ckiv) ==> event(CompromisedServerCertSK(server_name_24)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) && attacker(s2ckiv) ==> event(CompromisedServerPSK(server_name_24)) is false.

Query event(ClientFinished(server_name_24,bertie__tls13record__DuplexCipherState1_c(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_22),cst)) && attacker(s2ckiv) ==> event(CompromisedServerCertSK(server_name_24)) || event(CompromisedServerPSK(server_name_24)) is true.

--------------------------------------------------------------

[karthikbhargavan]

There is still some work to do to to clean up the patches:

• events should not be automatically injected into every letfun
• we should separate out the crypto model (heavily hand-edited) from the protocol model (mostly untouched)
• we should have markers where we can inject the hand-edited bits so that the diff can be cleaner.

[jschneider-bensch]

events should not be automatically injected into every letfun

This is tracked by cryspen/hax#581.

we should separate out the crypto model (heavily hand-edited) from the protocol model (mostly untouched)

we should have markers where we can inject the hand-edited bits so that the diff can be cleaner.

These are both related to cryspen/hax#563. Once that is addressed, we should be able to cleanly separate the hand-edits from the rest of the model.

---

I've added issues #104, #105 to track progress here.