Closed bwesterb closed 3 months ago
LGTM.
We do need a separate proof for the combined KEM, using the fact that we include the X25519 public key and ephemeral public key, otherwise we do not get HON-BIND-K-PK/HON-BIND-K-CT. We could also shorten the list of misbinding properties to only list the MAL-BIND properties, since the others are true a fortiori.
@bwesterb we should update the eprint with the MAL-BIND proof(s)
LGTM.
We do need a separate proof for the combined KEM, using the fact that we include the X25519 public key and ephemeral public key, otherwise we do not get HON-BIND-K-PK/HON-BIND-K-CT. We could also shorten the list of misbinding properties to only list the MAL-BIND properties, since the others are true a fortiori.