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