ProVerif Handshake Model

Cargo.toml

@@ -18,12 +18,15 @@ rand = "0.8.0"
 hex = "0.4.3"
 tracing = "0.1"
 libcrux = { version = "0.0.2-pre.2", features = ["rand"] }
+hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
+
 
 [features]
 default = ["api"]
 test_utils = []
 secret_integers = []
 api = []             # The streaming Rust API that everyone should use but is not hacspec.
+hax-pv = ["dep:hax-lib-macros"]
 
 [dev-dependencies]
 bertie = { path = ".", features = ["test_utils"] }

hax-driver.py

@@ -37,7 +37,9 @@ def shell(command, expect=0, cwd=None, env={}):
 extract_parser = sub_parser.add_parser("extract")
 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")
 typecheck_proverif_parser = sub_parser.add_parser("typecheck-proverif")
+
 typecheck_parser.add_argument(
     "--lax",
     action="store_true",
@@ -108,16 +110,11 @@ def shell(command, expect=0, cwd=None, env={}):
             " ".join([
                 "-**",
                 "+~**::tls13handshake::**",
-                "+~**::server::lookup_db" #transitive dependency on tls13utils
+                "+~**::server::lookup_db", # to include transitive dependency on tls13utils
+                "+~**::tls13utils::parse_failed", # transitive dependencies required
+                "+~**::tls13crypto::zero_key", # transitive dependencies required
                 ]),
             "pro-verif",
-            "--assume-items",
-            " ".join([
-                "+**::tls13formats::**",
-                "+**::tls13crypto::**",
-                "+**::tls13utils::**",
-                "+**::tls13cert::**"
-            ])
         ],
         cwd=".",
         env=hax_env,
@@ -133,10 +130,15 @@ def shell(command, expect=0, cwd=None, env={}):
         shell(["make", "-C", "proofs/fstar/extraction/", "clean"])
     shell(["make", "-C", "proofs/fstar/extraction/"], env=custom_env)
     exit(0)
+elif options.sub == "patch-proverif":
+    custom_env = {}
+    shell(["patch", "proofs/proverif/extraction/lib.pvl", "proofs/proverif/patches/lib.patch"], env=custom_env)
+    shell(["patch", "proofs/proverif/extraction/analysis.pv", "proofs/proverif/patches/analysis.patch"], env=custom_env)
+    exit(0)
 elif options.sub == "typecheck-proverif":
     # Typecheck subcommand.
     custom_env = {}
-    shell(["proverif", "-lib", "proofs/proverif/extraction/handwritten_lib", "-lib", "proofs/proverif/extraction/lib", "proofs/proverif/extraction/analysis.pv"], env=custom_env)
+    shell(["proverif", "-lib", "proofs/proverif/handwritten_lib", "-lib", "proofs/proverif/extraction/lib", "proofs/proverif/extraction/analysis.pv"], env=custom_env)
     exit(0)
 else:
     parser.print_help()

proofs/proverif/handwritten_lib.pvl

@@ -0,0 +1,18 @@
+type impl_CryptoRng___RngCore.
+letfun rand_core__RngCore_f_fill_bytes(rng: impl_CryptoRng___RngCore, dest: bitstring) = new b: bitstring; (rng, b).
+
+fun rust_primitives__hax__repeat(nat, nat): bitstring.
+
+letfun core__ops__bit__Not__v_not(b: bool) = if b then false else true.
+letfun core__cmp__PartialOrd__ge(lhs: nat, rhs:nat ) = lhs >= rhs.
+
+
+type libcrux__digest__Algorithm.
+fun libcrux__digest__Algorithm_Algorithm_Sha256_c(): libcrux__digest__Algorithm [data].
+fun libcrux__digest__Algorithm_Algorithm_Sha384_c(): libcrux__digest__Algorithm [data].
+fun libcrux__digest__Algorithm_Algorithm_Sha512_c(): libcrux__digest__Algorithm [data].
+
+letfun libcrux__digest__digest_size(alg: libcrux__digest__Algorithm) =
+       let libcrux__digest__Algorithm_Algorithm_Sha256_c() = alg in 32
+       else let libcrux__digest__Algorithm_Algorithm_Sha384_c() = alg in 48
+       else let libcrux__digest__Algorithm_Algorithm_Sha512_c() = alg in 64.