package dirsp-exchange-kbb2017

You can search for identifiers within the package.

in-package search v0.2.0

dirsp-exchange-kbb2017
- Dirsp_exchange_kbb2017
  - Make
    
    HANDLE
    
    ProScript
    
    Crypto
    
    ED25519
    
    Encoding
    
    RATCHET
    
    TOPLEVEL
    
    Type_iv
    
    Type_key
    
    Type_keypair
    
    Type_msg
    
    Type_recvoutput
    
    Type_sendoutput
    
    Type_them
    
    UTIL

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 record_recvoutput that, if and only if return_value.output.valid is true, will have valid plaintext