Update F*, SSProve, ProVerif in sync

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

ARTIFACT.md

@@ -0,0 +1,105 @@
+# Instructions for artifact evaluation
+
+## Prerequisites
+### Setting up the hax toolchain
+We use the hax toolchain to extract proof artifacts from the Rust
+source code in `src`. To be able to reproduce this extraction for
+yourself, please follow the installation instructions for `hax`
+provided at:
+
+https://github.com/cryspen/hax?tab=readme-ov-file#installation
+
+#### `hax-driver.py`
+We use the Python 3 script `hax-driver.py` to drive extraction and
+verification of the proof artifacts, so an installation of Python 3 is
+required.
+
+### Setting up F*
+We use F* version 2025.03.25 to prove runtime safety and transcript
+unambiguity as described in section 7 of the paper submission. To
+reproduce these results for yourself, please install F* following the
+instructions at:
+
+https://fstar-lang.org/index.html#download
+
+### Setting up Rocq + SSProve
+We use Rocq version 8.18.0 and SSProve for the security proofs of the
+key schedule as described in section 5 of the paper submission. Installation
+instructions can be found at:
+
+https://rocq-prover.org/install
+https://github.com/SSProve/ssprove
+
+Furthermore, Rust core library, which is used by the Hax translation, for Rocq/SSProve is located at:
+
+https://github.com/cryspen/hax/tree/main/proof-libs
+
+### Setting up ProVerif
+We use ProVerif version 2.05 to perform protocol security analysis of the
+implementation, as described in section 6 of the paper submission.
+To be able to reproduce the analysis, please follow the installation
+instructions provided at:
+
+https://bblanche.gitlabpages.inria.fr/proverif/
+
+## Proof extraction using hax
+### F*
+To regenerate the extraction to F*, run
+```
+./hax-driver.py extract-fstar
+```
+
+### SSProve
+To regenerate the extraction for the key schedule in SSProve, run
+```
+./hax-driver.py extract-ssprove
+```
+
+To get the code running we apply a patch
+```
+patch -d extraction/ < extraction.patch
+rm -rf fextraction/
+mv extraction/ fextraction/
+```
+
+### ProVerif
+The ProVerif proofs described in section 6 of the paper submission can
+be extracted from the Rust source code by running
+```
+./hax-driver.py extract-proverif
+```
+
+This will generate the file `proofs/proverif/extraction/lib.pvl` from
+the Rust source code.
+
+## Running the Proofs
+### F*
+To run the F* proofs, run the following command:
+```
+./hax-driver.py typecheck
+```
+
+### SSProve
+First generate the Makefile from the _CoqProject
+```
+coq_makefile -f _CoqProject -o Makefile
+```
+and run `make`.
+
+### ProVerif
+To run the ProVerif analysis, as described in section 6 of the paper
+submission, run
+```
+./hax-driver.py typecheck-proverif
+```
+
+This will run the command 
+```
+proverif -lib proofs/proverif/handwritten_lib.pvl -lib
+proofs/proverif/extraction/lib.pvl proofs/proverif/extraction/analysis.pv
+```
+to start the analysis. The file `handwritten_lib.pvl` exists for
+technical reasons and contains early
+definitions of certain terms. The file `analysis.pvl` contains the
+top-level protocol process and analysis queries, as described in
+section 6 of the paper submission.

Cargo.toml

@@ -29,10 +29,12 @@ libcrux-ed25519 = { version = "0.0.2-beta.3", git = "https://github.com/cryspen/
 libcrux-ecdsa = { version = "0.0.2-beta.3", git = "https://github.com/cryspen/libcrux", features = [
     "rand",
 ] }
-hax-lib = { version = "0.2", git = "https://github.com/cryspen/hax" }
+#hax-lib = { version = "0.2", git = "https://github.com/cryspen/hax" }
+hax-lib = { git = "https://github.com/cryspen/hax" }
 
 [features]
-default = ["api", "std"]
+default = ["api", "std", "defensive"]
+defensive = []
 std = []
 test_utils = []
 secret_integers = []
@@ -82,4 +84,4 @@ default-members = [
 ]
 
 [lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(bench)'] }
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(bench)', 'cfg(hax)'] }

PROOFS.md

@@ -61,24 +61,29 @@ Using hax, we generate a ProVerif model of the TLS 1.3 handshake
 in `proofs/proverif/extraction/lib.pvl`.  This file contains the bulk of the extraction,
 while `analysis.pv` contains the top-level processes are set up and analysis queries.
 
-We provide patches that include changes to the extracted model (described below), which allow us to show
+We can 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.
+* Server authenticity, assuming the certificate signing key is not
+  compromised 
+* Forward 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 hacspec/hax#581)
+./hax-driver.py typecheck-proverif to run the analysis
+```
+
+## Security of the Key Schedule in SSProve
+
+We extract the implementation of the Key Schedule from SSProve.
+We then fix the implementation to only include the parts we need and make sure the translation is actually valid.
+This is done with a patch file to allow easier updates to the implementation.
+
+The proof for security of the key schedule is done on a specification.
+The entry functions of the specification are generalized and then instantiated with the functions in the implementation.
+We show the implemented functions fulfill some properties to be valid in the key schedule proof.
+
+The proof for the specification follows the proof in "Key-schedule Security for the TLS 1.3 Standard."
+We prove the Core Key Schedule Theorem by showing the main lemma D6.
+The other lemmas are a direct consequence of the correct implementation of the cryptographic primitives, which we inherit from libcrux.
+These lemmas are therefore only stated, and the proof is Admitted.

anonymize.sh

@@ -0,0 +1,76 @@
+rm -rf assets/
+rm -rf target/
+rm -f CODEOWNERS
+rm -f SECURITY.md
+rm -f CODE_OF_CONDUCT.md
+rm -f util/top1m.txt
+rm -rf .github/ISSUE_TEMPLATE
+rm -rf CLA.md
+rm -rf bench.md
+rm -rf LICENSE
+
+### ACKNOWLEDGEMENTS
+
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/assets/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/cryspen/d' {} \;
+
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/PUBLICATIONS/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/a number of prior/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/Some of the most relevant/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/succinct, executable/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/Verified Models and Reference/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/A Messy State of the Union/d' {} \;
+
+find . -not -path "./.git/*" -type f -exec sed -i -e '/reach out to Crypsen/d' {} \;
+
+find . -not -path "./.git/*" -type f -exec sed -i -e '/LICENSE/d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i -e '/licensed under/d' {} \;
+
+# find . -not -path "./.git/*" -type f -exec sed -i -e '/ACKNOWLEDGEMENTS/d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i -e '/The Bertie project./d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i -e '/project tasks/d' {} \;
+# find . -not -path "./.git/*" -type f -exec sed -i -e '/Cryspen/d' {} \;
+find ./README.md -not -path "./.git/*" -type f -exec sed -i -e '/Inria/d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i -e '/nlnet foundation/d' {} \;
+
+find . -not -path "./.git/*" -type f -exec sed -i '/first authored Bertie/d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i '/authors =/d' {} \;
+find . -not -path "./.git/*" -type f -exec sed -i '/repository =/d' {} \;
+
+######################################
+# Replace instances of Bertie/bertie #
+######################################
+
+find . -not -path "./.git/*" -type f -name '*Bertie*' | while read FILE ; do
+    newfile="$(echo ${FILE} |sed -e 's/Bertie/T13/')" ;
+    mv "${FILE}" "${newfile}" ;
+done
+
+find . -not -path "./.git/*" -type f -iname '*bertie*' | while read FILE ; do
+    newfile="$(echo ${FILE} |sed -e 's/bertie/t13/')" ;
+    mv "${FILE}" "${newfile}" ;
+done
+
+find . -not -path "./.git/*" -not -path "./tests/*" -type f -exec sed -i 's/Bertie/T13/gi' {} \;
+find . -not -path "./.git/*" -not -path "./tests/*" -type f -exec sed -i 's/bertie/t13/gi' {} \;
+find ./tests -name "*.md" -type f -exec sed -i 's/bertie/t13/gi' {} \;
+find ./tests -name "*.rs" -type f -exec sed -i 's/bertie/t13/gi' {} \;
+find ./tests -name "*.sh" -type f -exec sed -i 's/bertie/t13/gi' {} \;
+
+find ./Cargo.toml -type f -exec sed -i 's/bertie-libs/t13-libs/g' {} \;
+
+rm Cargo.lock
+cargo clean
+
+### Checks
+
+grep -riI bertie --exclude-dir=.git
+grep -riI cryspen --exclude-dir=.git
+grep -riI inria --exclude-dir=.git
+grep -riI "Karthikeyan" --exclude-dir=.git
+grep -riI "Karthikeyan Bhargavan" --exclude-dir=.git
+find . -type f -iname '*bertie*'
+
+rm -rf .git
+rm -f anonymize.sh
+

bench.md

@@ -0,0 +1,90 @@
+# Raspberry Pi 3
+```
+       _,met$$$$$gg.          jonas@raspberrypi
+    ,g$$$$$$$$$$$$$$$P.       -----------------
+  ,g$$P"     """Y$$.".        OS: Debian GNU/Linux 11 (bullseye) aarch64
+ ,$$P'              `$$$.     Host: Raspberry Pi 3 Model B Rev 1.2
+',$$P       ,ggs.     `$$b:   Kernel: 6.1.21-v8+
+`d$$'     ,$P"'   .    $$$    Uptime: 2 hours, 41 mins
+ $$P      d$'     ,    $$P    Packages: 660 (dpkg)
+ $$:      $$.   -    ,d$$'    Shell: bash 5.1.4
+ $$;      Y$b._   _,d$P'      Terminal: /dev/pts/0
+ Y$$.    `.`"Y$$$$P"'         CPU: BCM2835 (4) @ 1.200GHz
+ `$$b      "-.__              Memory: 82MiB / 909MiB
+  `Y$$
+   `Y$$.
+     `$$b.
+       `Y$$b.
+          `"Y$b._
+              `"""
+```
+
+## Client
+Client
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1:
+	Handshake: 7122 μs | 140.4094748062547 /s
+	Application: 244 μs | 63.7759811051013 MB/s
+	Message Sizes: 200, 838, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519:
+	Handshake: 4566 μs | 218.98451159470278 /s
+	Application: 245 μs | 63.71299735155773 MB/s
+	Message Sizes: 167, 805, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1:
+	Handshake: 21473 μs | 46.56802728954948 /s
+	Application: 254 μs | 61.3644019146746 MB/s
+	Message Sizes: 200, 2230, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519:
+	Handshake: 18850 μs | 53.05039006817865 /s
+	Application: 254 μs | 61.42504065826636 MB/s
+	Message Sizes: 167, 2197, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519Kyber768Draft00:
+	Handshake: 5582 μs | 179.1359595215902 /s
+	Application: 256 μs | 61.01392340465518 MB/s
+	Message Sizes: 1351, 1893, 58 bytes
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519MlKem768:
+	Handshake: 5487 μs | 182.24313662925482 /s
+	Application: 253 μs | 61.53509645857742 MB/s
+	Message Sizes: 1351, 1892, 58 bytes
+
+## Client Stack
+Client Stack Usage:
+===================
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1
+[Client Connect] Highest stack usage: 56.1 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519
+[Client Connect] Highest stack usage: 55.4 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1
+[Client Connect] Highest stack usage: 56.1 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519
+[Client Connect] Highest stack usage: 55.4 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519Kyber768Draft00
+[Client Connect] Highest stack usage: 78.2 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+Ciphersuite: TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519MlKem768
+[Client Connect] Highest stack usage: 78.2 KB
+[Client Read   ] Highest stack usage: 5.9 KB
+
+## Server
+Server
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | Secp256r1:
+	Handshake: 5481 μs | 182.43040791837637 /s
+	Application: 259 μs | 60.18269424576024 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ EcdsaSecp256r1Sha256 | X25519:
+	Handshake: 2819 μs | 354.63931635299485 /s
+	Application: 256 μs | 60.92005874557329 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | Secp256r1:
+	Handshake: 699193 μs | 1.430219917317012 /s
+	Application: 262 μs | 59.581248116755916 MB/s
+ - TLS_Chacha20Poly1305_SHA256 w/ RsaPssRsaSha256 | X25519:
+	Handshake: 694248 μs | 1.4404070652725713 /s
+	Application: 260 μs | 60.00107706253405 MB/s