From 3ae6570e1b84c66e635cc97434890f89c52f03d3 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Thu, 20 Feb 2025 10:50:51 +0100 Subject: [PATCH 01/16] online: minor cleanup --- examples/Online/DY.Online.Protocol.fst | 2 +- examples/Online/DY.Online.Run.Printing.fst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/Online/DY.Online.Protocol.fst b/examples/Online/DY.Online.Protocol.fst index 75ef21b..a28d5c9 100644 --- a/examples/Online/DY.Online.Protocol.fst +++ b/examples/Online/DY.Online.Protocol.fst @@ -9,7 +9,7 @@ open DY.Extend open DY.Online.Data -/// Here we define the DY* mode of the "Online?" protocol, +/// Here we define the DY* model of the "Online?" protocol, /// an extension of the simple Two-Message protocol: /// the two messages are now (asymmetrically) encrypted /// diff --git a/examples/Online/DY.Online.Run.Printing.fst b/examples/Online/DY.Online.Run.Printing.fst index 60faa8a..a15fabe 100644 --- a/examples/Online/DY.Online.Run.Printing.fst +++ b/examples/Online/DY.Online.Run.Printing.fst @@ -17,7 +17,7 @@ val message_to_string: bytes -> option string let message_to_string b = match? parse message_t b with | Ping p -> Some (Printf.sprintf "Ping [name = (%s), n_a = (%s)]" (p.alice) (bytes_to_string p.n_a)) - | Ack a -> Some (Printf.sprintf "Ping [n_a = (%s)]" (bytes_to_string a.n_a)) + | Ack a -> Some (Printf.sprintf "Ack [n_a = (%s)]" (bytes_to_string a.n_a)) val state_to_string: bytes -> option string From ac73e23f4860cabee1f2ba3ff2ccd4cd5f0605dc Mon Sep 17 00:00:00 2001 From: cwaldm Date: Thu, 20 Feb 2025 10:51:24 +0100 Subject: [PATCH 02/16] added first model of NSL (without properties; just steps and example trace) --- examples/NSL/DY.NSL.Data.fst | 125 ++++++++++++++++++++ examples/NSL/DY.NSL.Protocol.fst | 167 +++++++++++++++++++++++++++ examples/NSL/DY.NSL.Run.Printing.fst | 38 ++++++ examples/NSL/DY.NSL.Run.fst | 67 +++++++++++ examples/NSL/Makefile | 10 ++ 5 files changed, 407 insertions(+) create mode 100644 examples/NSL/DY.NSL.Data.fst create mode 100644 examples/NSL/DY.NSL.Protocol.fst create mode 100644 examples/NSL/DY.NSL.Run.Printing.fst create mode 100644 examples/NSL/DY.NSL.Run.fst create mode 100644 examples/NSL/Makefile diff --git a/examples/NSL/DY.NSL.Data.fst b/examples/NSL/DY.NSL.Data.fst new file mode 100644 index 0000000..7073dff --- /dev/null +++ b/examples/NSL/DY.NSL.Data.fst @@ -0,0 +1,125 @@ +module DY.NSL.Data + +open Comparse +open DY.Core +open DY.Lib + +/// Needham-Schroeder-Lowe Fixed Public Key Protocol [1] +/// +/// A -> B: {A, N_A}K_PB Msg 1 +/// B -> A: {B, N_A, N_B}K_PA Msg 2 -- note addition of B +/// A -> B: {N_B}K_PB Msg 3 +/// +/// [1] Gavin Lowe. "Breaking and fixing the Needham-Schroeder Public-Key +/// Protocol using FDR". TACAS, pp 147-166, 1996. +/// +/// Here, we define the abstract types for the NSL protocol. + +(*** Message Type ***) + +/// for each of the messages we define an abstract message type + +[@@ with_bytes bytes] +type message1_t = { + alice: principal; + n_a: bytes; +} + +[@@ with_bytes bytes] +type message2_t = { + bob: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type message3_t = { + n_b: bytes; +} + +/// the overall abstract message type +/// (consisting of constructors for the messages +/// and using the above abstract types for each of them) + +[@@ with_bytes bytes] +type message_t = + | Msg1: message1_t -> message_t + | Msg2: message2_t -> message_t + | Msg3: message3_t -> message_t + +/// Using Comparse to generate parser and serializer for the message type + +%splice [ps_message1_t] (gen_parser (`message1_t)) +%splice [ps_message2_t] (gen_parser (`message2_t)) +%splice [ps_message3_t] (gen_parser (`message3_t)) +%splice [ps_message_t] (gen_parser (`message_t)) + +instance parseable_serializeable_bytes_message: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t + +(*** State Type ***) + +/// As for the messages we define abstract state types +/// for the four states stored by Alice and Bob after each step of the protocol. + +[@@ with_bytes bytes] +type sent_msg1_t = { + bob: principal; + n_a: bytes; +} + +[@@ with_bytes bytes] +type sent_msg2_t = { + alice: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type sent_msg3_t = { + bob: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type received_msg3_t = { + alice: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type state_t = + | SentMsg1: (sentmsg1:sent_msg1_t) -> state_t + | SentMsg2: (sentmsg2:sent_msg2_t) -> state_t + | SentMsg3: sent_msg3_t -> state_t + | ReceivedMsg3: received_msg3_t -> state_t + +/// As for messages, we use Comparse to generate +/// a parser and serializer for our abstract state types. + +%splice [ps_sent_msg1_t] (gen_parser (`sent_msg1_t)) +%splice [ps_sent_msg2_t] (gen_parser (`sent_msg2_t)) +%splice [ps_sent_msg3_t] (gen_parser (`sent_msg3_t)) +%splice [ps_received_msg3_t] (gen_parser (`received_msg3_t)) +%splice [ps_state_t] (gen_parser (`state_t)) + +instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t + + +/// We tag our protocol level states, +/// so that they are distinguishable from any internal DY* states. + +instance local_state_state: local_state state_t = { + tag = "NSL.State"; + format = parseable_serializeable_bytes_state_t; +} + + +(*** PKI ***) + +/// Similarly as for states, +/// we tag the keys that are used on the protocol level, +/// so that they can not be confused with other keys. + +let key_tag = "NSL.Key" diff --git a/examples/NSL/DY.NSL.Protocol.fst b/examples/NSL/DY.NSL.Protocol.fst new file mode 100644 index 0000000..55052fb --- /dev/null +++ b/examples/NSL/DY.NSL.Protocol.fst @@ -0,0 +1,167 @@ +module DY.NSL.Protocol + +open Comparse +open DY.Core +open DY.Lib + +open DY.Simplified +open DY.Extend + +open DY.NSL.Data + +/// Here, we define the model of the +/// Needham-Schroeder-Lowe Fixed Public Key Protocol (NSL) +/// +/// A -> B: enc{A, N_A}_B Msg 1 +/// B -> A: enc{B, N_A, N_B}_A Msg 2 +/// A -> B: enc{N_B}_B Msg 3 +/// +/// The model consists of 4 function, +/// one for each protocol step: +/// 1. Alice sends the first message to Bob (`send_msg1`) +/// 2. Bob sends the second message to Alice (`send_msg2`) +/// 3. Alice sends the third message to Bob (`send_msg3`) +/// 4. Bob receives the third message from Alice (`receive_msg3`) + +(*** Sending the first message (Alice, n_a) ***) + +/// Alice sends the first message to Bob: +/// * Alice generates a new nonce [n_a] +/// * encrypts the message (Alice, n_a) for Bob +/// * sends the encrypted message +/// * stores n_a and Bob in a state (in a new session) +/// The step returns the ID of the new state +/// and the timestamp of the message on the trace +/// The step fails, if +/// encryption was not successful, i.e., +/// Alice does not have a public key of Bob. + +val send_msg1: principal -> principal -> state_id -> traceful (option (state_id & timestamp)) +let send_msg1 alice bob alice_public_keys_sid = + let* n_a = gen_rand in + + let msg1 = Msg1 {alice; n_a} in + let*? msg1_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg1 in + let* msg_ts = send_msg msg1_encrypted in + + let state = SentMsg1 {bob; n_a} in + let* sid = start_new_session alice state in + + return (Some (sid, msg_ts)) + +(*** Replying to a first message ***) + +/// Bob receives the first messages and replies: +/// * read the message from the trace +/// * decrypt the message to (Alice, n_a) +/// * generate a new nonce [n_b] +/// * encrypt the reply (Bob, n_a, n_b) for Alice +/// * send the encrypted reply +/// * store n_a, n_b and Alice in a state in a new session +/// The step returns the ID of the new state +/// and the timestamp of the reply on the trace. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a first message +/// * encryption fails (for example, if Bob doesn't have a public key for Alice) + +val receive_msg1_and_send_msg2: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) +let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts = + let*? msg = recv_msg msg_ts in + + let*? msg1_ = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg1? msg1_);*? + let Msg1 msg1 = msg1_ in + let alice = msg1.alice in + let n_a = msg1.n_a in + + let* n_b = gen_rand in + + let msg2 = Msg2 {bob; n_a; n_b} in + let*? msg2_encrypted = pke_enc_for bob alice bob_public_keys_sid key_tag msg2 in + let* msg2_ts = send_msg msg2_encrypted in + + let state = SentMsg2 {alice; n_a; n_b} in + let* sess_id = start_new_session bob state in + + return (Some (sess_id, msg2_ts)) + +(*** Sending the final message ***) + + +/// Alice receives the second messages and replies: +/// * read the message from the trace +/// * decrypt the message to (Bob, n_a, n_b) +/// * encrypt the reply (n_b) for Bob +/// * send the encrypted reply +/// * store n_a, n_b and Bob in a state in the session related to Bob and n_a +/// The step returns the ID of the new state +/// and the timestamp of the reply on the trace. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a first message +/// * encryption fails (for example, if Bob doesn't have a public key for Alice) +/// * there is no prior session related to Bob and n_a + +val receive_msg2_and_send_msg3: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) +let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts = + let*? msg = recv_msg msg_ts in + + let*? msg2_ = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag msg in + guard_tr (Msg2? msg2_);*? + let Msg2 msg2 = msg2_ in + let bob = msg2.bob in + let n_a = msg2.n_a in + let n_b = msg2.n_b in + + let*? (sid, st) = lookup_state #state_t alice + (fun st -> + SentMsg1? st + && (SentMsg1?.sentmsg1 st).n_a = n_a + && (SentMsg1?.sentmsg1 st).bob = bob + ) in + guard_tr(SentMsg1? st);*? + + + let msg3 = Msg3 {n_b} in + let*? msg3_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg3 in + let* msg3_ts = send_msg msg3_encrypted in + + let state = SentMsg3 {bob; n_a; n_b} in + set_state alice sid state;* + + return (Some (sid, msg3_ts)) + +(*** Receiving the final message ***) + +/// Bob receives the reply from Alice: +/// * read the message from the trace +/// * decrypt the message to (n_b) +/// * check if Bob previously sent n_b in some session +/// * store completion of this session in a new state +/// Returns the ID of the session that is marked as completed. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a reply +/// * there is no prior session related to n_a + +val receive_msg3: principal -> state_id -> timestamp -> traceful (option state_id) +let receive_msg3 bob bob_private_keys_sid msg3_ts = + let*? msg = recv_msg msg3_ts in + let*? msg3 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg3? msg3);*? + let Msg3 msg3 = msg3 in + let n_b = msg3.n_b in + + let*? (sid, st) = lookup_state #state_t bob + (fun st -> + SentMsg2? st + && (SentMsg2?.sentmsg2 st).n_b = n_b + ) in + guard_tr(SentMsg2? st);*? + let alice = (SentMsg2?.sentmsg2 st).alice in + let n_a = (SentMsg2?.sentmsg2 st).n_a in + + set_state alice sid (ReceivedMsg3 {alice; n_a; n_b});* + + return (Some sid) diff --git a/examples/NSL/DY.NSL.Run.Printing.fst b/examples/NSL/DY.NSL.Run.Printing.fst new file mode 100644 index 0000000..7712e72 --- /dev/null +++ b/examples/NSL/DY.NSL.Run.Printing.fst @@ -0,0 +1,38 @@ +module DY.NSL.Run.Printing + +open DY.Core +open DY.Lib +open Comparse + +open DY.Simplified + +open DY.NSL.Data + +/// Helper functions for trace printing. +/// Here we define how our abstract message and state types +/// should be printed. + + +val message_to_string: bytes -> option string +let message_to_string b = + match? parse message_t b with + | Msg1 m -> Some (Printf.sprintf "Msg1 [name = (%s), n_a = (%s)]" (m.alice) (bytes_to_string m.n_a)) + | Msg2 m -> Some (Printf.sprintf "Msg2 [name = (%s), n_a = (%s), n_b = (%s)]" (m.bob) (bytes_to_string m.n_a) (bytes_to_string m.n_b)) + | Msg3 m -> Some (Printf.sprintf "Msg3 [n_b = (%s)]" (bytes_to_string m.n_b)) + + +val state_to_string: bytes -> option string +let state_to_string b = + match? parse state_t b with + | SentMsg1 s -> Some (Printf.sprintf "SentMsg1 [n_a = (%s), to = (%s)]" (bytes_to_string s.n_a) s.bob) + | SentMsg2 s -> Some (Printf.sprintf "SentMsg2 [n_a = (%s), n_b = (%s), to = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.alice) + | SentMsg3 s -> Some (Printf.sprintf "SentMsg3 [n_a = (%s), n_b = (%s), to = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.bob) + | ReceivedMsg3 s -> Some (Printf.sprintf "ReceivedMsg3 [n_a = (%s), n_b = (%s), from = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.alice) + + +val get_trace_to_string_printers: trace_to_string_printers +let get_trace_to_string_printers = + trace_to_string_printers_builder + message_to_string + ((local_state_state.tag, state_to_string) :: default_state_to_string) + [] diff --git a/examples/NSL/DY.NSL.Run.fst b/examples/NSL/DY.NSL.Run.fst new file mode 100644 index 0000000..eb11934 --- /dev/null +++ b/examples/NSL/DY.NSL.Run.fst @@ -0,0 +1,67 @@ +module DY.NSL.Run + +open DY.Core +open DY.Lib + +open DY.Simplified + +open DY.NSL.Run.Printing +open DY.NSL.Data +open DY.NSL.Protocol + +/// Here, we print the trace after a successful run of the NSL protocol. + + +let run () : traceful (option unit ) = + let _ = IO.debug_print_string "************* Trace *************\n" in + + (*** Protocol Setup ***) + + // the names of the participants + let alice = "Alice" in + let bob = "Bob" in + + (*** PKI setup ***) + + // Initialize key storage for Alice + // private and public keys are stored in separate sessions + let* alice_private_keys_sid = initialize_private_keys alice in + let* alice_public_keys_sid = initialize_pki alice in + + // Initialize key storage for Bob + let* bob_private_keys_sid = initialize_private_keys bob in + let* bob_public_keys_sid = initialize_pki bob in + + // Generate private key for Alice and store it in her private keys session + generate_private_pke_key alice alice_private_keys_sid key_tag;* + + // Generate private key for Bob and store it in his private keys session + generate_private_pke_key bob bob_private_keys_sid key_tag;* + + // Store Bob's public key in Alice's state + install_public_pke_key alice alice_public_keys_sid key_tag bob bob_private_keys_sid;* + + // Store Alice's public key in Bob's state + install_public_pke_key bob bob_public_keys_sid key_tag alice alice_private_keys_sid;* + + (*** The actual protocol run ***) + + // Alice sends a Ping to Bob + let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in + // Bob replies with an Ack (reading the ping at the given timestamp) + let*? (bob_sid, msg2_ts) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg1_ts in + let*? (bob_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in + // Alice receives the Ack (at the given ack timestamp) + receive_msg3 bob bob_private_keys_sid msg3_ts;*? + + + (*** Printing the Trace ***) + + let* tr = get_trace in + let _ = IO.debug_print_string ( + trace_to_string get_trace_to_string_printers tr + ) in + + return (Some ()) + +let _ = run () empty_trace diff --git a/examples/NSL/Makefile b/examples/NSL/Makefile new file mode 100644 index 0000000..71d7a99 --- /dev/null +++ b/examples/NSL/Makefile @@ -0,0 +1,10 @@ +TUTORIAL_HOME ?= ../.. + +EXAMPLES = NSL +EXAMPLE_DIRS = $(addprefix $(TUTORIAL_HOME)/examples/, $(EXAMPLES)) + +include $(TUTORIAL_HOME)/Makefile + +test: + cd $(TUTORIAL_HOME)/obj; $(FSTAR_EXE) --ocamlenv ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib DY_NSL_Run.native + $(TUTORIAL_HOME)/obj/DY_NSL_Run.native From e0b31c891f1660158456a7470d51133f565c5ff6 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Thu, 20 Feb 2025 10:52:25 +0100 Subject: [PATCH 03/16] added NSL to global makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c6961c3..ce491b2 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ INNER_SOURCE_DIRS = dy-extensions # SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS)) SOURCE_DIRS = $(addprefix $(TUTORIAL_HOME)/, $(INNER_SOURCE_DIRS)) -INNER_EXAMPLE_DIRS = nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy +INNER_EXAMPLE_DIRS = NSL nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS)) From 2fdbe9dd704217ca329368c5ec679f37cd15a407 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Fri, 21 Feb 2025 09:33:20 +0100 Subject: [PATCH 04/16] nsl properties - added events to protocol --- Makefile | 2 +- examples/NSL_with_properties/DY.NSLP.Data.fst | 186 ++++++++++++++++++ .../NSL_with_properties/DY.NSLP.Protocol.fst | 177 +++++++++++++++++ .../DY.NSLP.Run.Printing.fst | 47 +++++ examples/NSL_with_properties/DY.NSLP.Run.fst | 67 +++++++ examples/NSL_with_properties/Makefile | 10 + 6 files changed, 488 insertions(+), 1 deletion(-) create mode 100644 examples/NSL_with_properties/DY.NSLP.Data.fst create mode 100644 examples/NSL_with_properties/DY.NSLP.Protocol.fst create mode 100644 examples/NSL_with_properties/DY.NSLP.Run.Printing.fst create mode 100644 examples/NSL_with_properties/DY.NSLP.Run.fst create mode 100644 examples/NSL_with_properties/Makefile diff --git a/Makefile b/Makefile index ce491b2..a7f0b67 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ INNER_SOURCE_DIRS = dy-extensions # SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS)) SOURCE_DIRS = $(addprefix $(TUTORIAL_HOME)/, $(INNER_SOURCE_DIRS)) -INNER_EXAMPLE_DIRS = NSL nsl_pk_only_one_event_lookup TwoMessageP Online Online_with_secrecy +INNER_EXAMPLE_DIRS = NSL NSL_with_properties TwoMessageP Online Online_with_secrecy EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS)) diff --git a/examples/NSL_with_properties/DY.NSLP.Data.fst b/examples/NSL_with_properties/DY.NSLP.Data.fst new file mode 100644 index 0000000..6bc46ed --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Data.fst @@ -0,0 +1,186 @@ +module DY.NSLP.Data + +open Comparse +open DY.Core +open DY.Lib + +/// Needham-Schroeder-Lowe Fixed Public Key Protocol [1] +/// +/// A -> B: {A, N_A}K_PB Msg 1 +/// B -> A: {B, N_A, N_B}K_PA Msg 2 -- note addition of B +/// A -> B: {N_B}K_PB Msg 3 +/// +/// [1] Gavin Lowe. "Breaking and fixing the Needham-Schroeder Public-Key +/// Protocol using FDR". TACAS, pp 147-166, 1996. +/// +/// Here, we define the abstract types for the NSL protocol. + +(*** Message Type ***) + +/// for each of the messages we define an abstract message type + +[@@ with_bytes bytes] +type message1_t = { + alice: principal; + n_a: bytes; +} + +[@@ with_bytes bytes] +type message2_t = { + bob: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type message3_t = { + n_b: bytes; +} + +/// the overall abstract message type +/// (consisting of constructors for the messages +/// and using the above abstract types for each of them) + +[@@ with_bytes bytes] +type message_t = + | Msg1: message1_t -> message_t + | Msg2: message2_t -> message_t + | Msg3: message3_t -> message_t + +/// Using Comparse to generate parser and serializer for the message type + +%splice [ps_message1_t] (gen_parser (`message1_t)) +%splice [ps_message2_t] (gen_parser (`message2_t)) +%splice [ps_message3_t] (gen_parser (`message3_t)) +%splice [ps_message_t] (gen_parser (`message_t)) + +instance parseable_serializeable_bytes_message: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t + +(*** State Type ***) + +/// As for the messages we define abstract state types +/// for the four states stored by Alice and Bob after each step of the protocol. + +[@@ with_bytes bytes] +type sent_msg1_t = { + bob: principal; + n_a: bytes; +} + +[@@ with_bytes bytes] +type sent_msg2_t = { + alice: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type sent_msg3_t = { + bob: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type received_msg3_t = { + alice: principal; + n_a: bytes; + n_b: bytes; +} + +[@@ with_bytes bytes] +type state_t = + | SentMsg1: (sentmsg1:sent_msg1_t) -> state_t + | SentMsg2: (sentmsg2:sent_msg2_t) -> state_t + | SentMsg3: sent_msg3_t -> state_t + | ReceivedMsg3: received_msg3_t -> state_t + +/// As for messages, we use Comparse to generate +/// a parser and serializer for our abstract state types. + +%splice [ps_sent_msg1_t] (gen_parser (`sent_msg1_t)) +%splice [ps_sent_msg2_t] (gen_parser (`sent_msg2_t)) +%splice [ps_sent_msg3_t] (gen_parser (`sent_msg3_t)) +%splice [ps_received_msg3_t] (gen_parser (`received_msg3_t)) +%splice [ps_state_t] (gen_parser (`state_t)) + +instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes state_t = mk_parseable_serializeable ps_state_t + + +/// We tag our protocol level states, +/// so that they are distinguishable from any internal DY* states. + +instance local_state_state: local_state state_t = { + tag = "NSL.State"; + format = parseable_serializeable_bytes_state_t; +} + + +(*** PKI ***) + +/// Similarly as for states, +/// we tag the keys that are used on the protocol level, +/// so that they can not be confused with other keys. + +let key_tag = "NSL.Key" + +(*** Event type ***) + +/// We have one event per protocol step: +/// * an Initiating event, +/// that Alice triggers, when she starts a new run +/// * a Responding1 event, +/// that Bob triggers, when he replies to a first message +/// * a Responding2 event, +/// that Alice triggers, when she replies to a second message +/// * a Finishing event, +/// that Bob triggers, when he receives a final message and finishes the run. + +[@@ with_bytes bytes] +type ev_init_t = { + alice:principal; + bob:principal; + n_a:bytes +} + +[@@ with_bytes bytes] +type ev_respond1_t = { + alice:principal; + bob:principal; + n_a:bytes; + n_b:bytes +} + +[@@ with_bytes bytes] +type ev_respond2_t = { + alice:principal; + bob:principal; + n_a:bytes; + n_b:bytes +} + +[@@ with_bytes bytes] +type ev_finish_t = { + alice:principal; + bob:principal; + n_a:bytes; + n_b:bytes +} + +[@@ with_bytes bytes] +type event_t = + | Initiating: ev_init_t -> event_t + | Responding1: ev_respond1_t -> event_t + | Responding2: ev_respond2_t -> event_t + | Finishing: ev_finish_t -> event_t + +%splice [ps_ev_init_t] (gen_parser (`ev_init_t)) +%splice [ps_ev_respond1_t] (gen_parser (`ev_respond1_t)) +%splice [ps_ev_respond2_t] (gen_parser (`ev_respond2_t)) +%splice [ps_ev_finish_t] (gen_parser (`ev_finish_t)) +%splice [ps_event_t] (gen_parser (`event_t)) + +instance event_event_t: event event_t = { + tag = "NSL.Event"; + format = mk_parseable_serializeable ps_event_t; +} diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst new file mode 100644 index 0000000..fd24b68 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -0,0 +1,177 @@ +module DY.NSLP.Protocol + +open Comparse +open DY.Core +open DY.Lib + +open DY.Simplified +open DY.Extend + +open DY.NSLP.Data + +/// Here, we define the model of the +/// Needham-Schroeder-Lowe Fixed Public Key Protocol (NSL) +/// +/// A -> B: enc{A, N_A}_B Msg 1 +/// B -> A: enc{B, N_A, N_B}_A Msg 2 +/// A -> B: enc{N_B}_B Msg 3 +/// +/// The model consists of 4 function, +/// one for each protocol step: +/// 1. Alice sends the first message to Bob (`send_msg1`) +/// 2. Bob sends the second message to Alice (`send_msg2`) +/// 3. Alice sends the third message to Bob (`send_msg3`) +/// 4. Bob receives the third message from Alice (`receive_msg3`) + +(*** Sending the first message (Alice, n_a) ***) + +/// Alice sends the first message to Bob: +/// * Alice generates a new nonce [n_a] +/// * encrypts the message (Alice, n_a) for Bob +/// * sends the encrypted message +/// * stores n_a and Bob in a state (in a new session) +/// The step returns the ID of the new state +/// and the timestamp of the message on the trace +/// The step fails, if +/// encryption was not successful, i.e., +/// Alice does not have a public key of Bob. + +let nonce_label alice bob = join (principal_label alice) (principal_label bob) + +val send_msg1: principal -> principal -> state_id -> traceful (option (state_id & timestamp)) +let send_msg1 alice bob alice_public_keys_sid = + let* n_a = gen_rand_labeled (nonce_label alice bob) in + + trigger_event alice (Initiating {alice; bob; n_a});* + + let msg1 = Msg1 {alice; n_a} in + let*? msg1_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg1 in + let* msg_ts = send_msg msg1_encrypted in + + let state = SentMsg1 {bob; n_a} in + let* sid = start_new_session alice state in + + return (Some (sid, msg_ts)) + +(*** Replying to a first message ***) + +/// Bob receives the first messages and replies: +/// * read the message from the trace +/// * decrypt the message to (Alice, n_a) +/// * generate a new nonce [n_b] +/// * encrypt the reply (Bob, n_a, n_b) for Alice +/// * send the encrypted reply +/// * store n_a, n_b and Alice in a state in a new session +/// The step returns the ID of the new state +/// and the timestamp of the reply on the trace. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a first message +/// * encryption fails (for example, if Bob doesn't have a public key for Alice) + +val receive_msg1_and_send_msg2: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) +let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts = + let*? msg = recv_msg msg_ts in + + let*? msg1_ = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg1? msg1_);*? + let Msg1 msg1 = msg1_ in + let alice = msg1.alice in + let n_a = msg1.n_a in + + let* n_b = gen_rand_labeled (nonce_label alice bob) in + + let msg2 = Msg2 {bob; n_a; n_b} in + let*? msg2_encrypted = pke_enc_for bob alice bob_public_keys_sid key_tag msg2 in + let* msg2_ts = send_msg msg2_encrypted in + + trigger_event bob (Responding1 {alice; bob; n_a; n_b});* + + let state = SentMsg2 {alice; n_a; n_b} in + let* sess_id = start_new_session bob state in + + return (Some (sess_id, msg2_ts)) + +(*** Sending the final message ***) + + +/// Alice receives the second messages and replies: +/// * read the message from the trace +/// * decrypt the message to (Bob, n_a, n_b) +/// * encrypt the reply (n_b) for Bob +/// * send the encrypted reply +/// * store n_a, n_b and Bob in a state in the session related to Bob and n_a +/// The step returns the ID of the new state +/// and the timestamp of the reply on the trace. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a first message +/// * encryption fails (for example, if Bob doesn't have a public key for Alice) +/// * there is no prior session related to Bob and n_a + +val receive_msg2_and_send_msg3: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) +let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts = + let*? msg = recv_msg msg_ts in + + let*? msg2_ = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag msg in + guard_tr (Msg2? msg2_);*? + let Msg2 msg2 = msg2_ in + let bob = msg2.bob in + let n_a = msg2.n_a in + let n_b = msg2.n_b in + + let*? (sid, st) = lookup_state #state_t alice + (fun st -> + SentMsg1? st + && (SentMsg1?.sentmsg1 st).n_a = n_a + && (SentMsg1?.sentmsg1 st).bob = bob + ) in + guard_tr(SentMsg1? st);*? + + + let msg3 = Msg3 {n_b} in + let*? msg3_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg3 in + let* msg3_ts = send_msg msg3_encrypted in + + trigger_event alice (Responding2 {alice; bob; n_a; n_b});* + + let state = SentMsg3 {bob; n_a; n_b} in + set_state alice sid state;* + + return (Some (sid, msg3_ts)) + +(*** Receiving the final message ***) + +/// Bob receives the reply from Alice: +/// * read the message from the trace +/// * decrypt the message to (n_b) +/// * check if Bob previously sent n_b in some session +/// * store completion of this session in a new state +/// Returns the ID of the session that is marked as completed. +/// The step fails, if one of +/// * decryption fails +/// * the message is not of the right type, i.e., not a reply +/// * there is no prior session related to n_a + +val receive_msg3: principal -> state_id -> timestamp -> traceful (option state_id) +let receive_msg3 bob bob_private_keys_sid msg3_ts = + let*? msg = recv_msg msg3_ts in + let*? msg3 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg3? msg3);*? + let Msg3 msg3 = msg3 in + let n_b = msg3.n_b in + + let*? (sid, st) = lookup_state #state_t bob + (fun st -> + SentMsg2? st + && (SentMsg2?.sentmsg2 st).n_b = n_b + ) in + guard_tr(SentMsg2? st);*? + let alice = (SentMsg2?.sentmsg2 st).alice in + let n_a = (SentMsg2?.sentmsg2 st).n_a in + + trigger_event bob (Finishing {alice; bob; n_a; n_b});* + + set_state alice sid (ReceivedMsg3 {alice; n_a; n_b});* + + return (Some sid) diff --git a/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst b/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst new file mode 100644 index 0000000..9662b6d --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst @@ -0,0 +1,47 @@ +module DY.NSLP.Run.Printing + +open DY.Core +open DY.Lib +open Comparse + +open DY.Simplified + +open DY.NSLP.Data + +/// Helper functions for trace printing. +/// Here we define how our abstract message and state types +/// should be printed. + + +val message_to_string: bytes -> option string +let message_to_string b = + match? parse message_t b with + | Msg1 m -> Some (Printf.sprintf "Msg1 [name = (%s), n_a = (%s)]" (m.alice) (bytes_to_string m.n_a)) + | Msg2 m -> Some (Printf.sprintf "Msg2 [name = (%s), n_a = (%s), n_b = (%s)]" (m.bob) (bytes_to_string m.n_a) (bytes_to_string m.n_b)) + | Msg3 m -> Some (Printf.sprintf "Msg3 [n_b = (%s)]" (bytes_to_string m.n_b)) + + +val state_to_string: bytes -> option string +let state_to_string b = + match? parse state_t b with + | SentMsg1 s -> Some (Printf.sprintf "SentMsg1 [n_a = (%s), to = (%s)]" (bytes_to_string s.n_a) s.bob) + | SentMsg2 s -> Some (Printf.sprintf "SentMsg2 [n_a = (%s), n_b = (%s), to = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.alice) + | SentMsg3 s -> Some (Printf.sprintf "SentMsg3 [n_a = (%s), n_b = (%s), to = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.bob) + | ReceivedMsg3 s -> Some (Printf.sprintf "ReceivedMsg3 [n_a = (%s), n_b = (%s), from = (%s)]" (bytes_to_string s.n_a) (bytes_to_string s.n_b) s.alice) + +val event_to_string: bytes -> option string +let event_to_string b = + match? parse event_t b with + | Initiating {alice; bob; n_a} -> Some (Printf.sprintf "Initiating [alice = (%s), n_a = (%s), with = (%s)]" alice (bytes_to_string n_a) bob) + | Responding1 {alice; bob; n_a; n_b} -> Some (Printf.sprintf "Responding1 [bob = (%s), n_a = (%s), n_b = (%s), to = (%s)]" bob (bytes_to_string n_a) (bytes_to_string n_b) alice) + | Responding2 {alice; bob; n_a; n_b} -> Some (Printf.sprintf "Responding2 [alice = (%s), n_a = (%s), n_b = (%s), to = (%s)]" alice (bytes_to_string n_a) (bytes_to_string n_b) bob) + | Finishing {alice; bob; n_a; n_b} -> Some (Printf.sprintf "Finishing [bob = (%s), n_a = (%s), n_b = (%s), with = (%s)]" bob (bytes_to_string n_a) (bytes_to_string n_b) alice) + + + +val get_trace_to_string_printers: trace_to_string_printers +let get_trace_to_string_printers = + trace_to_string_printers_builder + message_to_string + ((local_state_state.tag, state_to_string) :: default_state_to_string) + [(event_event_t.tag, event_to_string)] diff --git a/examples/NSL_with_properties/DY.NSLP.Run.fst b/examples/NSL_with_properties/DY.NSLP.Run.fst new file mode 100644 index 0000000..3085893 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Run.fst @@ -0,0 +1,67 @@ +module DY.NSLP.Run + +open DY.Core +open DY.Lib + +open DY.Simplified + +open DY.NSLP.Run.Printing +open DY.NSLP.Data +open DY.NSLP.Protocol + +/// Here, we print the trace after a successful run of the NSL protocol. + + +let run () : traceful (option unit ) = + let _ = IO.debug_print_string "************* Trace *************\n" in + + (*** Protocol Setup ***) + + // the names of the participants + let alice = "Alice" in + let bob = "Bob" in + + (*** PKI setup ***) + + // Initialize key storage for Alice + // private and public keys are stored in separate sessions + let* alice_private_keys_sid = initialize_private_keys alice in + let* alice_public_keys_sid = initialize_pki alice in + + // Initialize key storage for Bob + let* bob_private_keys_sid = initialize_private_keys bob in + let* bob_public_keys_sid = initialize_pki bob in + + // Generate private key for Alice and store it in her private keys session + generate_private_pke_key alice alice_private_keys_sid key_tag;* + + // Generate private key for Bob and store it in his private keys session + generate_private_pke_key bob bob_private_keys_sid key_tag;* + + // Store Bob's public key in Alice's state + install_public_pke_key alice alice_public_keys_sid key_tag bob bob_private_keys_sid;* + + // Store Alice's public key in Bob's state + install_public_pke_key bob bob_public_keys_sid key_tag alice alice_private_keys_sid;* + + (*** The actual protocol run ***) + + // Alice sends a Ping to Bob + let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in + // Bob replies with an Ack (reading the ping at the given timestamp) + let*? (bob_sid, msg2_ts) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg1_ts in + let*? (bob_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in + // Alice receives the Ack (at the given ack timestamp) + receive_msg3 bob bob_private_keys_sid msg3_ts;*? + + + (*** Printing the Trace ***) + + let* tr = get_trace in + let _ = IO.debug_print_string ( + trace_to_string get_trace_to_string_printers tr + ) in + + return (Some ()) + +let _ = run () empty_trace diff --git a/examples/NSL_with_properties/Makefile b/examples/NSL_with_properties/Makefile new file mode 100644 index 0000000..59f3b4e --- /dev/null +++ b/examples/NSL_with_properties/Makefile @@ -0,0 +1,10 @@ +TUTORIAL_HOME ?= ../.. + +EXAMPLES = NSL_with_properties +EXAMPLE_DIRS = $(addprefix $(TUTORIAL_HOME)/examples/, $(EXAMPLES)) + +include $(TUTORIAL_HOME)/Makefile + +test: + cd $(TUTORIAL_HOME)/obj; $(FSTAR_EXE) --ocamlenv ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib DY_NSLP_Run.native + $(TUTORIAL_HOME)/obj/DY_NSLP_Run.native From 375786cfa837872866cb2522f95d07b670908a89 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Fri, 21 Feb 2025 10:26:09 +0100 Subject: [PATCH 05/16] nsl: added invariants and properties --- .../DY.NSLP.Invariants.fst | 200 ++++++++++++++++++ .../DY.NSLP.Properties.fst | 92 ++++++++ 2 files changed, 292 insertions(+) create mode 100644 examples/NSL_with_properties/DY.NSLP.Invariants.fst create mode 100644 examples/NSL_with_properties/DY.NSLP.Properties.fst diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst new file mode 100644 index 0000000..90c63b4 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -0,0 +1,200 @@ +module DY.NSLP.Invariants + +open Comparse +open DY.Core +open DY.Lib +open DY.Extend + +open DY.NSLP.Data +open DY.NSLP.Protocol + +#set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" + +/// This module defines the protocol invariants, +/// consisting of: +/// * the crypto invariants +/// * trace invariants: +/// * state invariants +/// * event invariants + +(*** Crypto Invariants ***) + +%splice [ps_message1_t_is_well_formed] (gen_is_well_formed_lemma (`message1_t)) +%splice [ps_message2_t_is_well_formed] (gen_is_well_formed_lemma (`message2_t)) +%splice [ps_message3_t_is_well_formed] (gen_is_well_formed_lemma (`message3_t)) +%splice [ps_message_t_is_well_formed] (gen_is_well_formed_lemma (`message_t)) + +instance crypto_usages_nsl : crypto_usages = default_crypto_usages + +#push-options "--ifuel 3 --fuel 0" +val crypto_predicates_nsl: crypto_predicates +let crypto_predicates_nsl = { + default_crypto_predicates with + pke_pred = { + pred = (fun tr sk_usage pk msg -> + (exists prin. + sk_usage == long_term_key_type_to_usage (LongTermPkeKey key_tag) prin /\ + (match parse message_t msg with + | Some (Msg1 {alice; n_a}) -> ( + let bob = prin in + get_label tr n_a == nonce_label alice bob /\ + event_triggered tr alice (Initiating {alice; bob; n_a}) + ) + | Some (Msg2 {bob; n_a; n_b}) -> ( + let alice = prin in + get_label tr n_b == nonce_label alice bob /\ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) + ) + | Some (Msg3 {n_b}) -> ( + let bob = prin in + exists alice n_a. + get_label tr n_b `can_flow tr` (nonce_label alice bob) /\ + event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) + ) + | None -> False + )) + ); + pred_later = (fun tr1 tr2 sk_usage pk msg -> + parse_wf_lemma message_t (bytes_well_formed tr1) msg + ); + }; +} +#pop-options + + + +instance crypto_invariants_nsl: crypto_invariants = { + usages = crypto_usages_nsl; + preds = crypto_predicates_nsl +} + + +(*** State Invariant ***) + +%splice [ps_sent_msg1_t_is_well_formed] (gen_is_well_formed_lemma (`sent_msg1_t)) +%splice [ps_sent_msg2_t_is_well_formed] (gen_is_well_formed_lemma (`sent_msg2_t)) +%splice [ps_sent_msg3_t_is_well_formed] (gen_is_well_formed_lemma (`sent_msg3_t)) +%splice [ps_received_msg3_t_is_well_formed] (gen_is_well_formed_lemma (`received_msg3_t)) +%splice [ps_state_t_is_well_formed] (gen_is_well_formed_lemma (`state_t)) + +/// The (local) state predicate. + +#push-options "--ifuel 2" +let state_predicate_nsl: local_state_predicate state_t = { + pred = (fun tr prin sess_id st -> + match st with + | SentMsg1 {bob; n_a} -> ( + let alice = prin in + is_knowable_by (nonce_label alice bob) tr n_a /\ + event_triggered tr alice (Initiating {alice; bob; n_a}) + ) + | SentMsg2 {alice; n_a; n_b} -> ( + let bob = prin in + is_knowable_by (nonce_label alice bob) tr n_a /\ + is_knowable_by (nonce_label alice bob) tr n_b /\ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) + ) + | SentMsg3 {bob; n_a; n_b} -> ( + let alice = prin in + is_knowable_by (nonce_label alice bob) tr n_a /\ + is_knowable_by (nonce_label alice bob) tr n_b /\ + event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) + ) + | ReceivedMsg3 {alice; n_a; n_b} -> ( + let bob = prin in + is_knowable_by (nonce_label alice bob) tr n_a /\ + is_knowable_by (nonce_label alice bob) tr n_b /\ + event_triggered tr bob (Finishing {alice; bob; n_a; n_b} ) + ) + ); + pred_later = (fun tr1 tr2 prin sess_id st -> ()); + pred_knowable = (fun tr prin sess_id st -> ()); +} +#pop-options + +(*** Event Predicate ***) + + +let event_predicate_nsl: event_predicate event_t = + fun tr prin e -> + match e with + | Initiating {alice; bob; n_a} -> ( + prin == alice /\ + is_secret (nonce_label alice bob) tr n_a /\ + rand_just_generated tr n_a + ) + | Responding1 {alice; bob; n_a; n_b} -> ( + prin == bob /\ + is_secret (nonce_label alice bob) tr n_b /\ + rand_just_generated tr n_b + ) + | Responding2 {alice; bob; n_a; n_b} -> ( + prin == alice /\ + event_triggered tr alice (Initiating {alice; bob; n_a}) /\ ( + is_corrupt tr (nonce_label alice bob) \/ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) + ) + ) + | Finishing {alice; bob; n_a; n_b} -> ( + prin == bob /\ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) /\ ( + is_corrupt tr (nonce_label alice bob) \/ + event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) + ) + ) + +/// List of all local state predicates. + +let all_sessions = [ + pki_tag_and_invariant; + private_keys_tag_and_invariant; + (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_nsl|); +] + +/// List of all local event predicates. + +let all_events = [ + (event_event_t.tag, compile_event_pred event_predicate_nsl) +] + +/// Create the global trace invariants. + +let trace_invariants_nsl: trace_invariants = { + state_pred = mk_state_pred all_sessions; + event_pred = mk_event_pred all_events; +} + +instance protocol_invariants_nsl: protocol_invariants = { + crypto_invs = crypto_invariants_nsl; + trace_invs = trace_invariants_nsl; +} + +/// Lemmas that the global state predicate contains all the local ones + +val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate #protocol_invariants_nsl) all_sessions)) +let all_sessions_has_all_sessions () = + assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_sessions))); + mk_state_pred_correct #protocol_invariants_nsl all_sessions; + norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate #protocol_invariants_nsl) all_sessions) + +val protocol_invariants_nsl_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_nsl) +let protocol_invariants_nsl_has_pki_invariant = all_sessions_has_all_sessions () + +val protocol_invariants_nsl_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_nsl) +let protocol_invariants_nsl_has_private_keys_invariant = all_sessions_has_all_sessions () + +val protocol_invariants_nsl_has_nsl_session_invariant: squash (has_local_state_predicate state_predicate_nsl) +let protocol_invariants_nsl_has_nsl_session_invariant = all_sessions_has_all_sessions () + +/// Lemmas that the global event predicate contains all the local ones + +val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events)) +let all_events_has_all_events () = + assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events))); + mk_event_pred_correct #protocol_invariants_nsl all_events; + norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events); + let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in + dumb_lemma (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events)) + +val protocol_invariants_nsl_has_nsl_event_invariant: squash (has_event_pred event_predicate_nsl) +let protocol_invariants_nsl_has_nsl_event_invariant = all_events_has_all_events () diff --git a/examples/NSL_with_properties/DY.NSLP.Properties.fst b/examples/NSL_with_properties/DY.NSLP.Properties.fst new file mode 100644 index 0000000..1a88f23 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -0,0 +1,92 @@ +module DY.NSLP.Properties + +open Comparse +open DY.Core +open DY.Lib +open DY.Extend +open DY.Simplified + +open DY.NSLP.Data +open DY.NSLP.Invariants + +#set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" + +/// This module defines the security properties of the NSL protocol: +/// * secrecy of both nonces +/// * authentication of both participants + + +/// The nonce n_a is unknown to the attacker, +/// unless the attacker corrupted Alice or Bob. + +val n_a_secrecy: + tr:trace -> alice:principal -> bob:principal -> n_a:bytes -> + Lemma + (requires + attacker_knows tr n_a /\ + trace_invariant tr /\ ( + (state_was_set_some_id tr alice (SentMsg1 {bob; n_a})) \/ + (exists n_b. state_was_set_some_id tr alice (SentMsg3 {bob; n_a; n_b})) \/ + (exists n_b. state_was_set_some_id tr bob (ReceivedMsg3 {alice; n_a; n_b})) + ) + ) + (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob) +let n_a_secrecy tr alice bob n_a = + attacker_only_knows_publishable_values tr n_a + +/// The nonce n_b is unknown to the attacker, +/// unless the attacker corrupted Alice or Bob. + +val n_b_secrecy: + tr:trace -> alice:principal -> bob:principal -> n_b:bytes -> + Lemma + (requires + attacker_knows tr n_b /\ + trace_invariant tr /\ ( + (exists n_a. state_was_set_some_id tr bob (SentMsg2 {alice; n_a; n_b})) \/ + (exists n_a. state_was_set_some_id tr bob (ReceivedMsg3 {alice; n_a; n_b})) \/ + (exists n_a. state_was_set_some_id tr alice (SentMsg3 {bob; n_a; n_b})) + ) + ) + (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob) +let n_b_secrecy tr alice bob n_b = + attacker_only_knows_publishable_values tr n_b + + +/// If Bob thinks he talks with Alice, +/// then Alice thinks she talk to Bob (with the same nonces), +/// unless the attacker corrupted Alice or Bob. + +val initiator_authentication: + tr:trace -> i:timestamp -> + alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> + Lemma + (requires + event_triggered_at tr i bob (Finishing {alice; bob; n_a; n_b}) /\ + trace_invariant tr + ) + (ensures + principal_is_corrupt (prefix tr i) alice \/ + principal_is_corrupt (prefix tr i) bob \/ + event_triggered (prefix tr i) alice (Responding2 {alice; bob; n_a; n_b}) + ) +let initiator_authentication tr i alice bob n_a n_b = () + +/// If Alice thinks she talks with Bob, +/// then Bob thinks he talk to Alice (with the same nonces), +/// unless the attacker corrupted Alice or Bob. + +val responder_authentication: + tr:trace -> i:timestamp -> + alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> + Lemma + (requires + event_triggered_at tr i alice (Responding2 {alice; bob; n_a; n_b}) /\ + trace_invariant tr + ) + (ensures + principal_is_corrupt (prefix tr i) alice \/ + principal_is_corrupt (prefix tr i) bob \/ + event_triggered (prefix tr i) bob (Responding1 {alice; bob; n_a; n_b}) + ) +let responder_authentication tr i alice bob n_a n_b = () From f858a92109e6595af6d31da1b7e2a98ab3b8ea7b Mon Sep 17 00:00:00 2001 From: cwaldm Date: Fri, 21 Feb 2025 11:21:02 +0100 Subject: [PATCH 06/16] nsl: invariant proofs: step 1, step 2 init --- examples/NSL_with_properties/DY.NSLP.Data.fst | 6 +- .../DY.NSLP.Invariants.Proofs.fst | 98 +++++++++++++++++++ .../NSL_with_properties/DY.NSLP.Protocol.fst | 14 ++- 3 files changed, 110 insertions(+), 8 deletions(-) create mode 100644 examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst diff --git a/examples/NSL_with_properties/DY.NSLP.Data.fst b/examples/NSL_with_properties/DY.NSLP.Data.fst index 6bc46ed..60cb3e7 100644 --- a/examples/NSL_with_properties/DY.NSLP.Data.fst +++ b/examples/NSL_with_properties/DY.NSLP.Data.fst @@ -43,9 +43,9 @@ type message3_t = { [@@ with_bytes bytes] type message_t = - | Msg1: message1_t -> message_t - | Msg2: message2_t -> message_t - | Msg3: message3_t -> message_t + | Msg1: (m1:message1_t) -> message_t + | Msg2: (m2:message2_t) -> message_t + | Msg3: (m3:message3_t) -> message_t /// Using Comparse to generate parser and serializer for the message type diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst new file mode 100644 index 0000000..8239d31 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -0,0 +1,98 @@ +module DY.NSLP.Invariants.Proofs + +open Comparse +open DY.Core +open DY.Lib + +open DY.Simplified +open DY.Extend + +open DY.NSLP.Data +open DY.NSLP.Protocol +open DY.NSLP.Invariants + +#set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" + +/// In this module, we show that +/// the protocol steps maintain the protocol invariants. +/// +/// For every step s we show a lemma of the form: +/// trace_invariant tr ==> trace_invariant ( trace after step s ) + +(*** Sending the First Message ***) + + +val send_msg1_invariant: + alice:principal -> bob:principal -> alice_public_keys_sid:state_id -> + tr:trace -> + Lemma + ( requires trace_invariant tr + ) + (ensures ( + let (_ , tr_out) = send_msg1 alice bob alice_public_keys_sid tr in + trace_invariant tr_out + )) +let send_msg1_invariant alice bob alice_public_keys_sid tr = + let (n_a, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in + let (_, tr_ev) = trigger_event alice (Initiating {alice; bob; n_a}) tr_rand in + let msg1 = Msg1 {alice; n_a} in + serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_ev) msg1; + pke_enc_for_is_publishable tr_ev alice bob alice_public_keys_sid key_tag msg1 + +(*** Sending the Second Message ***) + + +val decode_msg1_invariant: + bob:principal -> bob_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires trace_invariant tr) + (ensures ( + let (_, tr_out) = decode_msg1 bob bob_private_keys_sid msg tr in + trace_invariant tr_out + )) +let decode_msg1_invariant bob bob_private_keys_sid msg tr = () + + +val receive_msg1_and_send_msg2_invariant: + bob:principal -> + bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> + msg_ts:timestamp -> + tr:trace -> + Lemma + ( requires trace_invariant tr + ) + (ensures ( + let (_ , tr_out) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts tr in + trace_invariant tr_out + )) +let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_keys_sid msg_ts tr = + match recv_msg msg_ts tr with + | (None, _ ) -> () + | (Some msg, _) -> ( + match decode_msg1 bob bob_private_keys_sid msg tr with + | (None, _) -> () + | (Some {alice; n_a}, tr_decode) -> ( + assert(trace_invariant tr_decode); + let (n_b, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in + assert(trace_invariant tr_rand); + let (_, tr_ev) = trigger_event bob (Responding1 {alice; bob; n_a; n_b}) tr_rand in + assert(trace_invariant tr_ev); + let msg2 = Msg2 {bob; n_a; n_b} in + match pke_enc_for bob alice bob_public_keys_sid key_tag msg2 tr_ev with + | (None, _) -> () + | (Some msg2_encrypted, tr_msg2) ->( + assert(trace_invariant tr_msg2); + let (msg2_ts, tr_msg2) = send_msg msg2_encrypted tr_msg2 in + assume(trace_invariant tr_msg2); + let state = SentMsg2 {alice; n_a; n_b} in + let (sess_id, tr_sess) = start_new_session bob state tr_msg2 in + assume(trace_invariant tr_sess) + ) + ) + ) + +(*** Sending the Third Message ***) + +(*** Receiving the Final Message ***) diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst index fd24b68..2711acb 100644 --- a/examples/NSL_with_properties/DY.NSLP.Protocol.fst +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -69,23 +69,27 @@ let send_msg1 alice bob alice_public_keys_sid = /// * the message is not of the right type, i.e., not a first message /// * encryption fails (for example, if Bob doesn't have a public key for Alice) +val decode_msg1: principal -> state_id -> bytes -> traceful (option message1_t) +let decode_msg1 bob bob_private_keys_sid msg = + let*? msg1 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg1? msg1);*? + return (Some (Msg1?.m1 msg1)) + + val receive_msg1_and_send_msg2: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts = let*? msg = recv_msg msg_ts in - - let*? msg1_ = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in - guard_tr (Msg1? msg1_);*? - let Msg1 msg1 = msg1_ in + let*? msg1 = decode_msg1 bob bob_private_keys_sid msg in let alice = msg1.alice in let n_a = msg1.n_a in let* n_b = gen_rand_labeled (nonce_label alice bob) in + trigger_event bob (Responding1 {alice; bob; n_a; n_b});* let msg2 = Msg2 {bob; n_a; n_b} in let*? msg2_encrypted = pke_enc_for bob alice bob_public_keys_sid key_tag msg2 in let* msg2_ts = send_msg msg2_encrypted in - trigger_event bob (Responding1 {alice; bob; n_a; n_b});* let state = SentMsg2 {alice; n_a; n_b} in let* sess_id = start_new_session bob state in From 62ffb3fee2776565dad10e0d19e884af225f113f Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 10:19:26 +0100 Subject: [PATCH 07/16] nsl invariant proofs: msg 2 --- examples/NSL_with_properties/DY.NSLP.Data.fst | 2 +- .../DY.NSLP.Invariants.Proofs.fst | 42 ++++++++++++++++--- 2 files changed, 37 insertions(+), 7 deletions(-) diff --git a/examples/NSL_with_properties/DY.NSLP.Data.fst b/examples/NSL_with_properties/DY.NSLP.Data.fst index 60cb3e7..e3bb611 100644 --- a/examples/NSL_with_properties/DY.NSLP.Data.fst +++ b/examples/NSL_with_properties/DY.NSLP.Data.fst @@ -54,7 +54,7 @@ type message_t = %splice [ps_message3_t] (gen_parser (`message3_t)) %splice [ps_message_t] (gen_parser (`message_t)) -instance parseable_serializeable_bytes_message: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t +instance parseable_serializeable_bytes_message_t: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t (*** State Type ***) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 8239d31..6f7a4e4 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -55,6 +55,33 @@ val decode_msg1_invariant: let decode_msg1_invariant bob bob_private_keys_sid msg tr = () +val decode_msg1_proof: + bob:principal -> bob_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + bytes_invariant tr msg + ) + (ensures ( + match decode_msg1 bob bob_private_keys_sid msg tr with + | (None, _) -> True + | (Some msg1, _) -> ( + let n_a = msg1.n_a in + is_knowable_by (nonce_label msg1.alice bob) tr n_a + ) + )) +let decode_msg1_proof bob bob_private_keys_sid msg tr = + match decode_msg1 bob bob_private_keys_sid msg tr with + | (None, _) -> () + | (Some msg1, _) -> ( + bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t bob bob_private_keys_sid key_tag msg; + let plain = serialize message_t (Msg1 msg1) in + parse_wf_lemma message_t (bytes_invariant tr) plain; + FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain + ) + val receive_msg1_and_send_msg2_invariant: bob:principal -> bob_private_keys_sid:state_id -> bob_public_keys_sid:state_id -> @@ -73,8 +100,7 @@ let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_key | (Some msg, _) -> ( match decode_msg1 bob bob_private_keys_sid msg tr with | (None, _) -> () - | (Some {alice; n_a}, tr_decode) -> ( - assert(trace_invariant tr_decode); + | (Some {alice; n_a}, _) -> ( let (n_b, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in assert(trace_invariant tr_rand); let (_, tr_ev) = trigger_event bob (Responding1 {alice; bob; n_a; n_b}) tr_rand in @@ -84,11 +110,15 @@ let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_key | (None, _) -> () | (Some msg2_encrypted, tr_msg2) ->( assert(trace_invariant tr_msg2); - let (msg2_ts, tr_msg2) = send_msg msg2_encrypted tr_msg2 in - assume(trace_invariant tr_msg2); + let (msg2_ts, tr_msg2_) = send_msg msg2_encrypted tr_msg2 in + decode_msg1_proof bob bob_private_keys_sid msg tr; + serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_rand) msg2; + pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag msg2; + assert(is_publishable tr_msg2 msg2_encrypted); + assert(trace_invariant tr_msg2_); let state = SentMsg2 {alice; n_a; n_b} in - let (sess_id, tr_sess) = start_new_session bob state tr_msg2 in - assume(trace_invariant tr_sess) + let (sess_id, tr_sess) = start_new_session bob state tr_msg2_ in + assert(trace_invariant tr_sess) ) ) ) From 16e9d32ba5028d9b84abd16eb86fab5592804d48 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 11:52:48 +0100 Subject: [PATCH 08/16] nsl invariant proofs: sending msg3 --- .../DY.NSLP.Invariants.Proofs.fst | 96 +++++++++++++++++++ .../DY.NSLP.Invariants.fst | 3 +- .../NSL_with_properties/DY.NSLP.Protocol.fst | 18 ++-- 3 files changed, 110 insertions(+), 7 deletions(-) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 6f7a4e4..117eb60 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -125,4 +125,100 @@ let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_key (*** Sending the Third Message ***) +val decode_msg2_invariant: + alice:principal -> alice_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires trace_invariant tr) + (ensures ( + let (_, tr_out) = decode_msg2 alice alice_private_keys_sid msg tr in + trace_invariant tr_out + )) +let decode_msg2_invariant alice alice_private_keys_sid msg tr = () + +val decode_msg2_proof: + alice:principal -> alice_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + bytes_invariant tr msg + ) + (ensures ( + match decode_msg2 alice alice_private_keys_sid msg tr with + | (None, _) -> True + | (Some msg2, _) -> ( + let bob = msg2.bob in + let n_a = msg2.n_a in + let n_b = msg2.n_b in + is_knowable_by (nonce_label alice msg2.bob) tr n_b /\ + ( is_publishable tr n_a \/ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b})) + ) + )) +let decode_msg2_proof alice alice_private_keys_sid msg tr = + match decode_msg2 alice alice_private_keys_sid msg tr with + | (None, _) -> () + | (Some msg2, _) -> ( + bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t alice alice_private_keys_sid key_tag msg; + let plain = serialize message_t (Msg2 msg2) in + parse_wf_lemma message_t (bytes_invariant tr) plain; + FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain + ) + +#push-options "--z3rlimit 30" +val receive_msg2_and_send_msg3_invariant: + alice:principal -> + alice_private_keys_sid:state_id -> alice_public_keys_sid:state_id -> + msg_ts:timestamp -> + tr:trace -> + Lemma + ( requires trace_invariant tr + ) + (ensures ( + let (_ , tr_out) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts tr in + trace_invariant tr_out + )) +let receive_msg2_and_send_msg3_invariant alice alice_private_keys_sid alice_public_keys_sid msg_ts tr = + match recv_msg msg_ts tr with + | (None, _) -> () + | (Some msg2_, _) -> ( + match decode_msg2 alice alice_private_keys_sid msg2_ tr with + | (None, _ ) -> () + | (Some msg2, _) -> ( + let bob = msg2.bob in + let n_a = msg2.n_a in + let n_b = msg2.n_b in + + let p = (fun (st:state_t) -> + SentMsg1? st + && (SentMsg1?.sentmsg1 st).n_a = n_a + && (SentMsg1?.sentmsg1 st).bob = bob + ) in + match lookup_state #state_t alice p tr with + | (None, _) -> () + | (Some (sid, st), _ ) -> ( + let ((), tr_ev) = trigger_event alice (Responding2 {alice; bob; n_a; n_b}) tr in + decode_msg2_proof alice alice_private_keys_sid msg2_ tr; + assert(trace_invariant tr_ev); + let msg3 = Msg3 {n_b} in + match pke_enc_for alice bob alice_public_keys_sid key_tag msg3 tr_ev with + | (None, _ ) -> () + | (Some msg3_encrypted, tr_enc) -> ( + assert(trace_invariant tr_enc); + let (_, tr_msg3) = send_msg msg3_encrypted tr_enc in + serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) msg3; + pke_enc_for_is_publishable tr_ev alice bob alice_public_keys_sid key_tag msg3; + assert(trace_invariant tr_msg3); + let state = SentMsg3 {bob; n_a; n_b} in + let ((), tr_st) = set_state alice sid state tr_msg3 in + assert(trace_invariant tr_st) + ) + ) + ) + ) +#pop-options + (*** Receiving the Final Message ***) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst index 90c63b4..12b622a 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -131,7 +131,8 @@ let event_predicate_nsl: event_predicate event_t = | Responding2 {alice; bob; n_a; n_b} -> ( prin == alice /\ event_triggered tr alice (Initiating {alice; bob; n_a}) /\ ( - is_corrupt tr (nonce_label alice bob) \/ + is_publishable tr n_a + \/ event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) ) ) diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst index 2711acb..69f32f2 100644 --- a/examples/NSL_with_properties/DY.NSLP.Protocol.fst +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -113,13 +113,18 @@ let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ /// * encryption fails (for example, if Bob doesn't have a public key for Alice) /// * there is no prior session related to Bob and n_a +val decode_msg2: principal -> state_id -> bytes -> traceful (option message2_t) +let decode_msg2 alice alice_private_keys_sid msg = + let*? msg2 = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag msg in + guard_tr (Msg2? msg2);*? + return (Some (Msg2?.m2 msg2)) + + val receive_msg2_and_send_msg3: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts = let*? msg = recv_msg msg_ts in - let*? msg2_ = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag msg in - guard_tr (Msg2? msg2_);*? - let Msg2 msg2 = msg2_ in + let*? msg2 = decode_msg2 alice alice_private_keys_sid msg in let bob = msg2.bob in let n_a = msg2.n_a in let n_b = msg2.n_b in @@ -131,13 +136,14 @@ let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_si && (SentMsg1?.sentmsg1 st).bob = bob ) in guard_tr(SentMsg1? st);*? - + + trigger_event alice (Responding2 {alice; bob; n_a; n_b});* let msg3 = Msg3 {n_b} in let*? msg3_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg3 in - let* msg3_ts = send_msg msg3_encrypted in - trigger_event alice (Responding2 {alice; bob; n_a; n_b});* + let* msg3_ts = send_msg msg3_encrypted in + let state = SentMsg3 {bob; n_a; n_b} in set_state alice sid state;* From 71e886c3fa8ac5d9ccc56f37e17da409dfa81b94 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 12:17:45 +0100 Subject: [PATCH 09/16] nsl invariant proofs: receive final message --- examples/NSL/DY.NSL.Protocol.fst | 2 +- .../DY.NSLP.Invariants.Proofs.fst | 84 +++++++++++++++++++ .../DY.NSLP.Invariants.fst | 4 +- .../NSL_with_properties/DY.NSLP.Protocol.fst | 14 +++- 4 files changed, 98 insertions(+), 6 deletions(-) diff --git a/examples/NSL/DY.NSL.Protocol.fst b/examples/NSL/DY.NSL.Protocol.fst index 55052fb..158e145 100644 --- a/examples/NSL/DY.NSL.Protocol.fst +++ b/examples/NSL/DY.NSL.Protocol.fst @@ -162,6 +162,6 @@ let receive_msg3 bob bob_private_keys_sid msg3_ts = let alice = (SentMsg2?.sentmsg2 st).alice in let n_a = (SentMsg2?.sentmsg2 st).n_a in - set_state alice sid (ReceivedMsg3 {alice; n_a; n_b});* + set_state bob sid (ReceivedMsg3 {alice; n_a; n_b});* return (Some sid) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 117eb60..1869ec4 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -222,3 +222,87 @@ let receive_msg2_and_send_msg3_invariant alice alice_private_keys_sid alice_publ #pop-options (*** Receiving the Final Message ***) + + +val decode_msg3_invariant: + bob:principal -> bob_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires trace_invariant tr) + (ensures ( + let (_, tr_out) = decode_msg3 bob bob_private_keys_sid msg tr in + trace_invariant tr_out + )) +let decode_msg3_invariant bob bob_private_keys_sid msg tr = () + +val decode_msg3_proof: + bob:principal -> bob_private_keys_sid:state_id -> + msg:bytes -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + bytes_invariant tr msg + ) + (ensures ( + match decode_msg3 bob bob_private_keys_sid msg tr with + | (None, _) -> True + | (Some msg3, _) -> ( + let n_b = msg3.n_b in + is_publishable tr n_b \/ ( + exists alice n_a. + get_label tr n_b `can_flow tr` (nonce_label alice bob) /\ + event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) + ) + ) + )) +let decode_msg3_proof bob bob_private_keys_sid msg tr = + match decode_msg3 bob bob_private_keys_sid msg tr with + | (None, _) -> () + | (Some msg3, _) -> ( + bytes_invariant_pke_dec_with_key_lookup tr #message_t #parseable_serializeable_bytes_message_t bob bob_private_keys_sid key_tag msg; + let plain = serialize message_t (Msg3 msg3) in + parse_wf_lemma message_t (bytes_invariant tr) plain; + FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain + ) + +val receive_msg3_invariant: + bob:principal -> + bob_private_keys_sid:state_id -> + msg_ts:timestamp -> + tr:trace -> + Lemma + (requires + trace_invariant tr + ) + (ensures ( + let (_, tr_out) = receive_msg3 bob bob_private_keys_sid msg_ts tr in + trace_invariant tr_out + )) +let receive_msg3_invariant bob bob_private_keys_sid msg_ts tr = + match recv_msg msg_ts tr with + | (None, _ ) -> () + | (Some msg3_, _) -> ( + match decode_msg3 bob bob_private_keys_sid msg3_ tr with + | (None, _ ) -> () + | (Some msg3, _) -> ( + let n_b = msg3.n_b in + let p = (fun (st:state_t) -> + SentMsg2? st + && (SentMsg2?.sentmsg2 st).n_b = n_b + ) in + match lookup_state #state_t bob p tr with + | (None, _ ) -> () + | (Some (sid, st), _ ) -> ( + let alice = (SentMsg2?.sentmsg2 st).alice in + let n_a = (SentMsg2?.sentmsg2 st).n_a in + + let (_, tr_ev) = trigger_event bob (Finishing {alice; bob; n_a; n_b}) tr in + decode_msg3_proof bob bob_private_keys_sid msg3_ tr; + assert(trace_invariant tr_ev); + let (_, tr_st) = set_state bob sid (ReceivedMsg3 {alice; n_a; n_b}) tr_ev in + assert(trace_invariant tr_st) + ) + ) + ) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst index 12b622a..a3843bb 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -139,7 +139,9 @@ let event_predicate_nsl: event_predicate event_t = | Finishing {alice; bob; n_a; n_b} -> ( prin == bob /\ event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) /\ ( - is_corrupt tr (nonce_label alice bob) \/ + // is_corrupt tr (nonce_label alice bob) + is_publishable tr n_b + \/ event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) ) ) diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst index 69f32f2..bdcedc4 100644 --- a/examples/NSL_with_properties/DY.NSLP.Protocol.fst +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -163,12 +163,18 @@ let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_si /// * the message is not of the right type, i.e., not a reply /// * there is no prior session related to n_a + +val decode_msg3: principal -> state_id -> bytes -> traceful (option message3_t) +let decode_msg3 bob bob_private_keys_sid msg = + let*? msg3 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in + guard_tr (Msg3? msg3);*? + return (Some (Msg3?.m3 msg3)) + + val receive_msg3: principal -> state_id -> timestamp -> traceful (option state_id) let receive_msg3 bob bob_private_keys_sid msg3_ts = let*? msg = recv_msg msg3_ts in - let*? msg3 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in - guard_tr (Msg3? msg3);*? - let Msg3 msg3 = msg3 in + let*? msg3 = decode_msg3 bob bob_private_keys_sid msg in let n_b = msg3.n_b in let*? (sid, st) = lookup_state #state_t bob @@ -182,6 +188,6 @@ let receive_msg3 bob bob_private_keys_sid msg3_ts = trigger_event bob (Finishing {alice; bob; n_a; n_b});* - set_state alice sid (ReceivedMsg3 {alice; n_a; n_b});* + set_state bob sid (ReceivedMsg3 {alice; n_a; n_b});* return (Some sid) From cc5f5c41e9f12dfe5b1c06adda3ce28df898277c Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 12:28:30 +0100 Subject: [PATCH 10/16] small cleanuip --- examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 1869ec4..276a3cf 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -69,7 +69,8 @@ val decode_msg1_proof: | (None, _) -> True | (Some msg1, _) -> ( let n_a = msg1.n_a in - is_knowable_by (nonce_label msg1.alice bob) tr n_a + let alice = msg1.alice in + is_knowable_by (nonce_label alice bob) tr n_a ) )) let decode_msg1_proof bob bob_private_keys_sid msg tr = @@ -114,7 +115,6 @@ let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_key decode_msg1_proof bob bob_private_keys_sid msg tr; serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_rand) msg2; pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag msg2; - assert(is_publishable tr_msg2 msg2_encrypted); assert(trace_invariant tr_msg2_); let state = SentMsg2 {alice; n_a; n_b} in let (sess_id, tr_sess) = start_new_session bob state tr_msg2_ in @@ -153,7 +153,7 @@ val decode_msg2_proof: let bob = msg2.bob in let n_a = msg2.n_a in let n_b = msg2.n_b in - is_knowable_by (nonce_label alice msg2.bob) tr n_b /\ + is_knowable_by (nonce_label alice bob) tr n_b /\ ( is_publishable tr n_a \/ event_triggered tr bob (Responding1 {alice; bob; n_a; n_b})) ) From 9f37e5e258c7207b67f323f13c42eaed35b3e969 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 12:35:41 +0100 Subject: [PATCH 11/16] cleanup --- examples/NSL/DY.NSL.Data.fst | 12 +++++----- examples/NSL_with_properties/DY.NSLP.Data.fst | 8 +++---- .../DY.NSLP.Invariants.fst | 7 ++---- .../DY.NSLP.Properties.fst | 24 +++++++++---------- .../NSL_with_properties/DY.NSLP.Protocol.fst | 4 +--- 5 files changed, 25 insertions(+), 30 deletions(-) diff --git a/examples/NSL/DY.NSL.Data.fst b/examples/NSL/DY.NSL.Data.fst index 7073dff..73fdfa6 100644 --- a/examples/NSL/DY.NSL.Data.fst +++ b/examples/NSL/DY.NSL.Data.fst @@ -43,9 +43,9 @@ type message3_t = { [@@ with_bytes bytes] type message_t = - | Msg1: message1_t -> message_t - | Msg2: message2_t -> message_t - | Msg3: message3_t -> message_t + | Msg1: (m1:message1_t) -> message_t + | Msg2: (m2:message2_t) -> message_t + | Msg3: (m3:message3_t) -> message_t /// Using Comparse to generate parser and serializer for the message type @@ -54,7 +54,7 @@ type message_t = %splice [ps_message3_t] (gen_parser (`message3_t)) %splice [ps_message_t] (gen_parser (`message_t)) -instance parseable_serializeable_bytes_message: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t +instance parseable_serializeable_bytes_message_t: parseable_serializeable bytes message_t = mk_parseable_serializeable ps_message_t (*** State Type ***) @@ -92,8 +92,8 @@ type received_msg3_t = { type state_t = | SentMsg1: (sentmsg1:sent_msg1_t) -> state_t | SentMsg2: (sentmsg2:sent_msg2_t) -> state_t - | SentMsg3: sent_msg3_t -> state_t - | ReceivedMsg3: received_msg3_t -> state_t + | SentMsg3: (sentmsg3:sent_msg3_t) -> state_t + | ReceivedMsg3: (receivedmsg3:received_msg3_t) -> state_t /// As for messages, we use Comparse to generate /// a parser and serializer for our abstract state types. diff --git a/examples/NSL_with_properties/DY.NSLP.Data.fst b/examples/NSL_with_properties/DY.NSLP.Data.fst index e3bb611..fe0e5c6 100644 --- a/examples/NSL_with_properties/DY.NSLP.Data.fst +++ b/examples/NSL_with_properties/DY.NSLP.Data.fst @@ -92,8 +92,8 @@ type received_msg3_t = { type state_t = | SentMsg1: (sentmsg1:sent_msg1_t) -> state_t | SentMsg2: (sentmsg2:sent_msg2_t) -> state_t - | SentMsg3: sent_msg3_t -> state_t - | ReceivedMsg3: received_msg3_t -> state_t + | SentMsg3: (sentmsg3:sent_msg3_t) -> state_t + | ReceivedMsg3: (receivedmsg3:received_msg3_t) -> state_t /// As for messages, we use Comparse to generate /// a parser and serializer for our abstract state types. @@ -169,10 +169,10 @@ type ev_finish_t = { [@@ with_bytes bytes] type event_t = - | Initiating: ev_init_t -> event_t + | Initiating: ev_init_t -> event_t | Responding1: ev_respond1_t -> event_t | Responding2: ev_respond2_t -> event_t - | Finishing: ev_finish_t -> event_t + | Finishing: ev_finish_t -> event_t %splice [ps_ev_init_t] (gen_parser (`ev_init_t)) %splice [ps_ev_respond1_t] (gen_parser (`ev_respond1_t)) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst index a3843bb..304155c 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -131,17 +131,14 @@ let event_predicate_nsl: event_predicate event_t = | Responding2 {alice; bob; n_a; n_b} -> ( prin == alice /\ event_triggered tr alice (Initiating {alice; bob; n_a}) /\ ( - is_publishable tr n_a - \/ + is_publishable tr n_a \/ event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) ) ) | Finishing {alice; bob; n_a; n_b} -> ( prin == bob /\ event_triggered tr bob (Responding1 {alice; bob; n_a; n_b}) /\ ( - // is_corrupt tr (nonce_label alice bob) - is_publishable tr n_b - \/ + is_publishable tr n_b \/ event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) ) ) diff --git a/examples/NSL_with_properties/DY.NSLP.Properties.fst b/examples/NSL_with_properties/DY.NSLP.Properties.fst index 1a88f23..91d1971 100644 --- a/examples/NSL_with_properties/DY.NSLP.Properties.fst +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -58,35 +58,35 @@ let n_b_secrecy tr alice bob n_b = /// unless the attacker corrupted Alice or Bob. val initiator_authentication: - tr:trace -> i:timestamp -> + tr:trace -> ts:timestamp -> alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> Lemma (requires - event_triggered_at tr i bob (Finishing {alice; bob; n_a; n_b}) /\ + event_triggered_at tr ts bob (Finishing {alice; bob; n_a; n_b}) /\ trace_invariant tr ) (ensures - principal_is_corrupt (prefix tr i) alice \/ - principal_is_corrupt (prefix tr i) bob \/ - event_triggered (prefix tr i) alice (Responding2 {alice; bob; n_a; n_b}) + principal_is_corrupt (prefix tr ts) alice \/ + principal_is_corrupt (prefix tr ts) bob \/ + event_triggered (prefix tr ts) alice (Responding2 {alice; bob; n_a; n_b}) ) -let initiator_authentication tr i alice bob n_a n_b = () +let initiator_authentication tr ts alice bob n_a n_b = () /// If Alice thinks she talks with Bob, /// then Bob thinks he talk to Alice (with the same nonces), /// unless the attacker corrupted Alice or Bob. val responder_authentication: - tr:trace -> i:timestamp -> + tr:trace -> ts:timestamp -> alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> Lemma (requires - event_triggered_at tr i alice (Responding2 {alice; bob; n_a; n_b}) /\ + event_triggered_at tr ts alice (Responding2 {alice; bob; n_a; n_b}) /\ trace_invariant tr ) (ensures - principal_is_corrupt (prefix tr i) alice \/ - principal_is_corrupt (prefix tr i) bob \/ - event_triggered (prefix tr i) bob (Responding1 {alice; bob; n_a; n_b}) + principal_is_corrupt (prefix tr ts) alice \/ + principal_is_corrupt (prefix tr ts) bob \/ + event_triggered (prefix tr ts) bob (Responding1 {alice; bob; n_a; n_b}) ) -let responder_authentication tr i alice bob n_a n_b = () +let responder_authentication tr ts alice bob n_a n_b = () diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst index bdcedc4..994b99c 100644 --- a/examples/NSL_with_properties/DY.NSLP.Protocol.fst +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -141,9 +141,7 @@ let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_si let msg3 = Msg3 {n_b} in let*? msg3_encrypted = pke_enc_for alice bob alice_public_keys_sid key_tag msg3 in - - let* msg3_ts = send_msg msg3_encrypted in - + let* msg3_ts = send_msg msg3_encrypted in let state = SentMsg3 {bob; n_a; n_b} in set_state alice sid state;* From bda6989857ea4f61155ff31fb634c4df27d4a2e1 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Mon, 24 Feb 2025 12:36:49 +0100 Subject: [PATCH 12/16] delet nsl version with only one event --- .../DY.Example.NSL.Debug.Printing.fst | 85 ---- .../DY.Example.NSL.Debug.fst | 79 --- ...DY.Example.NSL.Protocol.Stateful.Proof.fst | 469 ------------------ .../DY.Example.NSL.Protocol.Stateful.fst | 241 --------- .../DY.Example.NSL.Protocol.Total.Proof.fst | 308 ------------ .../DY.Example.NSL.Protocol.Total.fst | 143 ------ .../DY.Example.NSL.SecurityProperties.fst | 91 ---- .../nsl_pk_only_one_event_lookup/Makefile | 10 - 8 files changed, 1426 deletions(-) delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.Printing.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.Proof.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.SecurityProperties.fst delete mode 100644 examples/nsl_pk_only_one_event_lookup/Makefile diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.Printing.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.Printing.fst deleted file mode 100644 index 53ea7d3..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.Printing.fst +++ /dev/null @@ -1,85 +0,0 @@ -module DY.Example.NSL.Debug.Printing - -open Comparse -open DY.Core -open DY.Lib -open DY.Example.NSL.Protocol.Total -open DY.Example.NSL.Protocol.Stateful - -/// This module is not needed for modeling -/// the protocol. The purpose of this model -/// is to provide functions to nicely print -/// the trace to the console. - -(*** Convert NSL Messages to String ***) - -val decrypt_message: bytes -> bytes -> bytes -> option bytes -let decrypt_message sk_a sk_b msg_bytes = - let msg_plain = pke_dec sk_a msg_bytes in - match msg_plain with - | Some msg -> msg_plain - | None -> ( - pke_dec sk_b msg_bytes - ) - -val message_to_string: bytes -> bytes -> bytes -> option string -let message_to_string sk_a sk_b msg_bytes = - let? msg_plain = decrypt_message sk_a sk_b msg_bytes in - let? msg = parse message msg_plain in - match msg with - | Msg1 msg1 -> Some (Printf.sprintf "Msg1: Pke[sk=(%s), msg=(n_a=(%s), principal=%s)]" (bytes_to_string sk_b) (bytes_to_string msg1.n_a) msg1.alice) - | Msg2 msg2 -> ( - Some (Printf.sprintf "Msg2: Pke[sk=(%s), msg=(n_a=(%s), n_b=(%s), principal=%s)]" - (bytes_to_string sk_a) (bytes_to_string msg2.n_a) (bytes_to_string msg2.n_b) msg2.bob) - ) - | Msg3 msg3 -> Some (Printf.sprintf "Msg3: Pke[sk=(%s), msg=(n_b=(%s))]" (bytes_to_string sk_b) (bytes_to_string msg3.n_b)) - - -(*** Convert NSL Sessions to String ***) - -val session_to_string: bytes -> option string -let session_to_string sess_bytes = - let? sess = parse nsl_session sess_bytes in - match sess with - | InitiatorSendingMsg1 b n_a -> ( - Some (Printf.sprintf "InitiatorSendingMsg1 [n_a=(%s), to=%s]" (bytes_to_string n_a) b) - ) - | ResponderSendingMsg2 a n_a n_b -> ( - Some (Printf.sprintf "ResponderSendingMsg2 [n_a=(%s), n_b=(%s), to=%s]"(bytes_to_string n_a) (bytes_to_string n_b) a) - ) - | InitiatorSendingMsg3 b n_a n_b -> ( - Some (Printf.sprintf "InitiatorSendingMsg3 [n_a=(%s), n_b=(%s), to=%s]" (bytes_to_string n_a) (bytes_to_string n_b) b) - ) - | ResponderReceivedMsg3 a n_a n_b -> ( - Some (Printf.sprintf "ResponderReceivedMsg3 [n_a=(%s), n_b=(%s), from=%s]" (bytes_to_string n_a) (bytes_to_string n_b) a) - ) - - -(*** Convert NSL Events to String ***) - -val event_to_string: bytes -> option string -let event_to_string event_bytes = - let? event = parse nsl_event event_bytes in - match event with -// | Initiate1 a b n_a -> ( -// Some (Printf.sprintf "[principal1=%s, principal2=(%s), n_b=(%s)]" a b (bytes_to_string n_a)) -// ) - | Responding a b n_a n_b -> ( - Some (Printf.sprintf "Responding [principal1=%s, n_a=(%s), n_b=(%s), to=%s]" b (bytes_to_string n_a) (bytes_to_string n_b) a) - ) -// | Initiate2 a b n_a n_b -> ( -// Some (Printf.sprintf "[principal1=%s, principal2=(%s), n_a=(%s), n_b=(%s)]" a b (bytes_to_string n_a) (bytes_to_string n_b)) -// ) -// | Respond2 a b n_a n_b -> ( -// Some (Printf.sprintf "[principal1=%s, principal2=(%s), n_a=(%s), n_b=(%s)]" a b (bytes_to_string n_a) (bytes_to_string n_b)) -// ) - - -(*** Putting Everything Together ***) - -val get_nsl_trace_to_string_printers: bytes -> bytes -> trace_to_string_printers -let get_nsl_trace_to_string_printers priv_key_alice priv_key_bob = - trace_to_string_printers_builder - (message_to_string priv_key_alice priv_key_bob) - [(local_state_nsl_session.tag, session_to_string)] - [(event_nsl_event.tag, event_to_string)] diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.fst deleted file mode 100644 index fdc7f20..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Debug.fst +++ /dev/null @@ -1,79 +0,0 @@ -module DY.Example.NSL.Debug - -open Comparse -open DY.Core -open DY.Lib -open DY.Example.NSL.Protocol.Total -open DY.Example.NSL.Protocol.Stateful -open DY.Example.NSL.Debug.Printing - -(*** Example Protocol Run with Trace Printing ***) - -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 (LongTermPkeKey"NSL.PublicKey");* - - // 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 (LongTermPkeKey "NSL.PublicKey");* - - // 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 (LongTermPkeKey "NSL.PublicKey") in - let pub_key_bob = pk 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 (LongTermPkeKey "NSL.PublicKey") 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 (LongTermPkeKey "NSL.PublicKey") in - let pub_key_alice = pk 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 (LongTermPkeKey "NSL.PublicKey") alice pub_key_alice;* - - let alice_global_session_ids: nsl_global_sess_ids = {pki=alice_global_session_pub_key_id; private_keys=alice_global_session_priv_key_id} in - let bob_global_session_ids: nsl_global_sess_ids = {pki=bob_global_session_pub_key_id; private_keys=bob_global_session_priv_key_id} in - - (*** Run the protocol ***) - // Alice send message 1 - // let* alice_session_id = prepare_msg1 alice bob in - // let*? msg1_id = send_msg1 alice_global_session_ids alice alice_session_id in - let*? (msg1_id, alice_session_id) = send_msg1_ alice_global_session_ids alice bob in - - - - // Bob receive message 1 and send message 2 - // let*? bob_session_id = prepare_msg2 bob_global_session_ids bob msg1_id in - // let*? msg2_id = send_msg2 bob_global_session_ids bob bob_session_id in - let*? (msg2_id, bob_session_id) = send_msg2_ bob_global_session_ids bob msg1_id in - - // Alice receive message 2 and send message 3 - //prepare_msg3 alice_global_session_ids alice alice_session_id msg2_id;* -// let*? msg3_id = send_msg3 alice_global_session_ids alice alice_session_id in - // let*? sid = prepare_msg3_ alice_global_session_ids alice msg2_id in - // let*? msg3_id = send_msg3 alice_global_session_ids alice sid in - let*? (msg3_id, _) = send_msg3_ alice_global_session_ids alice msg2_id in - - // Bob receive message 3 - //prepare_msg4 bob_global_session_ids bob bob_session_id msg3_id;* - receive_msg3 bob_global_session_ids bob msg3_id;* - - let* tr = get_trace in - let _ = IO.debug_print_string ( - trace_to_string (get_nsl_trace_to_string_printers priv_key_alice priv_key_bob) tr - ) in - - return (Some ()) - -//Run ``debug ()`` when the module loads -#push-options "--warn_error -272" -let _ = debug () empty_trace -#pop-options diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst deleted file mode 100644 index ae453d5..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.Proof.fst +++ /dev/null @@ -1,469 +0,0 @@ -module DY.Example.NSL.Protocol.Stateful.Proof - -open Comparse -open DY.Core -open DY.Lib - -open DY.Extend - -open DY.Example.NSL.Protocol.Total -open DY.Example.NSL.Protocol.Total.Proof -open DY.Example.NSL.Protocol.Stateful - -#set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" - -/// This module proves invariant preservation -/// for all the functions in DY.Example.NSL.Protocol.Stateful. - -(*** Trace invariants ***) - - -/// The (local) state predicate. - -let state_predicate_nsl: local_state_predicate nsl_session = { - pred = (fun tr prin sess_id st -> - match st with - | InitiatorSendingMsg1 bob n_a -> ( - let alice = prin in - is_knowable_by (nonce_label alice bob) tr n_a /\ - is_secret (nonce_label alice bob) tr n_a /\ - rand_generated_before tr n_a - ) - | ResponderSendingMsg2 alice n_a n_b -> ( - let bob = prin in - is_knowable_by (nonce_label alice bob) tr n_a /\ - is_knowable_by (nonce_label alice bob) tr n_b /\ - - event_triggered tr bob (Responding alice bob n_a n_b) - // is_secret (nonce_label alice bob) tr n_b /\ - // rand_generated_before tr n_b - ) - | InitiatorSendingMsg3 bob n_a n_b -> ( - let alice = prin in - is_knowable_by (nonce_label alice bob) tr n_a /\ - is_knowable_by (nonce_label alice bob) tr n_b /\ - - state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a) /\ - ( is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob) - \/ ( - state_was_set_some_id #_ tr bob (ResponderSendingMsg2 alice n_a n_b) - )) - ) - | ResponderReceivedMsg3 alice n_a n_b -> ( - let bob = prin in - is_knowable_by (nonce_label alice bob) tr n_a /\ - is_knowable_by (nonce_label alice bob) tr n_b /\ - state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a n_b) /\ - (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob) - \/ - state_was_set_some_id #_ tr alice (InitiatorSendingMsg3 bob n_a n_b) - ) - ) - ); - pred_later = (fun tr1 tr2 prin sess_id st -> ()); - pred_knowable = (fun tr prin sess_id st -> ()); -} - -/// List of all local state predicates. - -let all_sessions = [ - pki_tag_and_invariant; - private_keys_tag_and_invariant; - (|local_state_nsl_session.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_nsl|); -] - -/// The (local) event predicate. - -let event_predicate_nsl: event_predicate nsl_event = - fun tr prin e -> - match e with - | Responding alice bob n_a n_b -> ( - prin == bob /\ - is_secret (nonce_label alice bob) tr n_b /\ - rand_just_generated tr n_b - ) - - -/// List of all local event predicates. - -let all_events = [ - (event_nsl_event.tag, compile_event_pred event_predicate_nsl) -] - -/// Create the global trace invariants. - -let trace_invariants_nsl: trace_invariants = { - state_pred = mk_state_pred all_sessions; - event_pred = mk_event_pred all_events; -} - -instance protocol_invariants_nsl: protocol_invariants = { - crypto_invs = crypto_invariants_nsl; - trace_invs = trace_invariants_nsl; -} - -let complies_with_nsl tr = trace_invariant #protocol_invariants_nsl tr - -/// Lemmas that the global state predicate contains all the local ones - -// Below, the `has_..._predicate` are called with the implicit argument `#protocol_invariants_nsl`. -// This argument could be omitted as it can be instantiated automatically by F*'s typeclass resolution algorithm. -// However we instantiate it explicitly here so that the meaning of `has_..._predicate` is easier to understand. - -val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate #protocol_invariants_nsl) all_sessions)) -let all_sessions_has_all_sessions () = - assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_sessions))); - mk_state_pred_correct #protocol_invariants_nsl all_sessions; - norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate #protocol_invariants_nsl) all_sessions) - -val protocol_invariants_nsl_has_pki_invariant: squash (has_pki_invariant #protocol_invariants_nsl) -let protocol_invariants_nsl_has_pki_invariant = all_sessions_has_all_sessions () - -val protocol_invariants_nsl_has_private_keys_invariant: squash (has_private_keys_invariant #protocol_invariants_nsl) -let protocol_invariants_nsl_has_private_keys_invariant = all_sessions_has_all_sessions () - -// As an example, below `#protocol_invariants_nsl` is omitted and instantiated using F*'s typeclass resolution algorithm -val protocol_invariants_nsl_has_nsl_session_invariant: squash (has_local_state_predicate state_predicate_nsl) -let protocol_invariants_nsl_has_nsl_session_invariant = all_sessions_has_all_sessions () - -/// Lemmas that the global event predicate contains all the local ones - -val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events)) -let all_events_has_all_events () = - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events))); - mk_event_pred_correct #protocol_invariants_nsl all_events; - norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events); - let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in - dumb_lemma (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred #protocol_invariants_nsl) all_events)) - -// As an example, below `#protocol_invariants_nsl` is omitted and instantiated using F*'s typeclass resolution algorithm -val protocol_invariants_nsl_has_nsl_event_invariant: squash (has_event_pred event_predicate_nsl) -let protocol_invariants_nsl_has_nsl_event_invariant = all_events_has_all_events () - -(*** Proofs ***) - -val prepare_msg1_proof: - tr:trace -> - alice:principal -> bob:principal -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (sess_id, tr_out) = prepare_msg1 alice bob tr in - trace_invariant tr_out - )) -let prepare_msg1_proof tr alice bob = - () - -val send_msg1_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> sess_id:state_id -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_msg_id, tr_out) = send_msg1 global_sess_id alice sess_id tr in - trace_invariant tr_out - )) -let send_msg1_proof tr global_sess_id alice sess_id = - match get_state alice sess_id tr with - | (Some (InitiatorSendingMsg1 bob n_a), tr) -> ( - assert(state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a)); - match get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob tr with - | (None, tr) -> () - | (Some pk_b, tr) -> ( - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label alice) 32 tr in - compute_message1_proof tr alice bob pk_b n_a nonce - ) - ) - | _ -> () - -val send_msg1__proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> bob:principal -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_msg_id, tr_out) = send_msg1_ global_sess_id alice bob tr in - trace_invariant tr_out - )) -let send_msg1__proof tr global_sess_id alice bob = - let (n_a, tr) = mk_rand NoUsage (nonce_label alice bob) 32 tr in - - let (sess_id, _) = new_session_id alice tr in - let st = InitiatorSendingMsg1 bob n_a in - let (_ , tr_state) = set_state alice sess_id st tr in - set_state_state_was_set alice sess_id st tr; - assert(state_was_set_some_id tr_state alice (InitiatorSendingMsg1 bob n_a)); - - match get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob tr_state with - | (None, tr) -> () - | (Some pk_b, tr) -> ( - - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label alice) 32 tr in - compute_message1_proof tr alice bob pk_b n_a nonce; - - () - ) - -val prepare_msg2_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> bob:principal -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_sess_id, tr_out) = prepare_msg2 global_sess_id bob msg_id tr in - trace_invariant tr_out - )) -let prepare_msg2_proof tr global_sess_id bob msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_b, tr) -> ( - decode_message1_proof tr bob msg sk_b - ) - ) - -val send_msg2_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> bob:principal -> sess_id:state_id -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_msg_id, tr_out) = send_msg2 global_sess_id bob sess_id tr in - trace_invariant tr_out - )) -let send_msg2_proof tr global_sess_id bob sess_id = - match get_state bob sess_id tr with - | (Some (ResponderSendingMsg2 alice n_a n_b), tr) -> ( - assert(state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a n_b)); - match get_public_key bob global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") alice tr with - | (None, tr) -> () - | (Some pk_a, tr) -> ( - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label bob) 32 tr in - compute_message2_proof tr bob {n_a; alice;} pk_a n_b nonce - ) - ) - | (_, tr) -> () - -val send_msg2__proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> bob:principal -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_ids, tr_out) = send_msg2_ global_sess_id bob msg_id tr in - trace_invariant tr_out - )) -let send_msg2__proof tr global_sess_id bob msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_b, tr) -> ( - decode_message1_proof tr bob msg sk_b; - match decode_message1 bob msg sk_b with - | None -> () - | Some msg1 -> ( - let alice = msg1.alice in - let n_a = msg1.n_a in - let (n_b, tr) = mk_rand NoUsage (nonce_label msg1.alice bob) 32 tr in - let (_, tr) = trigger_event bob (Responding alice bob n_a n_b) tr in - let st = ResponderSendingMsg2 msg1.alice msg1.n_a n_b in - let (sess_id, _) = new_session_id bob tr in - let (_, tr_st) = set_state bob sess_id st tr in -// set_state_state_was_set bob sess_id st tr_st; - assert(state_was_set_some_id tr_st bob st); - match get_public_key bob global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") alice tr_st with - | (None, tr) -> () - | (Some pk_a, tr) -> ( - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label bob) 32 tr in - compute_message2_proof tr bob {n_a; alice;} pk_a n_b nonce - ) - )) - ) - -val prepare_msg3_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> sess_id:state_id -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_sess_id, tr_out) = prepare_msg3 global_sess_id alice sess_id msg_id tr in - trace_invariant tr_out - )) -let prepare_msg3_proof tr global_sess_id alice sess_id msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_a, tr) -> ( - match get_state alice sess_id tr with - | (Some (InitiatorSendingMsg1 bob n_a), tr) -> ( - decode_message2_proof tr alice bob msg sk_a n_a - ) - | (_, tr) -> () - ) - ) - -val prepare_msg3__proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_sess_id, tr_out) = prepare_msg3_ global_sess_id alice msg_id tr in - trace_invariant tr_out - )) -let prepare_msg3__proof tr global_sess_id alice msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_a, tr) -> ( - match decode_message2_ alice msg sk_a with - | None -> () - | Some msg2 -> - let p = (fun (s:nsl_session) -> - (InitiatorSendingMsg1? s) && - (InitiatorSendingMsg1?.n_a s = msg2.n_a) && - (InitiatorSendingMsg1?.b s = msg2.bob)) in - match lookup_state alice p tr with - | (None , _) -> () - | (Some (sid, st) , _ ) -> - decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a - ) - ) - - - -val send_msg3_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> sess_id:state_id -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_msg_id, tr_out) = send_msg3 global_sess_id alice sess_id tr in - trace_invariant tr_out - )) -let send_msg3_proof tr global_sess_id alice sess_id = - match get_state alice sess_id tr with - | (Some (InitiatorSendingMsg3 bob n_a n_b), tr) -> ( - assert(state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)); - match get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob tr with - | (None, tr) -> () - | (Some pk_b, tr) -> ( - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label alice) 32 tr in - compute_message3_proof tr alice bob pk_b n_b nonce - ) - ) - | (_, tr) -> () - - - -val send_msg3__proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> alice:principal -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_ids, tr_out) = send_msg3_ global_sess_id alice msg_id tr in - trace_invariant tr_out - )) -let send_msg3__proof tr global_sess_id alice msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_a, tr) -> ( - match decode_message2_ alice msg sk_a with - | None -> () - | Some msg2 -> ( - let p = (fun (s:nsl_session) -> - (InitiatorSendingMsg1? s) && - (InitiatorSendingMsg1?.n_a s = msg2.n_a) && - (InitiatorSendingMsg1?.b s = msg2.bob)) in - match lookup_state alice p tr with - | (None , _) -> () - | (Some (sid, st) , _ ) -> ( - decode_message2_proof tr alice msg2.bob msg sk_a msg2.n_a; - let n_b = msg2.n_b in - let InitiatorSendingMsg1 bob n_a = st in - let new_st = InitiatorSendingMsg3 bob n_a n_b in - let (_, tr_state) = set_state alice sid new_st tr in - assert(state_was_set_some_id tr_state alice new_st); - match get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob tr_state with - | (None, tr) -> () - | (Some pk_b, tr) -> ( - let (nonce, tr) = mk_rand PkeNonce (long_term_key_label alice) 32 tr in - compute_message3_proof tr alice bob pk_b n_b nonce - ) - )) - )) - - -val event_respond1_injective: - tr:trace -> - alice:principal -> alice':principal -> bob:principal -> - n_a:bytes -> n_a':bytes -> n_b:bytes -> - Lemma - (requires - trace_invariant tr /\ - event_triggered tr bob (Responding alice bob n_a n_b) /\ - event_triggered tr bob (Responding alice' bob n_a' n_b) - ) - (ensures - alice == alice' /\ - n_a == n_a' - ) -let event_respond1_injective tr alice alice' bob n_a n_a' n_b = () - -val receive_msg3_proof: - tr:trace -> - global_sess_id:nsl_global_sess_ids -> bob:principal -> sess_id:state_id -> msg_id:timestamp -> - Lemma - (requires trace_invariant tr) - (ensures ( - let (opt_sess_id, tr_out) = receive_msg3 global_sess_id bob msg_id tr in - trace_invariant tr_out - )) -let receive_msg3_proof tr global_sess_id bob sess_id msg_id = - match recv_msg msg_id tr with - | (None, tr) -> () - | (Some msg, tr) -> ( - match get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") tr with - | (None, tr) -> () - | (Some sk_b, tr) -> ( - match decode_message3_ msg sk_b with - | None -> () - | Some msg3 -> ( - let p = (fun (s:nsl_session) -> - (ResponderSendingMsg2? s) && - (ResponderSendingMsg2?.n_b s = msg3.n_b)) in - match lookup_state bob p tr with - | (None, _ ) -> () - | (Some (id, st), _) -> ( - let ResponderSendingMsg2 alice n_a n_b = st in - assert(event_triggered tr bob (Responding alice bob n_a n_b)); - - assert(is_publishable tr n_b ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)); - introduce ~(is_publishable tr n_b) ==> - state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b) - with _. ( - decode_message3__proof tr alice bob msg sk_b; - eliminate exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ - state_was_set_some_id tr alice' (InitiatorSendingMsg3 bob n_a' n_b) - returns _ - with _. ( - assert(event_triggered tr bob (Responding alice' bob n_a' n_b)); - event_respond1_injective tr alice alice' bob n_a n_a' n_b - - ) - - ) - ) - ))) diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.fst deleted file mode 100644 index 7c5596c..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Stateful.fst +++ /dev/null @@ -1,241 +0,0 @@ -module DY.Example.NSL.Protocol.Stateful - -open Comparse -open DY.Core -open DY.Lib -open DY.Extend - -open DY.Example.NSL.Protocol.Total - -/// This module implements the impure (or stateful) part of the NSL protocol. -/// This effectively connects the pure code of NSL to the outside world, -/// by handling network connections, state storage, or random generation. - -(*** State type ***) - -/// Type for the NSL state machine - -[@@ with_bytes bytes] -type nsl_session = - | InitiatorSendingMsg1: b:principal -> n_a:bytes -> nsl_session - | ResponderSendingMsg2: a:principal -> n_a:bytes -> n_b:bytes -> nsl_session - | InitiatorSendingMsg3: b:principal -> n_a:bytes -> n_b:bytes -> nsl_session - | ResponderReceivedMsg3: a:principal -> n_a:bytes -> n_b:bytes -> nsl_session - -%splice [ps_nsl_session] (gen_parser (`nsl_session)) -%splice [ps_nsl_session_is_well_formed] (gen_is_well_formed_lemma (`nsl_session)) - -instance parseable_serializeable_bytes_nsl_session: parseable_serializeable bytes nsl_session - = mk_parseable_serializeable ps_nsl_session - -instance local_state_nsl_session: local_state nsl_session = { - tag = "NSL.Session"; - format = parseable_serializeable_bytes_nsl_session; -} - - -(*** Event type ***) - -/// Type for the NSL protocol events. -/// They will be used to write authentication security properties. - -[@@ with_bytes bytes] -type nsl_event = - | Responding: a:principal -> b:principal -> n_a:bytes -> n_b:bytes -> nsl_event - -%splice [ps_nsl_event] (gen_parser (`nsl_event)) -%splice [ps_nsl_event_is_well_formed] (gen_is_well_formed_lemma (`nsl_event)) - -instance event_nsl_event: event nsl_event = { - tag = "NSL.Event"; - format = mk_parseable_serializeable ps_nsl_event; -} - - -(*** Stateful code ***) - -type nsl_global_sess_ids = { - pki: state_id; - private_keys: state_id; -} - -let nonce_label alice bob = join (principal_label alice) (principal_label bob) - -val prepare_msg1: principal -> principal -> traceful state_id -let prepare_msg1 alice bob = - let* n_a = mk_rand NoUsage (nonce_label alice bob) 32 in - let* sess_id = new_session_id alice in - set_state alice sess_id (InitiatorSendingMsg1 bob n_a <: nsl_session);* - return sess_id - -val send_msg1: nsl_global_sess_ids -> principal -> state_id -> traceful (option timestamp) -let send_msg1 global_sess_id alice sess_id = - let*? st = get_state alice sess_id in - guard_tr (InitiatorSendingMsg1? st);*? - let InitiatorSendingMsg1 bob n_a = st in - let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob in - let* nonce = mk_rand PkeNonce (long_term_key_label alice) 32 in - let msg = compute_message1 alice bob pk_b n_a nonce in - let* msg_id = send_msg msg in - return (Some msg_id) - -val send_msg1_: nsl_global_sess_ids -> principal -> principal -> traceful (option (timestamp & state_id)) -let send_msg1_ global_sess_id alice bob = - let* n_a = mk_rand NoUsage (nonce_label alice bob) 32 in - - let* sess_id = new_session_id alice in - let st = InitiatorSendingMsg1 bob n_a in - set_state alice sess_id st;* - - let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob in - let* nonce = mk_rand PkeNonce (long_term_key_label alice) 32 in - let msg = compute_message1 alice bob pk_b n_a nonce in - let* msg_id = send_msg msg in - - return (Some (msg_id, sess_id)) - - -val prepare_msg2: nsl_global_sess_ids -> principal -> timestamp -> traceful (option state_id) -let prepare_msg2 global_sess_id bob msg_id = - let*? msg = recv_msg msg_id in - let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? msg1: message1 = return (decode_message1 bob msg sk_b) in - let* n_b = mk_rand NoUsage (nonce_label msg1.alice bob) 32 in - trigger_event bob (Responding msg1.alice bob msg1.n_a n_b);* - let* sess_id = new_session_id bob in - set_state bob sess_id (ResponderSendingMsg2 msg1.alice msg1.n_a n_b <: nsl_session);* - return (Some sess_id) - -val send_msg2: nsl_global_sess_ids -> principal -> state_id -> traceful (option timestamp) -let send_msg2 global_sess_id bob sess_id = - let*? st = get_state bob sess_id in - guard_tr (ResponderSendingMsg2? st);*? - let ResponderSendingMsg2 alice n_a n_b = st in - let*? pk_a = get_public_key bob global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") alice in - let* nonce = mk_rand PkeNonce (long_term_key_label bob) 32 in - let msg = compute_message2 bob {n_a; alice;} pk_a n_b nonce in - let* msg_id = send_msg msg in - return (Some msg_id) - - -val send_msg2_: nsl_global_sess_ids -> principal -> timestamp -> traceful (option (timestamp & state_id)) -let send_msg2_ global_sess_id bob msg_id = - let*? msg = recv_msg msg_id in - let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? msg1: message1 = return (decode_message1 bob msg sk_b) in - - let alice = msg1.alice in - let n_a = msg1.n_a in - let* n_b = mk_rand NoUsage (nonce_label alice bob) 32 in - trigger_event bob (Responding alice bob n_a n_b);* - - let st = ResponderSendingMsg2 alice n_a n_b in - let* sess_id = new_session_id bob in - set_state bob sess_id st;* - - let*? pk_a = get_public_key bob global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") msg1.alice in - let* nonce = mk_rand PkeNonce (long_term_key_label bob) 32 in - let msg2 = compute_message2 bob {n_a; alice;} pk_a n_b nonce in - let* msg_id = send_msg msg2 in - - - return (Some (msg_id, sess_id)) - -val prepare_msg3: nsl_global_sess_ids -> principal -> state_id -> timestamp -> traceful (option unit) -let prepare_msg3 global_sess_id alice sess_id msg_id = - let*? msg = recv_msg msg_id in - let*? sk_a = get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? st = get_state alice sess_id in - guard_tr (InitiatorSendingMsg1? st);*? - let InitiatorSendingMsg1 bob n_a = st in - let*? msg2: message2 = return (decode_message2 alice bob msg sk_a n_a) in - set_state alice sess_id (InitiatorSendingMsg3 bob n_a msg2.n_b <: nsl_session);* - return (Some ()) - -val prepare_msg3_: nsl_global_sess_ids -> principal -> timestamp -> traceful (option state_id) -let prepare_msg3_ global_sess_id alice msg_id = - let*? msg = recv_msg msg_id in - let*? sk_a = get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? msg2: message2 = return (decode_message2_ alice msg sk_a) in - let p = (fun (s:nsl_session) -> - (InitiatorSendingMsg1? s) && - (InitiatorSendingMsg1?.n_a s = msg2.n_a) && - (InitiatorSendingMsg1?.b s = msg2.bob)) in - let* tr = get_trace in - let (opt_st, _) = lookup_state #nsl_session alice p tr in - match opt_st with - | None -> return None - | Some (sid, st) -> ( - let InitiatorSendingMsg1 bob n_a = st in - set_state alice sid (InitiatorSendingMsg3 bob n_a msg2.n_b <: nsl_session);* - return (Some sid) - ) - - -val send_msg3: nsl_global_sess_ids -> principal -> state_id -> traceful (option timestamp) -let send_msg3 global_sess_id alice sess_id = - let*? st = get_state alice sess_id in - guard_tr (InitiatorSendingMsg3? st);*? - let InitiatorSendingMsg3 bob n_a n_b = st in - let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob in - let* nonce = mk_rand PkeNonce (long_term_key_label alice) 32 in - let msg = compute_message3 alice bob pk_b n_b nonce in - let* msg_id = send_msg msg in - return (Some msg_id) - -val send_msg3_: nsl_global_sess_ids -> principal -> timestamp -> traceful (option (timestamp & state_id)) -let send_msg3_ global_sess_id alice msg_id = - let*? msg = recv_msg msg_id in - let*? sk_a = get_private_key alice global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? msg2: message2 = return (decode_message2_ alice msg sk_a) in - - let p = (fun (s:nsl_session) -> - (InitiatorSendingMsg1? s) && - (InitiatorSendingMsg1?.n_a s = msg2.n_a) && - (InitiatorSendingMsg1?.b s = msg2.bob)) in - let* tr = get_trace in - let (opt_st, _) = lookup_state #nsl_session alice p tr in - match opt_st with - | None -> return None - | Some (sid, st) -> ( - let n_b = msg2.n_b in - let InitiatorSendingMsg1 bob n_a = st in - let st = InitiatorSendingMsg3 bob n_a n_b in - set_state alice sid st;* - - let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkeKey "NSL.PublicKey") bob in - let* nonce = mk_rand PkeNonce (long_term_key_label alice) 32 in - let msg3 = compute_message3 alice bob pk_b n_b nonce in - let* msg_id = send_msg msg3 in - return (Some (msg_id, sid)) - ) - -val prepare_msg4: nsl_global_sess_ids -> principal -> state_id -> timestamp -> traceful (option unit) -let prepare_msg4 global_sess_id bob sess_id msg_id = - let*? msg = recv_msg msg_id in - let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - let*? st = get_state bob sess_id in - guard_tr (ResponderSendingMsg2? st);*? - let ResponderSendingMsg2 alice n_a n_b = st in - let*? msg3: message3 = return (decode_message3 alice bob msg sk_b n_b) in - set_state bob sess_id (ResponderReceivedMsg3 alice n_a n_b <: nsl_session);* - return (Some ()) - -val receive_msg3: nsl_global_sess_ids -> principal -> timestamp -> traceful (option unit) -let receive_msg3 global_sess_id bob msg_id = - let*? msg = recv_msg msg_id in - let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkeKey "NSL.PublicKey") in - - let*? msg3: message3 = return (decode_message3_ msg sk_b) in - let p = (fun (s:nsl_session) -> - (ResponderSendingMsg2? s) && - (ResponderSendingMsg2?.n_b s = msg3.n_b)) in - let* tr = get_trace in - let (opt_st, _) = lookup_state #nsl_session bob p tr in - match opt_st with - | None -> return None - | Some (sid, st) -> ( - let ResponderSendingMsg2 alice n_a n_b = st in - set_state bob sid (ResponderReceivedMsg3 alice n_a n_b <: nsl_session);* - return (Some ()) - ) diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.Proof.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.Proof.fst deleted file mode 100644 index 670b4fa..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.Proof.fst +++ /dev/null @@ -1,308 +0,0 @@ -module DY.Example.NSL.Protocol.Total.Proof - -open Comparse -open DY.Core -open DY.Lib - -open DY.Extend - -open DY.Example.NSL.Protocol.Total -open DY.Example.NSL.Protocol.Stateful - -#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'" - -/// This module proves lemmas for the functions in DY.Example.NSL.Protocol.Total. -/// They will in turn be used in the stateful invariant proofs -/// in DY.Example.NSL.Protocol.Stateful.Proofs. - -(*** Cryptographic invariants ***) - -let state_was_set_some_id (#a:Type) {|local_state a|} tr prin (cont : a) = - exists sid. state_was_set tr prin sid cont - -val state_was_set_some_id_grows: - #a:Type -> {|lsa:local_state a|} -> - tr1:trace -> tr2:trace -> - prin:principal -> content:a -> - Lemma - (requires tr1 <$ tr2 - /\ state_was_set_some_id tr1 prin content - ) - (ensures - state_was_set_some_id tr2 prin content - ) - [SMTPat (state_was_set_some_id #a #lsa tr1 prin content); SMTPat (tr1 <$ tr2)] -let state_was_set_some_id_grows #a #ls tr1 tr2 prin content = admit() - - -instance crypto_usages_nsl : crypto_usages = default_crypto_usages - -#push-options "--ifuel 2 --fuel 0" -val crypto_predicates_nsl: crypto_predicates -let crypto_predicates_nsl = { - default_crypto_predicates with - - pke_pred = { - pred = (fun tr sk_usage pk msg -> - (exists prin. - sk_usage == long_term_key_type_to_usage (LongTermPkeKey "NSL.PublicKey") prin - /\ ( - match parse message msg with - | Some (Msg1 msg1) -> ( - let (alice, bob) = (msg1.alice, prin) in - state_was_set_some_id tr alice (InitiatorSendingMsg1 bob msg1.n_a)/\ - get_label tr msg1.n_a == nonce_label alice bob - ) - | Some (Msg2 msg2) -> ( - let (alice, bob) = (prin, msg2.bob) in - state_was_set_some_id tr bob (ResponderSendingMsg2 alice msg2.n_a msg2.n_b) /\ - get_label tr msg2.n_b == nonce_label alice bob - ) - | Some (Msg3 msg3) -> ( - let bob = prin in - exists alice n_a. - get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\ - state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a msg3.n_b) - ) - | None -> False - )) - ); - pred_later = (fun tr1 tr2 sk_usage pk msg -> - parse_wf_lemma message (bytes_well_formed tr1) msg - ); - }; -} -#pop-options - -instance crypto_invariants_nsl : crypto_invariants = { - usages = crypto_usages_nsl; - preds = crypto_predicates_nsl; -} - -(*** Proofs ***) - -val compute_message1_proof: - tr:trace -> - alice:principal -> bob:principal -> pk_b:bytes -> n_a:bytes -> nonce:bytes -> - Lemma - (requires - // From the stateful code - state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a)/\ - // From random generation - is_secret (nonce_label alice bob) tr n_a /\ - // From random generation - is_secret (long_term_key_label alice) tr nonce /\ - // From random generation - nonce `has_usage tr` PkeNonce /\ - // From PKI invariants - is_public_key_for tr pk_b (LongTermPkeKey "NSL.PublicKey") bob - ) - (ensures is_publishable tr (compute_message1 alice bob pk_b n_a nonce)) -let compute_message1_proof tr alice bob pk_b n_a nonce = - let msg = Msg1 {n_a; alice;} in - serialize_wf_lemma message (is_knowable_by (long_term_key_label alice) tr) msg; - serialize_wf_lemma message (is_knowable_by (long_term_key_label bob) tr) msg - -// If bob successfully decrypt the first message, -// then n_a is knownable both by alice (in the message) and bob (the principal) -// This is because: -// - if the message was encrypted by the attacker, then n_a is publishable hence knowable by alice and bob -// - if the message was encrypted by an honest principal, this follows from the encryption predicate -#push-options "--ifuel 1 --fuel 0 --z3rlimit 25" -val decode_message1_proof: - tr:trace -> - bob:principal -> msg_cipher:bytes -> sk_b:bytes -> - Lemma - (requires - // From PrivateKeys invariants - is_private_key_for tr sk_b (LongTermPkeKey "NSL.PublicKey") bob /\ - // From the network - bytes_invariant tr msg_cipher - ) - (ensures ( - match decode_message1 bob msg_cipher sk_b with - | None -> True - | Some msg1 -> ( - is_knowable_by (nonce_label msg1.alice bob) tr msg1.n_a - /\ ( - is_publishable tr msg1.n_a - \/ state_was_set_some_id tr msg1.alice (InitiatorSendingMsg1 bob msg1.n_a) - ) - ) - )) -let decode_message1_proof tr bob msg_cipher sk_b = - match decode_message1 bob msg_cipher sk_b with - | None -> () - | Some msg1 -> - let Some msg = pke_dec sk_b msg_cipher in - FStar.Classical.move_requires (parse_wf_lemma message (is_publishable tr)) msg; - FStar.Classical.move_requires (parse_wf_lemma message (bytes_invariant tr)) msg -#pop-options - -val compute_message2_proof: - tr:trace -> - bob:principal -> msg1:message1 -> pk_a:bytes -> n_b:bytes -> nonce:bytes -> - Lemma - (requires - // From the stateful code - state_was_set_some_id tr bob (ResponderSendingMsg2 msg1.alice msg1.n_a n_b) /\ - // From decode_message1_proof - is_knowable_by (nonce_label msg1.alice bob) tr msg1.n_a /\ - // From the random generation - is_secret (nonce_label msg1.alice bob) tr n_b /\ - // From the random generation - is_secret (long_term_key_label bob) tr nonce /\ - // From the random generation - nonce `has_usage tr` PkeNonce /\ - // From the PKI - is_public_key_for tr pk_a (LongTermPkeKey "NSL.PublicKey") msg1.alice - ) - (ensures - is_publishable tr (compute_message2 bob msg1 pk_a n_b nonce) - ) -let compute_message2_proof tr bob msg1 pk_a n_b nonce = - let msg = Msg2 {n_a = msg1.n_a; n_b; bob;} in - serialize_wf_lemma message (is_knowable_by (principal_label msg1.alice) tr) msg; - serialize_wf_lemma message (is_knowable_by (principal_label bob) tr) msg - -// If alice successfully decrypt the second message, -// then n_b is knownable both by alice (in the message) and bob (the principal) -// (for the same reasons with decode_message1) -// Furthermore, either alice or bob are corrupt, or bob triggered the Responding event -// (proved with the encryption predicate) -#push-options "--ifuel 1 --fuel 0 --z3rlimit 25" -val decode_message2_proof: - tr:trace -> - alice:principal -> bob:principal -> msg_cipher:bytes -> sk_a:bytes -> n_a:bytes -> - Lemma - (requires - // From the NSL state invariant - is_secret (nonce_label alice bob) tr n_a /\ - // From the PrivateKeys invariant - is_private_key_for tr sk_a (LongTermPkeKey "NSL.PublicKey") alice /\ - // From the network - bytes_invariant tr msg_cipher - ) - (ensures ( - match decode_message2 alice bob msg_cipher sk_a n_a with - | None -> True - | Some msg2 -> ( - is_knowable_by (nonce_label alice bob) tr msg2.n_b - /\ ( - (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)) - \/ ( - is_secret (nonce_label alice bob) tr msg2.n_b /\ - state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a msg2.n_b) - ) - ) - ) - )) -let decode_message2_proof tr alice bob msg_cipher sk_a n_a = - match decode_message2 alice bob msg_cipher sk_a n_a with - | None -> () - | Some msg2 -> ( - let Some msg = pke_dec sk_a msg_cipher in - FStar.Classical.move_requires (parse_wf_lemma message (is_publishable tr)) msg; - FStar.Classical.move_requires (parse_wf_lemma message (bytes_invariant tr)) msg - ; assert(is_publishable tr msg ==> is_publishable tr msg2.n_a) - ; assert(n_a = msg2.n_a) - ; assert(is_publishable tr msg ==> is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)) - - ) -#pop-options - -val compute_message3_proof: - tr:trace -> - alice:principal -> bob:principal -> pk_b:bytes -> n_b:bytes -> nonce:bytes -> - Lemma - (requires - // From the stateful code - (exists n_a. state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)) /\ - // From decode_message2_proof - is_knowable_by (nonce_label alice bob) tr n_b /\ - // From the random generation - is_secret (long_term_key_label alice) tr nonce /\ - // From the random generation - nonce `has_usage tr` PkeNonce /\ - // From the PKI - is_public_key_for tr pk_b (LongTermPkeKey "NSL.PublicKey") bob - ) - (ensures - is_publishable tr (compute_message3 alice bob pk_b n_b nonce) - ) -let compute_message3_proof tr alice bob pk_b n_b nonce = - let msg = Msg3 {n_b;} in - serialize_wf_lemma message (is_knowable_by (principal_label alice) tr) msg; - serialize_wf_lemma message (is_knowable_by (principal_label bob) tr) msg; - let msg3: message3 = {n_b;} in - assert(msg3.n_b == n_b) - -// If bob successfully decrypt the third message, -// Then either alice or bob are corrupt, or alice triggered the Initiate2 event -// (proved with the encryption predicate) -#push-options "--ifuel 1 --fuel 0 --z3rlimit 25" -val decode_message3_proof: - tr:trace -> - alice:principal -> bob:principal -> msg_cipher:bytes -> sk_b:bytes -> n_b:bytes -> - Lemma - (requires - // From the NSL state invariant - get_label tr n_b == nonce_label alice bob /\ - // From the PrivateKeys invariant - is_private_key_for tr sk_b (LongTermPkeKey "NSL.PublicKey") bob /\ - // From the network - bytes_invariant tr msg_cipher - ) - (ensures ( - match decode_message3 alice bob msg_cipher sk_b n_b with - | None -> True - | Some msg3 -> ( - (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)) \/ ( - (exists alice n_a. - get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\ - state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b) - )) - ) - )) -let decode_message3_proof tr alice bob msg_cipher sk_b n_b = - match decode_message3 alice bob msg_cipher sk_b n_b with - | None -> () - | Some msg3 -> ( - let Some msg = pke_dec sk_b msg_cipher in - FStar.Classical.move_requires (parse_wf_lemma message (is_publishable tr)) msg; - FStar.Classical.move_requires (parse_wf_lemma message (bytes_invariant tr)) msg - ) -#pop-options - -#push-options "--ifuel 1 --fuel 0 --z3rlimit 25" -val decode_message3__proof: - tr:trace -> - alice:principal -> bob:principal -> msg_cipher:bytes -> sk_b:bytes -> - Lemma - (requires - // From the PrivateKeys invariant - is_private_key_for tr sk_b (LongTermPkeKey "NSL.PublicKey") bob /\ - // From the network - bytes_invariant tr msg_cipher - ) - (ensures ( - match decode_message3_ msg_cipher sk_b with - | None -> True - | Some msg3 -> ( - (is_publishable tr msg3.n_b) - \/ ( - (exists alice (n_a:bytes). - get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\ - state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a msg3.n_b) - )) - ) - )) -let decode_message3__proof tr alice bob msg_cipher sk_b = - match decode_message3_ msg_cipher sk_b with - | None -> () - | Some msg3 -> ( - let Some msg = pke_dec sk_b msg_cipher in - FStar.Classical.move_requires (parse_wf_lemma message (is_publishable tr)) msg; - FStar.Classical.move_requires (parse_wf_lemma message (bytes_invariant tr)) msg - ) -#pop-options diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.fst deleted file mode 100644 index 5ee9e3c..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.Protocol.Total.fst +++ /dev/null @@ -1,143 +0,0 @@ -module DY.Example.NSL.Protocol.Total - -open Comparse -open DY.Core -open DY.Lib - -/// Needham-Schroeder-Lowe Fixed Public Key Protocol [1] -/// -/// A -> B: {N_A, A}K_PB msg 1 -/// B -> A: {N_A, N_B, B}K_PA msg 2 -- note addition of B -/// A -> B: {N_B}K_PB msg 3 -/// -/// [1] Gavin Lowe. "Breaking and fixing the Needham-Schroeder Public-Key -/// Protocol using FDR". TACAS, pp 147-166, 1996. -/// -/// This module implements the pure part of the NSL protocol. - -(*** Message type ***) - -/// We first define types for messages, -/// which are used as public-key encryption input. -/// We use Comparse to generate a message format for each of these. - -[@@ with_bytes bytes] -type message1 = { - n_a: bytes; - alice: principal; -} - -%splice [ps_message1] (gen_parser (`message1)) -%splice [ps_message1_is_well_formed] (gen_is_well_formed_lemma (`message1)) - -[@@ with_bytes bytes] -type message2 = { - n_a: bytes; - n_b: bytes; - bob: principal; -} - -%splice [ps_message2] (gen_parser (`message2)) -%splice [ps_message2_is_well_formed] (gen_is_well_formed_lemma (`message2)) - -[@@ with_bytes bytes] -type message3 = { - n_b: bytes; -} - -%splice [ps_message3] (gen_parser (`message3)) -%splice [ps_message3_is_well_formed] (gen_is_well_formed_lemma (`message3)) - -/// The type for messages. -/// This corresponds to a tagged union, -/// the tag is necessary to avoid type-confusion attacks, see [2]. -/// -/// [2] Catherine A. Meadows. "Analyzing the Needham-Schroeder public key protocol: -/// A comparison of two approaches". ESORICS, pages 351–364, 1996. - -[@@ with_bytes bytes] -type message = - | Msg1: message1 -> message - | Msg2: message2 -> message - | Msg3: message3 -> message - -%splice [ps_message] (gen_parser (`message)) -%splice [ps_message_is_well_formed] (gen_is_well_formed_lemma (`message)) - -instance parseable_serializeable_bytes_message: parseable_serializeable bytes message = mk_parseable_serializeable ps_message - -(*** Message 1 ***) - -/// Alice generates message 1 - -val compute_message1: principal -> principal -> bytes -> bytes -> bytes -> bytes -let compute_message1 alice bob pk_b n_a nonce = - let msg = Msg1 {n_a; alice;} in - pke_enc pk_b nonce (serialize message msg) - -/// Bob process message 1 - -val decode_message1: principal -> bytes -> bytes -> option message1 -let decode_message1 bob msg1_cipher sk_b = - let? msg1_plain = pke_dec sk_b msg1_cipher in - let? msg1 = parse message msg1_plain in - guard (Msg1? msg1);? - Some (Msg1?._0 msg1) - -(*** Message 2 ***) - -/// Bob generates message 2 - -val compute_message2: principal -> message1 -> bytes -> bytes -> bytes -> bytes -let compute_message2 bob msg1 pk_a n_b nonce = - let msg2 = Msg2 {n_a = msg1.n_a; n_b; bob;} in - pke_enc pk_a nonce (serialize message msg2) - -/// Alice process message 2 - -val decode_message2: principal -> principal -> bytes -> bytes -> bytes -> option (message2) -let decode_message2 alice bob msg2_cipher sk_a n_a = - let? msg2_plain = pke_dec sk_a msg2_cipher in - let? msg2 = parse _ msg2_plain in - guard (Msg2? msg2);? - let (Msg2 msg2) = msg2 in - guard (n_a = msg2.n_a);? - guard (bob = msg2.bob);? - Some msg2 - - -val decode_message2_: principal -> bytes -> bytes -> option (message2) -let decode_message2_ alice msg2_cipher sk_a = - let? msg2_plain = pke_dec sk_a msg2_cipher in - let? msg2 = parse _ msg2_plain in - guard (Msg2? msg2);? - let (Msg2 msg2) = msg2 in - Some msg2 - -(*** Message 3 ***) - -/// Alice generates message 3 - -val compute_message3: principal -> principal -> bytes -> bytes -> bytes -> bytes -let compute_message3 alice bob pk_b n_b nonce = - let msg3 = Msg3 {n_b;} in - pke_enc pk_b nonce (serialize message msg3) - -/// Bob process message 3 - -val decode_message3: principal -> principal -> bytes -> bytes -> bytes -> option (message3) -let decode_message3 alice bob msg_cipher sk_b n_b = - let? msg_plain = pke_dec sk_b msg_cipher in - let? msg = parse _ msg_plain in - guard (Msg3? msg);? - let (Msg3 msg3) = msg in - guard (n_b = msg3.n_b);? - Some msg3 - -val decode_message3_: bytes -> bytes -> option (message3) -let decode_message3_ msg_cipher sk_b = - let? msg_plain = pke_dec sk_b msg_cipher in - let? msg = parse _ msg_plain in - guard (Msg3? msg);? - let (Msg3 msg3) = msg in - Some msg3 diff --git a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.SecurityProperties.fst b/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.SecurityProperties.fst deleted file mode 100644 index 76b0079..0000000 --- a/examples/nsl_pk_only_one_event_lookup/DY.Example.NSL.SecurityProperties.fst +++ /dev/null @@ -1,91 +0,0 @@ -module DY.Example.NSL.SecurityProperties - -open Comparse -open DY.Core -open DY.Lib -open DY.Simplified -open DY.Example.NSL.Protocol.Total.Proof -open DY.Example.NSL.Protocol.Stateful -open DY.Example.NSL.Protocol.Stateful.Proof - -#set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" - -/// This module defines the security properties of the NSL protocol. -/// They are all implied by the protocol invariants, -/// defined in DY.Example.NSL.Protocol.Total.Proof -/// and DY.Example.NSL.Protocol.Stateful.Proof. -/// Because all functions of the NSL protocol preserve the protocol invariants, -/// the attacker function also preserves the invariants. -/// Hence these security theorems hold on every trace obtainable by the attacker. - -/// If Bob thinks he talks with Alice, -/// then Alice thinks she talk to Bob (with the same nonces), -/// unless the attacker corrupted Alice or Bob. - -val initiator_authentication: - tr:trace -> i:timestamp -> - alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> - Lemma - (requires - complies_with_nsl tr /\ - state_was_set_some_id tr bob (ResponderReceivedMsg3 alice n_a n_b) - ) - (ensures - principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/ - state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a) - ) -let initiator_authentication tr i alice bob n_a n_b = () - -/// If Alice thinks she talks with Bob, -/// then Bob thinks he talk to Alice (with the same nonces), -/// unless the attacker corrupted Alice or Bob. - -val responder_authentication: - tr:trace -> i:timestamp -> - alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> - Lemma - (requires - complies_with_nsl tr /\ - state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b) - ) - (ensures - principal_is_corrupt tr alice \/ principal_is_corrupt tr bob \/ - state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a n_b) - ) -let responder_authentication tr i alice bob n_a n_b = () - -/// The nonce n_a is unknown to the attacker, -/// unless the attacker corrupted Alice or Bob. - -val n_a_secrecy: - tr:trace -> alice:principal -> bob:principal -> n_a:bytes -> - Lemma - (requires - complies_with_nsl tr /\ - attacker_knows tr n_a /\ ( - (state_was_set_some_id tr alice (InitiatorSendingMsg1 bob n_a)) \/ - (exists n_b. state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)) \/ - (exists n_b. state_was_set_some_id tr bob (ResponderReceivedMsg3 alice n_a n_b)) - ) - ) - (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob) -let n_a_secrecy tr alice bob n_a = - attacker_only_knows_publishable_values tr n_a - -/// The nonce n_b is unknown to the attacker, -/// unless the attacker corrupted Alice or Bob. - -val n_b_secrecy: - tr:trace -> alice:principal -> bob:principal -> n_b:bytes -> - Lemma - (requires - complies_with_nsl tr /\ - attacker_knows tr n_b /\ ( - (exists n_a. state_was_set_some_id tr bob (ResponderSendingMsg2 alice n_a n_b)) \/ - (exists n_a. state_was_set_some_id tr bob (ResponderReceivedMsg3 alice n_a n_b)) \/ - (exists n_a. state_was_set_some_id tr alice (InitiatorSendingMsg3 bob n_a n_b)) - ) - ) - (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob) -let n_b_secrecy tr alice bob n_b = - attacker_only_knows_publishable_values tr n_b diff --git a/examples/nsl_pk_only_one_event_lookup/Makefile b/examples/nsl_pk_only_one_event_lookup/Makefile deleted file mode 100644 index 6b3ec18..0000000 --- a/examples/nsl_pk_only_one_event_lookup/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -TUTORIAL_HOME ?= ../.. - -EXAMPLES = nsl_pk_only_one_event_lookup -EXAMPLE_DIRS = $(addprefix $(TUTORIAL_HOME)/examples/, $(EXAMPLES)) - -include $(TUTORIAL_HOME)/Makefile - -test: - cd $(TUTORIAL_HOME)/obj; $(FSTAR_EXE) --ocamlenv ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib DY_Example_NSL_Debug.native - $(TUTORIAL_HOME)/obj/DY_Example_NSL_Debug.native From 1ea4449512722e25358dc83715df648206b584d7 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Tue, 25 Feb 2025 09:31:20 +0100 Subject: [PATCH 13/16] nsl: strengthen initiator_authentication --- dy-extensions/DY.Extend.fst | 22 +++++++++++++++++++ .../DY.NSLP.Properties.fst | 10 +++++---- 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/dy-extensions/DY.Extend.fst b/dy-extensions/DY.Extend.fst index 0be400a..9fe1eb6 100644 --- a/dy-extensions/DY.Extend.fst +++ b/dy-extensions/DY.Extend.fst @@ -5,6 +5,28 @@ open DY.Core open DY.Lib open DY.Core.Trace.Base +val prefix_inv: + {|protocol_invariants|} -> + tr:trace -> + p:trace -> + Lemma + (requires + trace_invariant tr /\ + p <$ tr + ) + (ensures + trace_invariant p + ) + [SMTPat (trace_invariant tr) + ; SMTPat (p <$ tr)] +let rec prefix_inv tr p = + reveal_opaque (`%trace_invariant) trace_invariant + ; reveal_opaque (`%grows) (grows #label) + ; reveal_opaque (`%prefix) (prefix #label) + ;if trace_length tr = trace_length p + then () + else prefix_inv (init tr) p + val is_secret_is_knowable: {|cinvs: crypto_invariants|} -> l:label -> diff --git a/examples/NSL_with_properties/DY.NSLP.Properties.fst b/examples/NSL_with_properties/DY.NSLP.Properties.fst index 91d1971..41e2b56 100644 --- a/examples/NSL_with_properties/DY.NSLP.Properties.fst +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -54,7 +54,7 @@ let n_b_secrecy tr alice bob n_b = /// If Bob thinks he talks with Alice, -/// then Alice thinks she talk to Bob (with the same nonces), +/// then Alice thinks she talks to Bob (with the same nonces), /// unless the attacker corrupted Alice or Bob. val initiator_authentication: @@ -67,13 +67,15 @@ val initiator_authentication: ) (ensures principal_is_corrupt (prefix tr ts) alice \/ - principal_is_corrupt (prefix tr ts) bob \/ - event_triggered (prefix tr ts) alice (Responding2 {alice; bob; n_a; n_b}) + principal_is_corrupt (prefix tr ts) bob \/ ( + event_triggered (prefix tr ts) alice (Responding2 {alice; bob; n_a; n_b}) /\ + event_triggered (prefix tr ts) alice (Initiating {alice; bob; n_a}) + ) ) let initiator_authentication tr ts alice bob n_a n_b = () /// If Alice thinks she talks with Bob, -/// then Bob thinks he talk to Alice (with the same nonces), +/// then Bob thinks he talks to Alice (with the same nonces), /// unless the attacker corrupted Alice or Bob. val responder_authentication: From 7adf5a21b728a5668c8888208dfe811200e1ccf8 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Tue, 25 Feb 2025 10:54:01 +0100 Subject: [PATCH 14/16] fix (?) nsl --- examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 276a3cf..1b438f7 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -168,7 +168,7 @@ let decode_msg2_proof alice alice_private_keys_sid msg tr = FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain ) -#push-options "--z3rlimit 30" +#push-options "--z3rlimit 50" val receive_msg2_and_send_msg3_invariant: alice:principal -> alice_private_keys_sid:state_id -> alice_public_keys_sid:state_id -> From 1adf252fcb774c14416ffafdc234918a886af9e3 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Wed, 26 Feb 2025 17:29:31 +0100 Subject: [PATCH 15/16] introducing event_triggered_before to avoid prefix in authentication properties --- dy-extensions/DY.Simplified.fst | 5 +++++ .../NSL_with_properties/DY.NSLP.Properties.fst | 14 +++++++------- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/dy-extensions/DY.Simplified.fst b/dy-extensions/DY.Simplified.fst index af35222..5b23291 100644 --- a/dy-extensions/DY.Simplified.fst +++ b/dy-extensions/DY.Simplified.fst @@ -6,6 +6,11 @@ open DY.Lib #set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" +val event_triggered_before: + #a:Type -> {|event a|} -> + tr:trace -> ts:timestamp{ts <= trace_length tr} -> principal -> a -> prop +let event_triggered_before tr ts prin ev = event_triggered (prefix tr ts) prin ev + let gen_rand = mk_rand NoUsage public 32 diff --git a/examples/NSL_with_properties/DY.NSLP.Properties.fst b/examples/NSL_with_properties/DY.NSLP.Properties.fst index 41e2b56..ace12f9 100644 --- a/examples/NSL_with_properties/DY.NSLP.Properties.fst +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -66,10 +66,10 @@ val initiator_authentication: trace_invariant tr ) (ensures - principal_is_corrupt (prefix tr ts) alice \/ - principal_is_corrupt (prefix tr ts) bob \/ ( - event_triggered (prefix tr ts) alice (Responding2 {alice; bob; n_a; n_b}) /\ - event_triggered (prefix tr ts) alice (Initiating {alice; bob; n_a}) + principal_is_corrupt tr alice \/ + principal_is_corrupt tr bob \/ ( + event_triggered_before tr ts alice (Responding2 {alice; bob; n_a; n_b}) /\ + event_triggered_before tr ts alice (Initiating {alice; bob; n_a}) ) ) let initiator_authentication tr ts alice bob n_a n_b = () @@ -87,8 +87,8 @@ val responder_authentication: trace_invariant tr ) (ensures - principal_is_corrupt (prefix tr ts) alice \/ - principal_is_corrupt (prefix tr ts) bob \/ - event_triggered (prefix tr ts) bob (Responding1 {alice; bob; n_a; n_b}) + principal_is_corrupt tr alice \/ + principal_is_corrupt tr bob \/ + event_triggered_before tr ts bob (Responding1 {alice; bob; n_a; n_b}) ) let responder_authentication tr ts alice bob n_a n_b = () From 76468953b1dfaa0ac34052d31231b5b314c93807 Mon Sep 17 00:00:00 2001 From: cwaldm Date: Thu, 27 Feb 2025 11:32:58 +0100 Subject: [PATCH 16/16] cleanup --- examples/NSL/DY.NSL.Data.fst | 2 +- examples/NSL/DY.NSL.Protocol.fst | 2 +- examples/NSL/DY.NSL.Run.Printing.fst | 2 +- examples/NSL/DY.NSL.Run.fst | 9 +- examples/NSL_with_properties/DY.NSLP.Data.fst | 2 +- .../DY.NSLP.Invariants.Proofs.fst | 115 +++++++++--------- .../DY.NSLP.Invariants.fst | 6 +- .../DY.NSLP.Properties.fst | 4 +- .../NSL_with_properties/DY.NSLP.Protocol.fst | 20 +-- .../DY.NSLP.Run.Printing.fst | 7 +- examples/NSL_with_properties/DY.NSLP.Run.fst | 9 +- 11 files changed, 88 insertions(+), 90 deletions(-) diff --git a/examples/NSL/DY.NSL.Data.fst b/examples/NSL/DY.NSL.Data.fst index 73fdfa6..0985f8e 100644 --- a/examples/NSL/DY.NSL.Data.fst +++ b/examples/NSL/DY.NSL.Data.fst @@ -110,7 +110,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st /// We tag our protocol level states, /// so that they are distinguishable from any internal DY* states. -instance local_state_state: local_state state_t = { +instance local_state_state_t: local_state state_t = { tag = "NSL.State"; format = parseable_serializeable_bytes_state_t; } diff --git a/examples/NSL/DY.NSL.Protocol.fst b/examples/NSL/DY.NSL.Protocol.fst index 158e145..b3c0461 100644 --- a/examples/NSL/DY.NSL.Protocol.fst +++ b/examples/NSL/DY.NSL.Protocol.fst @@ -16,7 +16,7 @@ open DY.NSL.Data /// B -> A: enc{B, N_A, N_B}_A Msg 2 /// A -> B: enc{N_B}_B Msg 3 /// -/// The model consists of 4 function, +/// The model consists of 4 functions, /// one for each protocol step: /// 1. Alice sends the first message to Bob (`send_msg1`) /// 2. Bob sends the second message to Alice (`send_msg2`) diff --git a/examples/NSL/DY.NSL.Run.Printing.fst b/examples/NSL/DY.NSL.Run.Printing.fst index 7712e72..fdaf4cf 100644 --- a/examples/NSL/DY.NSL.Run.Printing.fst +++ b/examples/NSL/DY.NSL.Run.Printing.fst @@ -34,5 +34,5 @@ val get_trace_to_string_printers: trace_to_string_printers let get_trace_to_string_printers = trace_to_string_printers_builder message_to_string - ((local_state_state.tag, state_to_string) :: default_state_to_string) + ((local_state_state_t.tag, state_to_string) :: default_state_to_string) [] diff --git a/examples/NSL/DY.NSL.Run.fst b/examples/NSL/DY.NSL.Run.fst index eb11934..b3bc349 100644 --- a/examples/NSL/DY.NSL.Run.fst +++ b/examples/NSL/DY.NSL.Run.fst @@ -46,12 +46,13 @@ let run () : traceful (option unit ) = (*** The actual protocol run ***) - // Alice sends a Ping to Bob + // Alice sends the first message to Bob let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in - // Bob replies with an Ack (reading the ping at the given timestamp) + // Bob replies with a second message (reading Message 1 at the provided timestamp) let*? (bob_sid, msg2_ts) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg1_ts in - let*? (bob_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in - // Alice receives the Ack (at the given ack timestamp) + // Alice replies with the third message + let*? (alice_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in + // Bob receives the final message (at the given timestamp) receive_msg3 bob bob_private_keys_sid msg3_ts;*? diff --git a/examples/NSL_with_properties/DY.NSLP.Data.fst b/examples/NSL_with_properties/DY.NSLP.Data.fst index fe0e5c6..436dd6e 100644 --- a/examples/NSL_with_properties/DY.NSLP.Data.fst +++ b/examples/NSL_with_properties/DY.NSLP.Data.fst @@ -110,7 +110,7 @@ instance parseable_serializeable_bytes_state_t: parseable_serializeable bytes st /// We tag our protocol level states, /// so that they are distinguishable from any internal DY* states. -instance local_state_state: local_state state_t = { +instance local_state_state_t: local_state state_t = { tag = "NSL.State"; format = parseable_serializeable_bytes_state_t; } diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst index 1b438f7..3add74e 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -26,8 +26,7 @@ val send_msg1_invariant: alice:principal -> bob:principal -> alice_public_keys_sid:state_id -> tr:trace -> Lemma - ( requires trace_invariant tr - ) + (requires trace_invariant tr) (ensures ( let (_ , tr_out) = send_msg1 alice bob alice_public_keys_sid tr in trace_invariant tr_out @@ -67,11 +66,8 @@ val decode_msg1_proof: (ensures ( match decode_msg1 bob bob_private_keys_sid msg tr with | (None, _) -> True - | (Some msg1, _) -> ( - let n_a = msg1.n_a in - let alice = msg1.alice in + | (Some {alice; n_a}, _) -> is_knowable_by (nonce_label alice bob) tr n_a - ) )) let decode_msg1_proof bob bob_private_keys_sid msg tr = match decode_msg1 bob bob_private_keys_sid msg tr with @@ -81,7 +77,7 @@ let decode_msg1_proof bob bob_private_keys_sid msg tr = let plain = serialize message_t (Msg1 msg1) in parse_wf_lemma message_t (bytes_invariant tr) plain; FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain - ) + ) val receive_msg1_and_send_msg2_invariant: bob:principal -> @@ -89,8 +85,7 @@ val receive_msg1_and_send_msg2_invariant: msg_ts:timestamp -> tr:trace -> Lemma - ( requires trace_invariant tr - ) + (requires trace_invariant tr) (ensures ( let (_ , tr_out) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts tr in trace_invariant tr_out @@ -101,21 +96,28 @@ let receive_msg1_and_send_msg2_invariant bob bob_private_keys_sid bob_public_key | (Some msg, _) -> ( match decode_msg1 bob bob_private_keys_sid msg tr with | (None, _) -> () - | (Some {alice; n_a}, _) -> ( + | (Some msg1, _) -> ( + let alice = msg1.alice in + let n_a = msg1.n_a in + let (n_b, tr_rand) = gen_rand_labeled (nonce_label alice bob) tr in assert(trace_invariant tr_rand); + let (_, tr_ev) = trigger_event bob (Responding1 {alice; bob; n_a; n_b}) tr_rand in assert(trace_invariant tr_ev); + let msg2 = Msg2 {bob; n_a; n_b} in match pke_enc_for bob alice bob_public_keys_sid key_tag msg2 tr_ev with | (None, _) -> () | (Some msg2_encrypted, tr_msg2) ->( assert(trace_invariant tr_msg2); + let (msg2_ts, tr_msg2_) = send_msg msg2_encrypted tr_msg2 in - decode_msg1_proof bob bob_private_keys_sid msg tr; - serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_rand) msg2; - pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag msg2; + decode_msg1_proof bob bob_private_keys_sid msg tr; + serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr_rand) msg2; + pke_enc_for_is_publishable tr_ev bob alice bob_public_keys_sid key_tag msg2; assert(trace_invariant tr_msg2_); + let state = SentMsg2 {alice; n_a; n_b} in let (sess_id, tr_sess) = start_new_session bob state tr_msg2_ in assert(trace_invariant tr_sess) @@ -142,22 +144,19 @@ val decode_msg2_proof: msg:bytes -> tr:trace -> Lemma - (requires - trace_invariant tr /\ - bytes_invariant tr msg - ) - (ensures ( - match decode_msg2 alice alice_private_keys_sid msg tr with - | (None, _) -> True - | (Some msg2, _) -> ( - let bob = msg2.bob in - let n_a = msg2.n_a in - let n_b = msg2.n_b in - is_knowable_by (nonce_label alice bob) tr n_b /\ - ( is_publishable tr n_a \/ - event_triggered tr bob (Responding1 {alice; bob; n_a; n_b})) - ) - )) + (requires + trace_invariant tr /\ + bytes_invariant tr msg + ) + (ensures ( + match decode_msg2 alice alice_private_keys_sid msg tr with + | (None, _) -> True + | (Some {bob; n_a; n_b}, _) -> ( + is_knowable_by (nonce_label alice bob) tr n_b /\ + ( is_publishable tr n_a \/ + event_triggered tr bob (Responding1 {alice; bob; n_a; n_b})) + ) + )) let decode_msg2_proof alice alice_private_keys_sid msg tr = match decode_msg2 alice alice_private_keys_sid msg tr with | (None, _) -> () @@ -175,8 +174,7 @@ val receive_msg2_and_send_msg3_invariant: msg_ts:timestamp -> tr:trace -> Lemma - ( requires trace_invariant tr - ) + (requires trace_invariant tr) (ensures ( let (_ , tr_out) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts tr in trace_invariant tr_out @@ -201,17 +199,20 @@ let receive_msg2_and_send_msg3_invariant alice alice_private_keys_sid alice_publ | (None, _) -> () | (Some (sid, st), _ ) -> ( let ((), tr_ev) = trigger_event alice (Responding2 {alice; bob; n_a; n_b}) tr in - decode_msg2_proof alice alice_private_keys_sid msg2_ tr; + decode_msg2_proof alice alice_private_keys_sid msg2_ tr; assert(trace_invariant tr_ev); + let msg3 = Msg3 {n_b} in match pke_enc_for alice bob alice_public_keys_sid key_tag msg3 tr_ev with | (None, _ ) -> () | (Some msg3_encrypted, tr_enc) -> ( assert(trace_invariant tr_enc); + let (_, tr_msg3) = send_msg msg3_encrypted tr_enc in - serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) msg3; - pke_enc_for_is_publishable tr_ev alice bob alice_public_keys_sid key_tag msg3; + serialize_wf_lemma message_t (is_knowable_by (nonce_label alice bob) tr) msg3; + pke_enc_for_is_publishable tr_ev alice bob alice_public_keys_sid key_tag msg3; assert(trace_invariant tr_msg3); + let state = SentMsg3 {bob; n_a; n_b} in let ((), tr_st) = set_state alice sid state tr_msg3 in assert(trace_invariant tr_st) @@ -241,22 +242,21 @@ val decode_msg3_proof: msg:bytes -> tr:trace -> Lemma - (requires - trace_invariant tr /\ - bytes_invariant tr msg - ) - (ensures ( - match decode_msg3 bob bob_private_keys_sid msg tr with - | (None, _) -> True - | (Some msg3, _) -> ( - let n_b = msg3.n_b in - is_publishable tr n_b \/ ( - exists alice n_a. - get_label tr n_b `can_flow tr` (nonce_label alice bob) /\ - event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) - ) - ) - )) + (requires + trace_invariant tr /\ + bytes_invariant tr msg + ) + (ensures ( + match decode_msg3 bob bob_private_keys_sid msg tr with + | (None, _) -> True + | (Some {n_b}, _) -> ( + is_publishable tr n_b \/ ( + exists alice n_a. + get_label tr n_b `can_flow tr` (nonce_label alice bob) /\ + event_triggered tr alice (Responding2 {alice; bob; n_a; n_b}) + ) + ) + )) let decode_msg3_proof bob bob_private_keys_sid msg tr = match decode_msg3 bob bob_private_keys_sid msg tr with | (None, _) -> () @@ -273,13 +273,11 @@ val receive_msg3_invariant: msg_ts:timestamp -> tr:trace -> Lemma - (requires - trace_invariant tr - ) - (ensures ( - let (_, tr_out) = receive_msg3 bob bob_private_keys_sid msg_ts tr in - trace_invariant tr_out - )) + (requires trace_invariant tr) + (ensures ( + let (_, tr_out) = receive_msg3 bob bob_private_keys_sid msg_ts tr in + trace_invariant tr_out + )) let receive_msg3_invariant bob bob_private_keys_sid msg_ts tr = match recv_msg msg_ts tr with | (None, _ ) -> () @@ -299,8 +297,9 @@ let receive_msg3_invariant bob bob_private_keys_sid msg_ts tr = let n_a = (SentMsg2?.sentmsg2 st).n_a in let (_, tr_ev) = trigger_event bob (Finishing {alice; bob; n_a; n_b}) tr in - decode_msg3_proof bob bob_private_keys_sid msg3_ tr; + decode_msg3_proof bob bob_private_keys_sid msg3_ tr; assert(trace_invariant tr_ev); + let (_, tr_st) = set_state bob sid (ReceivedMsg3 {alice; n_a; n_b}) tr_ev in assert(trace_invariant tr_st) ) diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst index 304155c..92dd56f 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -26,7 +26,7 @@ open DY.NSLP.Protocol instance crypto_usages_nsl : crypto_usages = default_crypto_usages -#push-options "--ifuel 3 --fuel 0" +#push-options "--ifuel 3" val crypto_predicates_nsl: crypto_predicates let crypto_predicates_nsl = { default_crypto_predicates with @@ -61,8 +61,6 @@ let crypto_predicates_nsl = { } #pop-options - - instance crypto_invariants_nsl: crypto_invariants = { usages = crypto_usages_nsl; preds = crypto_predicates_nsl @@ -148,7 +146,7 @@ let event_predicate_nsl: event_predicate event_t = let all_sessions = [ pki_tag_and_invariant; private_keys_tag_and_invariant; - (|local_state_state.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_nsl|); + (|local_state_state_t.tag, local_state_predicate_to_local_bytes_state_predicate state_predicate_nsl|); ] /// List of all local event predicates. diff --git a/examples/NSL_with_properties/DY.NSLP.Properties.fst b/examples/NSL_with_properties/DY.NSLP.Properties.fst index ace12f9..cc82fb9 100644 --- a/examples/NSL_with_properties/DY.NSLP.Properties.fst +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -23,12 +23,12 @@ val n_a_secrecy: tr:trace -> alice:principal -> bob:principal -> n_a:bytes -> Lemma (requires - attacker_knows tr n_a /\ trace_invariant tr /\ ( (state_was_set_some_id tr alice (SentMsg1 {bob; n_a})) \/ (exists n_b. state_was_set_some_id tr alice (SentMsg3 {bob; n_a; n_b})) \/ (exists n_b. state_was_set_some_id tr bob (ReceivedMsg3 {alice; n_a; n_b})) - ) + ) /\ + attacker_knows tr n_a ) (ensures principal_is_corrupt tr alice \/ principal_is_corrupt tr bob) let n_a_secrecy tr alice bob n_a = diff --git a/examples/NSL_with_properties/DY.NSLP.Protocol.fst b/examples/NSL_with_properties/DY.NSLP.Protocol.fst index 994b99c..fb8fd0b 100644 --- a/examples/NSL_with_properties/DY.NSLP.Protocol.fst +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -16,7 +16,7 @@ open DY.NSLP.Data /// B -> A: enc{B, N_A, N_B}_A Msg 2 /// A -> B: enc{N_B}_B Msg 3 /// -/// The model consists of 4 function, +/// The model consists of 4 functions, /// one for each protocol step: /// 1. Alice sends the first message to Bob (`send_msg1`) /// 2. Bob sends the second message to Alice (`send_msg2`) @@ -26,9 +26,10 @@ open DY.NSLP.Data (*** Sending the first message (Alice, n_a) ***) /// Alice sends the first message to Bob: -/// * Alice generates a new nonce [n_a] -/// * encrypts the message (Alice, n_a) for Bob -/// * sends the encrypted message +/// * Alice generates a new nonce [n_a], +/// * triggers an Initiating event, +/// * encrypts the message (Alice, n_a) for Bob, +/// * sends the encrypted message, and /// * stores n_a and Bob in a state (in a new session) /// The step returns the ID of the new state /// and the timestamp of the message on the trace @@ -59,6 +60,7 @@ let send_msg1 alice bob alice_public_keys_sid = /// * read the message from the trace /// * decrypt the message to (Alice, n_a) /// * generate a new nonce [n_b] +/// * trigger a "Responding to Message 1" event /// * encrypt the reply (Bob, n_a, n_b) for Alice /// * send the encrypted reply /// * store n_a, n_b and Alice in a state in a new session @@ -69,12 +71,12 @@ let send_msg1 alice bob alice_public_keys_sid = /// * the message is not of the right type, i.e., not a first message /// * encryption fails (for example, if Bob doesn't have a public key for Alice) +/// We pull out the decryption of the message. val decode_msg1: principal -> state_id -> bytes -> traceful (option message1_t) let decode_msg1 bob bob_private_keys_sid msg = let*? msg1 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in guard_tr (Msg1? msg1);*? return (Some (Msg1?.m1 msg1)) - val receive_msg1_and_send_msg2: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ts = @@ -90,7 +92,6 @@ let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ let*? msg2_encrypted = pke_enc_for bob alice bob_public_keys_sid key_tag msg2 in let* msg2_ts = send_msg msg2_encrypted in - let state = SentMsg2 {alice; n_a; n_b} in let* sess_id = start_new_session bob state in @@ -102,6 +103,7 @@ let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ /// Alice receives the second messages and replies: /// * read the message from the trace /// * decrypt the message to (Bob, n_a, n_b) +/// * trigger a "Responding to Message 2" event /// * encrypt the reply (n_b) for Bob /// * send the encrypted reply /// * store n_a, n_b and Bob in a state in the session related to Bob and n_a @@ -113,13 +115,13 @@ let receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg_ /// * encryption fails (for example, if Bob doesn't have a public key for Alice) /// * there is no prior session related to Bob and n_a +/// Again, we pull out decryption of the message. val decode_msg2: principal -> state_id -> bytes -> traceful (option message2_t) let decode_msg2 alice alice_private_keys_sid msg = let*? msg2 = pke_dec_with_key_lookup #message_t alice alice_private_keys_sid key_tag msg in guard_tr (Msg2? msg2);*? return (Some (Msg2?.m2 msg2)) - val receive_msg2_and_send_msg3: principal -> state_id -> state_id -> timestamp -> traceful (option (state_id & timestamp)) let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg_ts = let*? msg = recv_msg msg_ts in @@ -154,6 +156,7 @@ let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_si /// * read the message from the trace /// * decrypt the message to (n_b) /// * check if Bob previously sent n_b in some session +/// * trigger a "Finishing" event /// * store completion of this session in a new state /// Returns the ID of the session that is marked as completed. /// The step fails, if one of @@ -161,14 +164,13 @@ let receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_si /// * the message is not of the right type, i.e., not a reply /// * there is no prior session related to n_a - +/// Again, we pull out decryption of the message. val decode_msg3: principal -> state_id -> bytes -> traceful (option message3_t) let decode_msg3 bob bob_private_keys_sid msg = let*? msg3 = pke_dec_with_key_lookup #message_t bob bob_private_keys_sid key_tag msg in guard_tr (Msg3? msg3);*? return (Some (Msg3?.m3 msg3)) - val receive_msg3: principal -> state_id -> timestamp -> traceful (option state_id) let receive_msg3 bob bob_private_keys_sid msg3_ts = let*? msg = recv_msg msg3_ts in diff --git a/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst b/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst index 9662b6d..2859f4d 100644 --- a/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst +++ b/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst @@ -9,10 +9,9 @@ open DY.Simplified open DY.NSLP.Data /// Helper functions for trace printing. -/// Here we define how our abstract message and state types +/// Here we define how our abstract message, state and event types /// should be printed. - val message_to_string: bytes -> option string let message_to_string b = match? parse message_t b with @@ -20,7 +19,6 @@ let message_to_string b = | Msg2 m -> Some (Printf.sprintf "Msg2 [name = (%s), n_a = (%s), n_b = (%s)]" (m.bob) (bytes_to_string m.n_a) (bytes_to_string m.n_b)) | Msg3 m -> Some (Printf.sprintf "Msg3 [n_b = (%s)]" (bytes_to_string m.n_b)) - val state_to_string: bytes -> option string let state_to_string b = match? parse state_t b with @@ -38,10 +36,9 @@ let event_to_string b = | Finishing {alice; bob; n_a; n_b} -> Some (Printf.sprintf "Finishing [bob = (%s), n_a = (%s), n_b = (%s), with = (%s)]" bob (bytes_to_string n_a) (bytes_to_string n_b) alice) - val get_trace_to_string_printers: trace_to_string_printers let get_trace_to_string_printers = trace_to_string_printers_builder message_to_string - ((local_state_state.tag, state_to_string) :: default_state_to_string) + ((local_state_state_t.tag, state_to_string) :: default_state_to_string) [(event_event_t.tag, event_to_string)] diff --git a/examples/NSL_with_properties/DY.NSLP.Run.fst b/examples/NSL_with_properties/DY.NSLP.Run.fst index 3085893..75f2266 100644 --- a/examples/NSL_with_properties/DY.NSLP.Run.fst +++ b/examples/NSL_with_properties/DY.NSLP.Run.fst @@ -46,12 +46,13 @@ let run () : traceful (option unit ) = (*** The actual protocol run ***) - // Alice sends a Ping to Bob + // Alice sends the first message to Bob let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in - // Bob replies with an Ack (reading the ping at the given timestamp) + // Bob replies with a second message (reading Message 1 at the provided timestamp) let*? (bob_sid, msg2_ts) = receive_msg1_and_send_msg2 bob bob_private_keys_sid bob_public_keys_sid msg1_ts in - let*? (bob_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in - // Alice receives the Ack (at the given ack timestamp) + // Alice replies with the third message + let*? (alice_sid, msg3_ts) = receive_msg2_and_send_msg3 alice alice_private_keys_sid alice_public_keys_sid msg2_ts in + // Bob receives the final message (at the given timestamp) receive_msg3 bob bob_private_keys_sid msg3_ts;*?