ISO-DH Example (#36)

* Total and Stateful code of the DH model

* Updated comment

* Updated key usage in DH example

* Executable DH protocol run

* Adapted DH example to folder structure change in the main branch

* DH example trace and crypto predicates; DH security lemmas

* DH example add trace printing to debug protocol run

* DH example  compute_message1_proof and decode_message1_proof

* DH example compute_message2_proof and decode_message2_proof

* DH example compute_message3_proof and decode_message3_proof

* DH example add ifuel option to crypto preds

* DH example compatibility with main branch restored

* DH example finished stateful proofs

* Make DH example compatible with current main branch and clean up

* DH example: changed is_dh_shared_key definition to use `equivalent tr`

* DH example renamed folder to iso_dh and used 'equivalent tr' function in key_secrecy_lemma

* DH example added ISO reference

* DH example: changed names of security properties and added README.md

* DH example sanity check for trace invariants and proof refactoring

* DH example feedback Théophile

* DH example proof trace invariants for example trace with SMTPats

* cleanup: tighten ISO-DH invariants to simplify proofs

* DH example improved security properties and changed SMTPats for the stateful proof functions

* DH example move all crypto functions to the total code; cleanup code

* DH example feedback Théophile and code cleanup

* Updated README to include the ISO-DH example

* README changed path to ISO-DH example

* DH example updated README

* cleanup: rework some ISO-DH security proofs

---------

Co-authored-by: Théophile Wallez <[email protected]>

.fst.config.json

@@ -1,5 +1,5 @@
 { "fstar_exe":"fstar.exe",
   "options":["--cache_dir", "cache", "--hint_dir", "hints", "--use_hints", "--record_hints"],
   "include_dirs":[
-    "../comparse/src", "src/core", "src/lib", "src/lib/comparse", "src/lib/event", "src/lib/state", "src/lib/utils", "examples/nsl_pk"] 
+    "../comparse/src", "src/core", "src/lib", "src/lib/comparse", "src/lib/event", "src/lib/state", "src/lib/utils", "examples/nsl_pk", "examples/iso_dh"] 
 }

CONTRIBUTING.md

@@ -216,6 +216,9 @@ In general the `requires` is a big conjunction,
 each hypothesis should be on a separate line.
 The `ensures` often contains a `let`, a `match`,
 in that case extra parenthesis are needed for F\*'s parser.
+Defining variables with the `let` keyword should be 
+replaced by inlining the statement directly into the function that 
+requires the variable if it does not blow up the statement too much.
 
 When the lemma is very short, it may be written on one line.
 

Makefile

@@ -5,7 +5,7 @@ COMPARSE_HOME 	?= $(DY_HOME)/../comparse
 
 INNER_SOURCE_DIRS = core lib lib/comparse lib/event lib/state lib/utils
 SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS))
-INNER_EXAMPLE_DIRS = nsl_pk
+INNER_EXAMPLE_DIRS = nsl_pk iso_dh
 EXAMPLE_DIRS = $(addprefix $(DY_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 INCLUDE_DIRS = $(SOURCE_DIRS) $(EXAMPLE_DIRS) $(COMPARSE_HOME)/src

README.md

@@ -15,7 +15,8 @@ we can find functions and theorems built on top of [`DY.Core`](src/core/DY.Core.
 
 ### Examples
 
-The NSL protocol is proved secure in the namespace [`DY.Example.NSL`](examples/nsl_pk/DY.Example.NSL.SecurityProperties.fst).
+The NSL protocol has been proven secure in the namespace [`DY.Example.NSL`](examples/nsl_pk/DY.Example.NSL.SecurityProperties.fst), and the ISO-DH protocol has been
+proven secure in the namespace [`DY.Example.DH`](examples/iso_dh).
 
 ## How to build
 

examples/iso_dh/DY.Example.DH.Debug.Proof.fst

@@ -0,0 +1,30 @@
+module DY.Example.DH.Debug.Proof
+
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Stateful
+open DY.Example.DH.Protocol.Stateful.Proof
+open DY.Example.DH.Debug
+
+/// This module proves that the debug function
+/// fulfills the trace invariants.
+///
+/// The proof works automatically because each
+/// stateful proof as a SMTPat (`[SMTPat (trace_invariant tr); SMTPat (protocol_function)]`).
+/// Another way to do this proof is to basically
+/// duplicate the code from the debug function and
+/// call all the lemmas for the stateful code manually.
+
+#set-options "--fuel 0 --ifuel 0 --z3rlimit 10 --z3cliopt 'smt.qi.eager_threshold=100'"
+val debug_proof:
+  tr:trace ->
+  Lemma
+  (requires
+    trace_invariant tr
+  )
+  (ensures (
+    let (_, tr_out) = debug () tr in
+    trace_invariant tr_out
+    )
+  )
+let debug_proof tr = ()

examples/iso_dh/DY.Example.DH.Debug.fst

@@ -0,0 +1,67 @@
+module DY.Example.DH.Debug
+
+open DY.Core
+open DY.Lib
+open DY.Example.DH.Protocol.Stateful
+
+
+let debug () : traceful (option unit)  =
+  let _ = IO.debug_print_string "************* Trace *************\n" in
+  (*** Initialize protocol run ***)
+  let alice = "alice" in
+  let bob = "bob" in
+
+  // Generate private key for Alice
+  let* alice_global_session_priv_key_id = initialize_private_keys alice in
+  generate_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey");*
+
+  // Generate private key for Bob
+  let* bob_global_session_priv_key_id = initialize_private_keys bob in
+  generate_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey");*
+
+  // Store Bob's public key in Alice's state
+  // 1. Retrieve Bob's private key from his session
+  // 2. Compute the public key from the private key
+  // 3. Initialize Alice's session to store public keys
+  // 4. Install Bob's public key in Alice's public key store
+  let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey") in
+  let pub_key_bob = vk priv_key_bob in
+  let* alice_global_session_pub_key_id = initialize_pki alice in
+  install_public_key alice alice_global_session_pub_key_id (Verify "DH.SigningKey") bob pub_key_bob;*
+
+  // Store Alice's public key in Bob's state
+  let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey") in
+  let pub_key_alice = vk priv_key_alice in
+  let* bob_global_session_pub_key_id = initialize_pki bob in
+  install_public_key bob bob_global_session_pub_key_id (Verify "DH.SigningKey") alice pub_key_alice;*
+
+  let alice_global_session_ids: dh_global_sess_ids = {pki=alice_global_session_pub_key_id; private_keys=alice_global_session_priv_key_id} in
+  let bob_global_session_ids: dh_global_sess_ids = {pki=bob_global_session_pub_key_id; private_keys=bob_global_session_priv_key_id} in
+
+  (*** Run the protocol ***)
+  // Alice
+  let* alice_session_id = prepare_msg1 alice bob in
+  let*? msg1_id = send_msg1 alice alice_session_id in
+
+  // Bob
+  let*? bob_session_id = prepare_msg2 alice bob msg1_id in
+  let*? msg2_id = send_msg2 bob_global_session_ids bob bob_session_id in
+
+  // Alice
+  prepare_msg3 alice_global_session_ids alice alice_session_id bob msg2_id;*
+  let*? msg3_id = send_msg3 alice_global_session_ids alice bob alice_session_id in
+
+  // Bob
+  verify_msg3 bob_global_session_ids alice bob msg3_id bob_session_id;*
+
+  let* tr = get_trace in
+  let _ = IO.debug_print_string (
+      trace_to_string default_trace_to_string_printers tr
+    ) in
+
+  return (Some ())
+
+//Run ``debug ()`` when the module loads
+#push-options "--warn_error -272"
+let _ = debug () Nil
+#pop-options