ISO-DH Example

[fabian-hk]

I finally finished porting the ISO-DH example to the extrinsic DY* code base, and I am happy to receive your feedback.
We should also discuss whether that example is part of the core DY* repository or if it should live in its own repo. Right now, there are a lot of comments and debugging statements. I would like to keep it like that to help others understand it better, but I can understand if that is not something we want in the main repo. In this case, I would create a separate repo with a version that has more details in the code. This separate repo could also serve as an example of how to set up a repository to analyze a protocol with DY*.

[TWal]

Congrats, this looks good!
I left many comments but most of them are minor ones.

The major concern I have is about revealing definitions of DY.Core.Bytes, the lemmas we expose in this module are carefully crafted to vaguely correspond to standard cryptographic assumptions (although it is only best-effort, there is no computational soundness theorem).

I feel like we can probably do the proof without them (e.g. I don't think the original ISO-DH example rely on injectivity of dh_pub?), but I might be mistaken on that.
In any way, it would be interesting to isolate the lemmas that you are missing in DY.Core.Bytes.

Now that you successfully completed an example with DY*-extrinsic, do you have any complaints? Do you see any rough edges that could be polished, or places where you struggled to write the proof for no apparent good reason?

[fabian-hk]

@TWal, I would like to answer your question about my impression of the extrinsic DY*: I like the approach much better than the intrinsic version because you don't have all the complexity at once. In the extrinsic version, I am able to focus first on the model and then think about the proofs.

One thing I was wondering if it could be improved is the code that combines the invariants, because it seems to me that it is always the same (at least in the NSL and ISO-DH example):

/// List of all local state predicates.

let all_sessions = [
  pki_tag_and_invariant;
  private_keys_tag_and_invariant;
  (local_state_dh_session.tag, local_state_predicate_to_local_bytes_state_predicate dh_session_pred);
]

/// List of all local event predicates.

let all_events = [
  (dh_event_instance.tag, compile_event_pred dh_event_pred)
]

/// Create the global trace invariants.

let dh_trace_invs: trace_invariants (dh_crypto_invs) = {
  state_pred = mk_state_predicate dh_crypto_invs all_sessions;
  event_pred = mk_event_pred all_events;
}

instance dh_protocol_invs: protocol_invariants = {
  crypto_invs = dh_crypto_invs;
  trace_invs = dh_trace_invs;
}

/// 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 dh_protocol_invs) all_sessions))
let all_sessions_has_all_sessions () =
  assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sessions)));
  mk_global_local_bytes_state_predicate_correct dh_protocol_invs all_sessions;
  norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate dh_protocol_invs) all_sessions)

val full_dh_session_pred_has_pki_invariant: squash (has_pki_invariant dh_protocol_invs)
let full_dh_session_pred_has_pki_invariant = all_sessions_has_all_sessions ()

val full_dh_session_pred_has_private_keys_invariant: squash (has_private_keys_invariant dh_protocol_invs)
let full_dh_session_pred_has_private_keys_invariant = all_sessions_has_all_sessions ()

val full_dh_session_pred_has_dh_invariant: squash (has_local_state_predicate dh_protocol_invs dh_session_pred)
let full_dh_session_pred_has_dh_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 dh_protocol_invs) 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 dh_protocol_invs all_events;
  norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) 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 dh_protocol_invs) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events))

val full_dh_event_pred_has_dh_invariant: squash (has_event_pred dh_protocol_invs dh_event_pred)
let full_dh_event_pred_has_dh_invariant = all_events_has_all_events ()

Another thing I stumbled over is that is_secret matches labels with ==, which does not take into account the commutativity of labels. For this reason, I got stuck in the proof until I used the equivalent tr function. I was wondering whether we should use the equivalent tr function in the is_secret function?

[TWal]

A few additional comments:

• I wonder why the proofs for compute_message2 and compute_message3 are so different? They do essentially the same thing (computing a signature) but one takes y explicitly as an argument of the lemma, the other introduces x with an exists?
• I noticed that the total code do not output the shared secret? I think functions that verify signatures should also output the shared secret.
• In fact, the total code is not aware of the secret keys (except in compute_message1)? Maybe the total code should take private keys as argument when possible?

[TWal]

@fabian-hk to answer your remarks:

• Indeed, is_secret would be better using equivalent tr. The equivalent relation didn't exist when I wrote is_secret, that's why.
• I agree that merging the predicates is a bit painful, although this is already the second iteration that is much less annoying than before (see 9bfc683), it is still annoying. I opened Reduce boilerplate to merge local predicates #37 for that.

[TWal]

I think this is soon ready to merge, before that the following changes would be great:

• decode_message2 and decode_message3 should return the shared secret, which is currently computed in the stateful code using the dh function, I think cryptography should only be done in the total code (with the exception of the private to public key operations, I guess)
• nit: it would be nice if lemmas on the total code were using the same arguments as the functions that are proved unless there is a good reason, e.g. compute_message1 takes as input gx and gy but the lemma takes as input msg1 (that contains gx) and y (from which we can compute gy)
• nit: remove most of the commented code in Debug.Proof, and maybe replace that with informal explanations? (e.g. "Other ways to do the proof is to call the lemmas explicitly, or to call versions of the lemmas with "forall traces", here we use SMT patterns to do the proof automatically" or something like that)

I can take care of cleaning the proofs in SecurityProperties (or at least, see how much of it can be cleaned, given that they are already quite good!)

[TWal]

It looks good, other than some minor comments!

[qaphla]

Looks good to me.

We may want to think about naming of the properties (as @TWal notes they aren't exactly forward secrecy), but I see no technical problems currently.