Refresh ProVerif extraction

[jschneider-bensch]

The eventual goal will be to restore PV extraction and all properties for the code on the key_schedule_security branch.
The sub-issues here deal with restoring extraction and proofs on the main branch, which will be a prerequisite for doing so on the key schedule branch.

[jschneider-bensch]

My WIP on these tasks is on branch jonas/proverif-refresh.

[franziskuskiefer]

cryspen/hax#1360

[jschneider-bensch]

On jonas/proverif-refresh I have restored valid PV extraction.

I am now working through the model, making sure everything is reachable and restoring the verification results.

[jschneider-bensch]

The latest commit on jonas/proverif-refresh introduced a long wait time for the reachability analysis in the translation to Horn clauses phase. It did, however fix the most recent reachability issue I was investigating, meaning I can move on to test reachability further into the model.
I will keep this running on the side as I look at other things, for now.

[jschneider-bensch]

With the current state, PV can show reachability at least for all of the client process. I'm still waiting for the server process, due to the long processing time.
For the server we also have full reachability. Let's see about the security queries.

Ugh, I made a mistake and have to check again about the client.

[jschneider-bensch]

Okay, the reachability works for client and server, but only with the help of the attacker, at the moment:

Query not event(Reachable_simple) is false.

Query not event(ClientFinished(server_name_64,cipher_120,st_8)) is true.

Query not event(ServerFinished(server_name_64,cipher_120,st_8)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) ==> event(ServerFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_82),sst)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) ==> event(ServerFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_82),sst)) || event(CompromisedServerCertSK(server_name_64)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) ==> event(ServerFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_82),sst)) || event(CompromisedServerPSK(server_name_64)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) ==> event(ServerFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,s2ckiv,s2cctr,c2skiv,c2sctr,exp_82),sst)) || event(CompromisedServerCertSK(server_name_64)) || event(CompromisedServerPSK(server_name_64)) is true.

Query not (event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) && attacker(s2ckiv)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) && attacker(s2ckiv) ==> event(CompromisedServerCertSK(server_name_64)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) && attacker(s2ckiv) ==> event(CompromisedServerPSK(server_name_64)) is true.

Query event(ClientFinished(server_name_64,bertie__tls13record__DuplexCipherState1(alg_12,c2skiv,c2sctr,s2ckiv,s2cctr,exp_82),cst)) && attacker(s2ckiv) ==> event(CompromisedServerCertSK(server_name_64)) || event(CompromisedServerPSK(server_name_64)) is true.

This took 2h 40min.

[jschneider-bensch]

We have a refreshed ProVerif model with the latest changes to F* and SSProve on branch https://github.com/cryspen/bertie/tree/artifact.
Closing this is just a matter of getting that branch merged to main.

[jschneider-bensch]

Resolved by #148