Module Dirsp_exchange_kbb2017

For securing a conversation between two parties.

Summary

Dirsp is a short form for Diskuv Implementations of Research Security Protocols. The dirsp-exchange-kbb2017 library implements the Kobeissi, Bhargavan and Blanchet 2017 protocol that is a variant of the Signal Protocol v3 and has been verified using two complementary formal methodologies. It uses a dirsp-proscript library like dirsp-proscript-mirage to provide a runtime library of cryptographic primitives.

Here is the simplest example for an exchange of messages (based on the formal ProVerif secrecy-1-ab-twoway.pv proof test of secrecy):

(*  FIRST: Make some module shortcuts and initialize modules that need it *)
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
(* Initialize the random number generator; Mirage_crypto_rng_lwt works only on *nix *)
let ()         = Mirage_crypto_rng_lwt.initialize ()
;;

(*  SECOND: Let Alice and Bob create their own long-term key pairs.

    Alice keeps her private keys hidden, and Bob keeps his private
    keys hidden. As an implementor of this algorithm, you need to
    make sure there is a secure storage area for each person and place
    the private keys in that storage area.

    Note: The strings (ex. "alice-identity") are documentation hints, and are
    only meaningful during unit testing or proof testing.
*)
let aliceIdentityKey  = U.newIdentityKey (P.of_string "alice-identity")
let aliceSignedPreKey = U.newKeyPair     (P.of_string "alice-signed-prekey")
let bobIdentityKey    = U.newIdentityKey (P.of_string "bob-identity")
let bobSignedPreKey   = U.newKeyPair     (P.of_string "bob-signed-prekey")
;;

(* At any point you can see the contents of a key, message, etc. with `P.hexdump` *)
P.hexdump aliceIdentityKey.pub
;;

(*  THIRD: Alice and Bob exchange a set of long-term public keys.

    As an implementor, the exchange can be simply publishing the long-term keys
    once to a common location (ex. a server) and having each person download
    the other person's public keys.
 *)
let aliceIdentityKeyPub        = aliceIdentityKey.pub
let aliceIdentityDHKeyPub      = U.getDHPublicKey aliceIdentityKey.priv
let aliceSignedPreKeyPub       = aliceSignedPreKey.pub
let aliceSignedPreKeySignature = ED25519.signature (KEY.toBitstring aliceSignedPreKeyPub) aliceIdentityKey.priv aliceIdentityKeyPub
let bobIdentityKeyPub          = bobIdentityKey.pub
let bobIdentityDHKeyPub        = U.getDHPublicKey bobIdentityKey.priv
let bobSignedPreKeyPub         = bobSignedPreKey.pub
let bobSignedPreKeySignature   = ED25519.signature (KEY.toBitstring bobSignedPreKeyPub  ) bobIdentityKey.priv   bobIdentityKeyPub
;;

(*  FOURTH: Alice and Bob create their own prekeys.

    Each prekey has an identifier [Id]. As an implementor of this algorithm, you need
    to make sure there is a secure storage area for each person's prekeys. This storage
    area needs to have lookup by an integer [Id].

    In this example, we create one prekey each person. As an implementator, you should create many.
 *)
let alicePreKey   = U.newKeyPair     (P.of_string "alice-prekey")
let bobPreKey     = U.newKeyPair     (P.of_string "bob-prekey")
;;

(*  FIFTH: Alice consumes one of Bob's one-time prekeys. Bob consumes one of Alice's one-time prekeys.

    By "consume" we mean that once taken, the prekey can no longer be used. As an implementor, you
    need to have a common location (ex. a server) that lets:

    a) each person periodically post a large number of random prekeys
    b) each person consume prekeys that belongs to any other person

    {b CAUTION:} Be aware that "b" is an easy path to denial of service. Use standard anti-DOS
    techniques (ex. authentication, rate limiting on the consumer and the consumee) but inevitably
    that will not be enough. The solution from https://signal.org/docs/specifications/x3dh/#sending-the-initial-message
    is to fallback to an algorithm that uses only the signed prekey; KBB2017 however expects an infinite supply of
    prekeys. We suggest either letting each person post a "last resort" prekey that is used when all prekeys are
    exhausted -or- re-using the last prekey if all but the last prekey are exhausted.
*)
let alicePreKeyPub = alicePreKey.pub
let alicePreKeyId  = 1 (* the Id of alicePreKey *)
let bobPreKeyPub   = bobPreKey.pub
let bobPreKeyId    = 1 (* the Id of bobPreKey   *)
;;

(*  SIXTH: Alice establishes a session with Bob. *)
let aliceSessionWithBob = T.newSession
  aliceSignedPreKey
  alicePreKey
  (KEY.toBitstring bobIdentityKeyPub)
  (KEY.toBitstring bobIdentityDHKeyPub)
  (KEY.toBitstring bobSignedPreKeyPub)
  bobSignedPreKeySignature
  (KEY.toBitstring bobPreKeyPub)
  bobPreKeyId
;;

(*  SEVENTH: Alice sends a message to Bob and updates her session. *)
let aliceToBobMsg1        = P.of_string "Hi Bob!"
let aliceToBobSendOutput1 = T.send
  aliceIdentityKey
  aliceSessionWithBob
  aliceToBobMsg1
;;
Format.printf "Did Alice send successfully? %b\n" aliceToBobSendOutput1.output.valid
;;
(* Alice updates her session or she loses forward secrecy! *)
let updatedAliceSessionWithBob = aliceToBobSendOutput1.them

(*  EIGHTH: Bob establishes his own session with Alice. *)
let bobSessionWithAlice = T.newSession
  bobSignedPreKey
  bobPreKey
  (KEY.toBitstring aliceIdentityKeyPub)
  (KEY.toBitstring aliceIdentityDHKeyPub)
  (KEY.toBitstring aliceSignedPreKeyPub)
  aliceSignedPreKeySignature
  (KEY.toBitstring alicePreKeyPub)
  alicePreKeyId
;;

(*  NINTH: Bob receives the message from Alice and updates his session *)
let bobFromAliceMsg2           = aliceToBobSendOutput1.output
let bobFromAliceReceiveOutput2 = T.recv
  bobIdentityKey
  bobSignedPreKey
  bobSessionWithAlice
  bobFromAliceMsg2
;;
Format.printf "Did Bob receive a message? %b\n"
  bobFromAliceReceiveOutput2.output.valid
;;
Format.printf "Bob just received a new message: %s\n"
  (bobFromAliceReceiveOutput2.plaintext |> P.to_bytes |> Bytes.to_string)
(* Bob updates his session or he loses forward secrecy! *)
let updatedBobSessionWithAlice = bobFromAliceReceiveOutput2.them

The intent of the library is to provide software engineers with auditable source code that has some level of safety assurance (typically proofs) from security researchers. By "auditable" we mean the ability to justify every line of source code when undergoing an audit by a competent security engineer. No third-party vetting of the source code has been conducted (unless noted explicitly), and the original authors at Diskuv did not have security researchers or engineers on staff when the library was originally written. Contact security@diskuv.com to report any security issues, and feel free to shame publicly on Twitter @diskuv if Diskuv is not being responsive.

You may be interested in Comparison to Other Libraries.

See Source Code Verification for help authenticating the source code history.

Institutions

The security research used in dirsp-exchange comes from various research and corporate institutions. Diskuv has no affiliation with any of the institutions below:

1. Signal (formerly Open Whisper Systems), a non-profit organization in the US
2. INRIA (National Institute for Research in Digital Science and Technology), a national research institute of France

Please cite the institutions above rather than Diskuv. In fact, many academic licenses require you to credit the institution by name; see Licenses further below.

Algorithms

X3DH and Double Ratchet

X3DH was created by Open Whisper Systems and placed in the public domain in the publication The X3DH Key Agreement Protocol. That publication defines X3DH as "establish[ing] a shared secret key between two parties who mutually authenticate each other based on public keys. X3DH provides forward secrecy and cryptographic deniability."

X3DH uses The Double Ratchet Algorithm as a building block.

Olm: A Cryptographic Ratchet is a similar algorithm.

Licenses

dirsp-exchange-kbb2017 is distributed under the Apache-2.0 license.

The proscript-messaging source files used in Make are distributed with the following license:

    Copyright (c) 2012-2013 Institut National de Recherche en Informatique et Automatique (Inria Paris-Rocquencourt)
    All rights reserved.

    Redistribution and use in source and binary forms, with or without
    modification, are permitted provided that the following conditions are
    met:

    1. Redistributions of source code must retain the above copyright
        notice, this list of conditions and the following disclaimer.

    2. Redistributions in binary form must reproduce the above
        copyright notice, this list of conditions and the following
        disclaimer in the documentation and/or other materials provided
        with the distribution.

    THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
    IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
    WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
    DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> OR CONTRIBUTORS BE
    LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
    CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
    SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
    BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
    WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
    OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
    IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

    The views and conclusions contained in the software and documentation
    are those of the authors and should not be interpreted as representing
    official policies, either expressed or implied, of the authors.

Source Code Verification

We primarily use an independent third party tool vChain CodeNotary to establish an audit trail of what source code was placed when in this library. vcn lets us both create a trusted timestamp of commits and sign snapshots of third-party repositories, neither of which classical GPG git signing accomplish. Use vcn authenticate --signerID to validate git history.

1. The proscript-messaging source code repository has been forked at https://github.com/diskuv/proscript-messaging for audit redundancy.

   SignerID: 0xdaf31b40f750c92afc50e5750fac6a28da4cedc4
   Code: https://github.com/Inria-Prosecco/proscript-messaging.git@ddb66e4
   Hash: 3354e25ec0e92f6e99a1e26591c8c356d0c7b35b652539b624286c83e89a2a47

Unit Testing

If you need determinism, you can instantiate your own random number generation like the toy example below:

module P = Dirsp_proscript_mirage.CustomizedMake(struct
  include Dirsp_proscript_mirage.DefaultOptions
  (** We use the first byte of MD5(id), and repeat it until we fill the requested size.
      {b DO NOT USE THIS IN PRODUCTION}; only use this in unit tests. *)
  let random_bytes sz id =
    let md5bytes = Digest.string id in
    let firstbyte = String.get md5bytes 0 in
    Bytes.init sz (fun i -> firstbyte)
end)

author

Diskuv, Inc.