ISO-DH Example

.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