NSL

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))
 
 

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  -> 

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
 

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"

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)

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)
+    []