Module Dirsp_exchange_kbb2017.MakeSource

Makes the Kobeissi, Bhargavan and Blanchet (KBB2017) verified security protocol that will delegate to a Proscript runtime library of cryptographic primitives.

Basics

  module P       = Dirsp_proscript_mirage.Make()
  module C       = P.Crypto
  module ED25519 = P.Crypto.ED25519
  module E       = P.Encoding
  module K       = Dirsp_exchange_kbb2017.Make(P)
  module U       = K.UTIL
  module T       = K.TOPLEVEL
  module KEY     = K.Type_key
  module MSG     = K.Type_msg

  (* Alice sends a message to Bob *)
  let aliceSessionWithBob = T.newSession (* ... supply some keys you create with ED25519 and U ... *) ;;
  let aliceToBobSendOutput = T.send
    aliceIdentityKey
    aliceSessionWithBob
    (P.of_string "Hi Bob!")

  (* Now you can send the output "aliceToBobSendOutput" from Alice to Bob.
     Let's switch to Bob's computer. He gets notified using a notification
     library of your choosing and then does ...  *)

  let bobSessionWithAlice = T.newSession (* ... supply some keys ... *);;
  let bobFromAliceReceiveOutput = T.recv
    bobIdentityKey
    bobSignedPreKey
    bobSessionWithAlice
    theEncryptedMessageBobReceivedFromAlice
  assert (bobFromAliceReceiveOutput.output.valid)
  Format.printf "Bob just received a new message: %s\n"
    (bobFromAliceReceiveOutput.plaintext |> P.to_bytes |> Bytes.to_string)

Dirsp_exchange_kbb2017 has a more detailed example.

You must not re-use the sessions!. If you do, Alice and Bob's conversation will lose forward secrecy. Look at Managing State to see how to update the sessions.

The functor Make creates an implementation of the X3DH and Double Rachet protocols. It makes use of a Javascript implementation of the Signal Protocol that was used to prove the soundness of a variant of the "Signal Protocol" (aka X3DH + Double Ratchet) in the paper by the Prosecco research group

Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet.
Automated Verification for Secure Messaging Protocols
  and Their Implementations: A Symbolic and Computational Approach.
2nd IEEE European Symposium on Security and Privacy , Apr 2017, Paris, France.
pp.435 - 450, 2017, <https://www.ieee-security.org/TC/EuroSP2017/>.
<10.1109/EuroSP.2017.38>. <hal-01575923>

We call that paper’s algorithm the Kobeissi, Bhargavan and Blanchet (KBB2017) algorithm to both recognize the paper’s authors and to avoid the use of the trademark "Signal". Please be aware that the variant used in the Automated Verification paper deviates from the original Open Whisper System publications. Make corresponds to the variant in the Automated Verification paper.

Implementation

The Automated Verification paper has a source code repository called proscript-messaging. The authors of dirsp-exchange have a clone of that repository for audit redundancy.

The proscript-messaging directory contains an implementation of X3DH and Double Ratchet in a restricted form of Javascript ("ProScript") suited to security analysis. There is also a small security library written in ProScript called the ProScript Cryptographic Library (PSCL) containing security primitives like SHA-256. proscript-messaging also contains an OCaml parser and an Abstract Syntax Tree (AST) for that restricted Javascript, which it uses to translate the X3DH and Double Ratchet implementations into a few other languages.

With Make:

• the ProScript implementations of X3DH and Double Ratchet are used without modification
• the OCaml parser and OCaml AST are used without modification
• there is a hand-written translator called ps2ocaml from ProScript into OCaml that makes use of the OCaml AST
• there is this functor that wraps the X3DH and Double Ratchet machine translated OCaml into statement-by-statement equivalent OCaml

Please refer to File Structure for Auditing KBB2017 for complete details.

Managing State

The second parameter named them in Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.PROTOCOL.TOPLEVEL.send and Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.PROTOCOL.TOPLEVEL.recv requires special handling. You must set them to the last record_them used in a conversation or you lose forward secrecy!.

We suggest that you use the next section "Serialization and Deserialization" so you can save the last record_them into secure storage, and have it available when you need to send or recv.

Capture the record from the following scenarios:

1. When you create a session with Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.PROTOCOL.TOPLEVEL.newSession, the return value is a record_them.
2. When you send a message with Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.PROTOCOL.TOPLEVEL.send, the return value has an Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_sendoutput.them field which is a record_them.
3. When you receive a message with Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.PROTOCOL.TOPLEVEL.recv, the return value has an Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_recvoutput.them field which is a record_them.

Serialization and Deserialization

The records can all be serialized into and out of protobuf. Here we encode bobFromAliceReceiveOutput2.them from the Summary into bytes, and then we decode those bytes back into its original type Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf.record_them:

  module KBBI = Dirsp_exchange_kbb2017__.Kobeissi_bhargavan_blanchet_intf

  let encoder = KBBI.record_them_to_protobuf P.t_to_protobuf
  let decoder = KBBI.record_them_from_protobuf P.t_from_protobuf

  let (encoded_bytes: Bytes.t) =
    Protobuf.Encoder.encode_exn
      encoder
      bobFromAliceReceiveOutput2.them
  (* You can save the [encoded_bytes] in secure storage *)

  let (decoded_value: K.t KBBI.record_them) =
    Protobuf.Decoder.decode_exn
      decoder
      encoded_bytes
  (* Now you have a [record_them] *)

The complete list of parametric records that can be saved is at Kobeissi_bhargavan_blanchet_intf.

See ppx_deriving_protobuf for details about the protobuf encoding.

Parameters

Signature