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
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 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
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)
These are early releases, especially dirsp-ps2ocaml.
Online docs are at https://diskuv.github.io/dirsp-exchange
Feedback, contributions and downloads are very welcome!