[ANN] First releases of dirsp-exchange: auditable variant of Signal Protocol and ProScript-to-OCaml translator

I’m pleased to announce the first release of dirsp-exchange, available today from the Opam repositories.

The intent of the [dirsp] libraries is to provide software engineers with auditable source code that has some level of safety assurance (typically proofs) from security researchers.

The first libraries are:

  • dirsp-exchange-kbb2017 0.1.0 - The KBB2017 protocol for securing a two-party conversation. Similar to Signal Protocol v3 and Olm Cryptographic Ratchet.
  • dirsp-ps2ocaml 0.1.0 - A ProScript to OCaml translator. ProScript is an executable subset of JavaScript that can be formally verified.

and a couple more supporting libraries.

dirsp-exchange-kbb2017 has a build process that generates its own OCaml code using dirsp-ps2ocaml on formally verified ProScript source code.

The canonical example for dirsp-exchange-kbb2017 is:

module P       = Dirsp_proscript_mirage.Make()
module ED25519 = P.Crypto.ED25519
module K       = Dirsp_exchange_kbb2017.Make(P)
module U       = K.UTIL

(* Alice sends a message to Bob *)
let aliceSessionWithBob = T.newSession (* ... supply some keys you create with ED25519 and U ... *) ;;
let aliceToBobSendOutput = T.send
  (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 of a new message using a notification library of your choosing, and then does ...  *)

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

These are early releases, especially dirsp-ps2ocaml.

Online docs are at https://diskuv.github.io/dirsp-exchange

Feedback, contributions and downloads are very welcome!


Wow! What an unexpected and welcome contribution!

Appreciate the comment!

1 Like