small cleanup

Author: cwaldm

examples/Online_with_authn/DY.OnlineA.Invariants.Proofs.fst

@@ -193,14 +193,13 @@ let decode_ack_proof tr alice keys_sid msg =
         let plain = serialize message_t (Ack ack) in
         parse_wf_lemma message_t (bytes_invariant tr) plain;
         FStar.Classical.move_requires (parse_wf_lemma message_t (is_publishable tr)) plain
-        
     )
 
 
 /// Additionally,
 /// we need an injectivity lemma.
 /// The goal is to show that Alice uses the nonces n_a
-/// only once, i.e., the nonce n_a are unique for every run.
+/// only once, i.e., the nonces n_a are unique for every run.
 ///
 /// We show this with the help of the Initiating event:
 /// If there are two events triggered by the same Alice
@@ -223,7 +222,7 @@ val event_initiating_injective:
   (requires
     trace_invariant tr /\
     event_triggered tr alice (Initiating {alice; bob; n_a} ) /\
-    event_triggered tr alice (Initiating {alice; bob =bob'; n_a} )
+    event_triggered tr alice (Initiating {alice; bob = bob'; n_a} )
   )
   (ensures
     bob == bob'
@@ -304,7 +303,8 @@ let receive_ack_invariant alice keys_sid msg_ts tr =
                   // from the state predicate of the looked up SendingPing state of Alice:
                   assert(event_triggered tr alice (Initiating {alice; bob;n_a}));
 
-                  // from the state predicate of the SendingAck state of bob':
+                  // from the state predicate of the SendingAck state of bob'
+                  // (via the state prediate for the SendinPing state of Alice with bob'):
                   assert(event_triggered tr alice (Initiating {alice; bob = bob'; n_a} ));
 
                   // the injectivity lemma from above, yields bob' = bob

examples/Online_with_authn/DY.OnlineA.Invariants.fst

@@ -19,14 +19,13 @@ open DY.OnlineA.Protocol
 ///   * event invariants
 ///
 /// We then have to show
-/// * these invariants imply the secrecy property (see DY.OnlineS.Secrecy) and
+/// * these invariants imply the security properties: responder authentication and nonce secrecy (see DY.OnlineS.Properties) and
 /// * every protocol step maintains these invariants (see DY.OnlineS.Invariants.Proofs)
 /// With this, we then know that
-/// the protocol model satisfies the secrecy property.
+/// the protocol model satisfies the security properties.
 
 /// We highlight only the differences to
 /// the invariants for the nonce secrecy proof (Online_with_secrecy/DY.OnlineS.Invariants.fst)
-/// 
 
 (*** Crypto Invariants ***)
 
@@ -134,12 +133,6 @@ let state_predicate_p: local_state_predicate state_t = {
         )
     )
     | ReceivedAck rack  -> (
-        (* a ReceivedAck state may only be stored if
-           the stored nonce is labeled for
-           * the storing principal (alice)
-           * the principal stored in the state
-             (the expected sender of the Ack)
-        *)
         let alice = prin in
         let bob = rack.bob in
         let n_a = rack.n_a in
@@ -168,7 +161,7 @@ let state_predicate_p: local_state_predicate state_t = {
 /// we also have prediates on events.
 /// The intuition is similar:
 /// They say when an event is allowed to be triggered, or
-/// what guarantees we obtain, if we observe an event on the trace.
+/// what guarantees we obtain, if we observe a specific event on the trace.
 
 let event_predicate_event_t: event_predicate event_t =
   fun tr prin e ->
@@ -216,11 +209,6 @@ let trace_invariants_p: trace_invariants = {
 
 (*** Protocol Invariants ***)
 
-/// The final protocol invariants
-/// consisting of
-/// * the crypto invariants and
-/// * the trace invariants
-
 instance protocol_invariants_p: protocol_invariants = {
   crypto_invs = crypto_invariants_p;
   trace_invs = trace_invariants_p;

…s/Online_with_authn/DY.OnlineA.Authn.fst …ine_with_authn/DY.OnlineA.Properties.fstexamples/Online_with_authn/DY.OnlineA.Authn.fst renamed to examples/Online_with_authn/DY.OnlineA.Properties.fst examples/Online_with_authn/DY.OnlineA.Authn.fst renamed to examples/Online_with_authn/DY.OnlineA.Properties.fst

@@ -1,4 +1,4 @@
-module DY.OnlineA.Authn
+module DY.OnlineA.Properties
 
 open Comparse
 open DY.Core
@@ -15,7 +15,7 @@ open DY.OnlineA.Invariants
 /// i.e., Bob sent n_a in an acknowledgement to Alice.
 /// Unless one of Alice or Bob are corrupt.
 
-val authn:
+val responder_authentication:
   tr:trace -> 
   alice:principal -> bob:principal ->
   n_a:bytes ->