diff --git a/Makefile b/Makefile index aad44e1..bd36999 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 Basics +INNER_EXAMPLE_DIRS = NSL NSL_with_properties TwoMessageP Online Online_with_secrecy Basics EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS)) 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/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/DY.NSL.Data.fst b/examples/NSL/DY.NSL.Data.fst new file mode 100644 index 0000000..0985f8e --- /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: (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 + +%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_t: 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: (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. + +%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_t: 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..b3c0461 --- /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 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`) +/// 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 bob 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..fdaf4cf --- /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_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 new file mode 100644 index 0000000..b3bc349 --- /dev/null +++ b/examples/NSL/DY.NSL.Run.fst @@ -0,0 +1,68 @@ +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 the first message to Bob + let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in + // 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 + // 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;*? + + + (*** 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_pk_only_one_event_lookup/Makefile b/examples/NSL/Makefile similarity index 55% rename from examples/nsl_pk_only_one_event_lookup/Makefile rename to examples/NSL/Makefile index 6b3ec18..71d7a99 100644 --- a/examples/nsl_pk_only_one_event_lookup/Makefile +++ b/examples/NSL/Makefile @@ -1,10 +1,10 @@ TUTORIAL_HOME ?= ../.. -EXAMPLES = nsl_pk_only_one_event_lookup +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_Example_NSL_Debug.native - $(TUTORIAL_HOME)/obj/DY_Example_NSL_Debug.native + 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 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..436dd6e --- /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: (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 + +%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_t: 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: (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. + +%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_t: 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.Invariants.Proofs.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst new file mode 100644 index 0000000..3add74e --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.Proofs.fst @@ -0,0 +1,307 @@ +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 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 {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 + | (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 -> + 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 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; + 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) + ) + ) + ) + +(*** 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 {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, _) -> () + | (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 50" +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 ***) + + +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 {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, _) -> () + | (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 new file mode 100644 index 0000000..92dd56f --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -0,0 +1,198 @@ +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" +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_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_publishable tr n_b \/ + 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_t.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..cc82fb9 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Properties.fst @@ -0,0 +1,94 @@ +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 + 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 = + 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 talks to Bob (with the same nonces), +/// unless the attacker corrupted Alice or Bob. + +val initiator_authentication: + tr:trace -> ts:timestamp -> + alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> + Lemma + (requires + event_triggered_at tr ts bob (Finishing {alice; bob; n_a; n_b}) /\ + trace_invariant tr + ) + (ensures + 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 = () + +/// If Alice thinks she talks with Bob, +/// then Bob thinks he talks to Alice (with the same nonces), +/// unless the attacker corrupted Alice or Bob. + +val responder_authentication: + tr:trace -> ts:timestamp -> + alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes -> + Lemma + (requires + event_triggered_at tr ts alice (Responding2 {alice; bob; n_a; n_b}) /\ + trace_invariant tr + ) + (ensures + 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 = () 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..fb8fd0b --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Protocol.fst @@ -0,0 +1,193 @@ +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 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`) +/// 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], +/// * 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 +/// 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] +/// * 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 +/// 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) + +/// 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 = + let*? msg = recv_msg msg_ts 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 + + 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) +/// * 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 +/// 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 + +/// 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 + + 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 + + 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);*? + + 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 + + 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 +/// * 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 +/// * decryption fails +/// * 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 + 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 + (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 bob 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..2859f4d --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Run.Printing.fst @@ -0,0 +1,44 @@ +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, 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 + | 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_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 new file mode 100644 index 0000000..75f2266 --- /dev/null +++ b/examples/NSL_with_properties/DY.NSLP.Run.fst @@ -0,0 +1,68 @@ +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 the first message to Bob + let*? (alice_sid, msg1_ts) = send_msg1 alice bob alice_public_keys_sid in + // 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 + // 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;*? + + + (*** 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 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 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