Key schedule security

.github/workflows/gh-pages.yml

@@ -41,7 +41,7 @@ jobs:
           done
 
       - name: Upload Documentation Artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           path: "target/doc"
 
@@ -56,4 +56,4 @@ jobs:
     steps:
       - name: Deploy Documentation to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v2
+        uses: actions/deploy-pages@v4

.github/workflows/scheduled.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: EmbarkStudios/cargo-deny-action@v1
         # TODO: Check licenses, too.
         with:

benches/client.rs

@@ -1,5 +1,6 @@
 #![allow(dead_code)]
 
+use std::collections::HashMap;
 use std::time::{Duration, Instant};
 
 use bertie::{
@@ -21,7 +22,7 @@ use bertie::{
         SignatureScheme,
     },
     tls13utils::Bytes,
-    Client, Server,
+    Client, Server, TLSkeyscheduler,
 };
 use libcrux::{digest, drbg::Drbg};
 
@@ -156,6 +157,9 @@ fn protocol() {
 
     for ciphersuite in CIPHERSUITES {
         let mut rng = Drbg::new(digest::Algorithm::Sha256).unwrap();
+        let mut ks: TLSkeyscheduler = TLSkeyscheduler {
+            keys: HashMap::new(),
+        };
 
         // Server
         let server_name_str = "localhost";
@@ -182,24 +186,26 @@ fn protocol() {
         for _ in 0..ITERATIONS {
             let start_time = Instant::now();
             let (client_hello, client) =
-                Client::connect(ciphersuite, &server_name, None, None, &mut rng).unwrap();
+                Client::connect(ciphersuite, &server_name, None, None, &mut rng, &mut ks).unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
             size1 += client_hello.declassify().len();
 
             let (server_hello, server_finished, server) =
-                Server::accept(ciphersuite, db.clone(), &client_hello, &mut rng).unwrap();
+                Server::accept(ciphersuite, db.clone(), &client_hello, &mut rng, &mut ks).unwrap();
             size2 += server_hello.declassify().len();
             size2 += server_finished.declassify().len();
 
             let start_time = Instant::now();
-            let (_client_msg, client) = client.read_handshake(&server_hello).unwrap();
-            let (client_msg, client) = client.read_handshake(&server_finished).unwrap();
+            let (_client_msg, client) = client.read_handshake(&server_hello, &mut ks).unwrap();
+            let (client_msg, client) = client.read_handshake(&server_finished, &mut ks).unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
             size3 += client_msg.as_ref().unwrap().declassify().len();
 
-            let server = server.read_handshake(&client_msg.unwrap()).unwrap();
+            let server = server
+                .read_handshake(&client_msg.unwrap(), &mut ks)
+                .unwrap();
 
             let application_data = payload.clone().into();
 

benches/server.rs

@@ -1,3 +1,4 @@
+use std::collections::HashMap;
 use std::time::{Duration, Instant};
 
 use bertie::{
@@ -19,7 +20,7 @@ use bertie::{
         SignatureScheme,
     },
     tls13utils::Bytes,
-    Client, Server,
+    Client, Server, TLSkeyscheduler,
 };
 use libcrux::{digest, drbg::Drbg};
 
@@ -100,6 +101,12 @@ fn protocol() {
 
     for ciphersuite in CIPHERSUITES {
         let mut rng = Drbg::new(digest::Algorithm::Sha256).unwrap();
+        let mut client_ks: TLSkeyscheduler = TLSkeyscheduler {
+            keys: HashMap::new(),
+        };
+        let mut server_ks: TLSkeyscheduler = TLSkeyscheduler {
+            keys: HashMap::new(),
+        };
 
         // Server
         let server_name_str = "localhost";
@@ -121,20 +128,39 @@ fn protocol() {
         let payload = rng.generate_vec(NUM_PAYLOAD_BYTES).unwrap();
 
         for _ in 0..ITERATIONS {
-            let (client_hello, client) =
-                Client::connect(ciphersuite, &server_name, None, None, &mut rng).unwrap();
+            let (client_hello, client) = Client::connect(
+                ciphersuite,
+                &server_name,
+                None,
+                None,
+                &mut rng,
+                &mut client_ks,
+            )
+            .unwrap();
 
             let start_time = Instant::now();
-            let (server_hello, server_finished, server) =
-                Server::accept(ciphersuite, db.clone(), &client_hello, &mut rng).unwrap();
+            let (server_hello, server_finished, server) = Server::accept(
+                ciphersuite,
+                db.clone(),
+                &client_hello,
+                &mut rng,
+                &mut server_ks,
+            )
+            .unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
 
-            let (_client_msg, client) = client.read_handshake(&server_hello).unwrap();
-            let (client_msg, client) = client.read_handshake(&server_finished).unwrap();
+            let (_client_msg, client) = client
+                .read_handshake(&server_hello, &mut client_ks)
+                .unwrap();
+            let (client_msg, client) = client
+                .read_handshake(&server_finished, &mut client_ks)
+                .unwrap();
 
             let start_time = Instant::now();
-            let server = server.read_handshake(&client_msg.unwrap()).unwrap();
+            let server = server
+                .read_handshake(&client_msg.unwrap(), &mut server_ks)
+                .unwrap();
             let end_time = Instant::now();
             handshake_time += end_time.duration_since(start_time);
 

flake.nix

@@ -8,21 +8,25 @@
     };
     hax.url = "github:hacspec/hax";
   };
-  outputs =
-    inputs:
-    inputs.flake-utils.lib.eachDefaultSystem (
-      system:
-      let
-        hax = inputs.hax.packages.${system}.default;
-        pkgs = import inputs.nixpkgs { inherit system; };
-        craneLib = inputs.crane.mkLib pkgs;
-        src = ./.;
-        cargoArtifacts = craneLib.buildDepsOnly { inherit src; };
-        bertie = craneLib.buildPackage {
+  outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = import inputs.nixpkgs { inherit system; };
+      # Make an overrideable package.
+      bertie = { python3, craneLib, hax, runCommand, cargoLock }:
+        let
+          src = runCommand "bertie-src" { } ''
+            cp -r ${./.} $out
+            chmod u+w $out
+            rm -f $out/Cargo.lock
+            cp ${cargoLock} $out/Cargo.lock
+          '';
+          cargoArtifacts = craneLib.buildDepsOnly { inherit src; };
+        in
+        craneLib.buildPackage {
           inherit src cargoArtifacts;
           buildInputs = [
             hax
-            pkgs.python3
+            python3
           ];
           buildPhase = ''
             python hax-driver.py extract-fstar
@@ -31,9 +35,13 @@
           installPhase = "cp -r . $out";
           doCheck = false;
         };
-      in
-      {
-        packages.default = bertie;
-      }
-    );
+      hax = inputs.hax.packages.${system}.default;
+      craneLib = inputs.crane.mkLib pkgs;
+    in
+    {
+      # Takes the lockfile as input.
+      packages.default = cargoLock: pkgs.callPackage bertie { inherit hax craneLib cargoLock; };
+      devShells.default = craneLib.devShell { };
+    }
+  );
 }

hax-driver.py

@@ -35,6 +35,8 @@ def shell(command, expect=0, cwd=None, env={}):
     help="Extract and typecheck F* etc. from the Bertie Rust code.",
 )
 extract_parser = sub_parser.add_parser("extract-fstar")
+extract_parser = sub_parser.add_parser("extract-ssprove")
+extract_parser = sub_parser.add_parser("extract-coq")
 extract_proverif_parser = sub_parser.add_parser("extract-proverif")
 typecheck_parser = sub_parser.add_parser("typecheck")
 patch_proverif_parser = sub_parser.add_parser("patch-proverif")
@@ -102,6 +104,44 @@ def shell(command, expect=0, cwd=None, env={}):
         cwd=".",
         env=hax_env,
     )
+elif options.sub == "extract-ssprove":
+    # The extract sub command.
+    shell(
+        cargo_hax_into_pv
+        + [
+            "-i",
+            " ".join([
+                "-**",
+                "+~**::tls13handshake::**",
+                "+~**::server::lookup_db", # to include transitive dependency on tls13utils
+                "+~**::tls13keyscheduler::**",
+                "+~**::tls13utils::parse_failed", # transitive dependencies required
+                "+~**::tls13crypto::zero_key", # transitive dependencies required
+                ]),
+            "ssprove",
+        ],
+        cwd=".",
+        env=hax_env,
+    )
+elif options.sub == "extract-coq":
+    # The extract sub command.
+    shell(
+        cargo_hax_into_pv
+        + [
+            "-i",
+            " ".join([
+                "-**",
+                "+~**::tls13handshake::**",
+                "+~**::server::lookup_db", # to include transitive dependency on tls13utils
+                "+~**::tls13keyscheduler::**",
+                "+~**::tls13utils::parse_failed", # transitive dependencies required
+                "+~**::tls13crypto::zero_key", # transitive dependencies required
+                ]),
+            "coq",
+        ],
+        cwd=".",
+        env=hax_env,
+    )
 elif options.sub == "extract-handshake":
     # The extract sub command.
     shell(

proofs/ssprove/.gitignore

@@ -0,0 +1,62 @@
+.hidden
+*.tmp
+
+##Coq
+*.vo
+*.vok
+*.vos
+*.glob
+*.v.d
+*~
+CoqMakefile
+CoqMakefile.conf
+Makefile.coq
+Makefile.coq.conf
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.ml.d
+*.mllib.d
+*.ml4.d
+*.mli.d
+*.mlpack.d
+*.native
+*.o
+*.aux
+*.d
+*.lia.cache
+doc/
+docs/
+_opam/
+.merlin
+META.*
+
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+
+
+
+## Editors
+
+### VisualStudioCode ###
+.vscode/*
+!.vscode/tasks.json
+!.vscode/launch.json
+!.vscode/extensions.json
+
+### VisualStudioCode Patch ###
+# Ignore all local history of files
+.history