Module `Make.TOPLEVEL`

Entry point for sending and receiving messages while maintaining a KBB2017 session.

val newSession : t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_keypair -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_keypair -> t -> t -> t -> t -> t -> int -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_them

newSession mySignedPreKey myPreKey theirIdentityKeyPub theirIdentityDHKeyPub theirSignedPreKeyPub theirSignedPreKeySignature theirPreKeyPub preKeyId creates a KBB2017 session from "my" prekeys and "their" public information while consuming a one-time pre-key preKeyId.

Using nomenclature from the KBB2017 paper, the expectation is that the "their" party has published their long-term Diffie-Hellman public key theirIdentityDHKeyPub and a set of ephemeral Diffie-Hellman public keys (theirSignedPreKeyPub and theirPreKeyPub) called "pre-keys" to a common server or other shared location. The pre-keys include both signed pre-keys mySignedPreKey, which can be reused for some period of time, and non-signed, one-time pre-keys (myPreKey and their preKeyId), which are fresh at each session.

val send : t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_keypair -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_them -> t -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_sendoutput: send myIdentityKey them plaintext sends a plaintext message to them authenticated by myIdentityKey.

val recv : t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_keypair -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_keypair -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_them -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_msg -> t Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_recvoutput

recv myIdentityKey mySignedPreKey them msg receives an encrypted message msg that was ostensibly obtained from them and verifies that it was sent to the session both established with a pre-key signed with mySignedPreKey and authenticated with myIdentityKey.

returns: a Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_recvoutput that, if and only if return_value.output.valid is true, will have valid plaintext