Merge pull request #139 from cryspen/jonas/proverif-key-schedule

Workaround extraction issues

.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:

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 { };
+    }
+  );
 }

src/server.rs

@@ -55,7 +55,12 @@ pub(crate) fn lookup_db(
     sni: &Bytes,
     tkt: &Option<Bytes>,
 ) -> Result<ServerInfo, TLSError> {
-    println!("sni {:?} {:?} {}", sni, db.server_name, eq(sni, &db.server_name));
+    println!(
+        "sni {:?} {:?} {}",
+        sni,
+        db.server_name,
+        eq(sni, &db.server_name)
+    );
     if eq(sni, &Bytes::new()) || eq(sni, &db.server_name) {
         match (ciphersuite.psk_mode(), tkt, &db.psk_opt) {
             (true, Some(ctkt), Some((stkt, psk))) => {

src/tls13crypto.rs

@@ -115,8 +115,7 @@ impl HashAlgorithm {
     }
 
     /// Get the size of the hash digest.
-    pub// (crate)
-    fn hash_len(&self) -> usize {
+    pub fn hash_len(&self) -> usize {
         match self {
             HashAlgorithm::SHA256 => digest::digest_size(digest::Algorithm::Sha256),
             HashAlgorithm::SHA384 => digest::digest_size(digest::Algorithm::Sha384),

src/tls13handshake.rs

@@ -201,15 +201,19 @@ fn put_server_hello(
     };
     set_by_handle(ks, &shared_secret_handle, shared_secret);
 
-    let psk_handle = psk.map(|x| {
-        let handle = Handle {
-            alg: ciphersuite.hash,
-            name: PSK,
-            level: 0,
-        };
-        set_by_handle(ks, &handle, x);
-        handle
-    });
+    // hax-issue: can't use mutating map here
+    let psk_handle = match psk {
+        Some(bytes) => {
+            let handle = Handle {
+                alg: ciphersuite.hash,
+                name: PSK,
+                level: 0,
+            };
+            set_by_handle(ks, &handle, bytes);
+            Some(handle)
+        }
+        None => None,
+    };
 
     let (ch_handle, sh_handle, ms_handle) = derive_hk_handles(
         &ciphersuite.hash,
@@ -560,15 +564,20 @@ fn get_server_hello(
     let transcript = state.transcript.add(&sh);
     let transcript_hash = transcript.transcript_hash()?;
 
-    let psk_handle = state.server.psk_opt.clone().map(|x| {
-        let handle = Handle {
-            alg: state.ciphersuite.hash,
-            name: PSK,
-            level: 0,
-        };
-        set_by_handle(ks, &handle, x);
-        handle
-    });
+    // hax-issue: can't use mutating map here
+    let psk_handle = state.server.psk_opt.clone();
+    let psk_handle = match psk_handle {
+        Some(bytes) => {
+            let handle = Handle {
+                alg: state.ciphersuite.hash,
+                name: PSK,
+                level: 0,
+            };
+            set_by_handle(ks, &handle, bytes);
+            Some(handle)
+        }
+        None => None,
+    };
 
     let (ch_handle, sh_handle, ms_handle) = derive_hk_handles(
         &state.ciphersuite.hash,

src/tls13keyscheduler/key_schedule.rs

@@ -367,30 +367,29 @@ pub fn XPD<KS: KeySchedule<TLSnames>>(
         .get(n1.unwrap(), l, (h1.name, h1.alg, h1.level))
         .ok_or(INCORRECT_STATE)?;
 
-    let k: TagKey;
-    if n == PSK {
+    let k: TagKey = if n == PSK {
         l = l + 1;
-        k = xpd(
+        xpd(
             &TagKey {
                 alg: h1.alg,
                 tag: h1.name,
                 val: k1,
             },
             label,
             args,
-        )?;
+        )?
     } else {
         let d = KS::hash(args);
-        k = xpd(
+        xpd(
             &TagKey {
                 alg: h1.alg,
                 tag: h1.name,
                 val: k1,
             },
             label,
             &d,
-        )?;
-    }
+        )?
+    };
     // let h =
     let _ = ks.set(n, l, (h.name, h.alg, h.level), k.val);
     // set(&mut self, name: N, level: u8, h: (N, HashAlgorithm, u8), hon: bool, k: (N, Key));
@@ -535,7 +534,6 @@ pub(crate) fn XTR<KS: KeySchedule<TLSnames>>(
 //     }
 // }
 
-
 // pub(crate) fn nextKeys(key: &TagKey, extra: Bytes, digest: &Digest, aead_algorithm: &AeadAlgorithm,) -> Vec<TagKey> {
 //     // 0-RTT (k_cet)
 //     derive_0rtt_keys(

tests/test_tls13api.rs

@@ -222,7 +222,6 @@ fn test_full_round_trip() {
     assert!(b);
 }
 
-
 #[test]
 fn test_full_round_trip_with_psk() {
     let cr = random_bytes(32);