The WebAssembly used in this demo is generated from
F* sources using the
KreMLin compiler. The F* implementation, contains the cryptographic
top-level functions of the Signal protocol like
respond. F* is a verification framework, that we use to
prove three properties about this Signal protocol implementation:
What you can see below is Signal* running in your browser and passing some of the tests from the Signal protocol test suite. This proof of concept shows that Signal* can be made to interoperate with actual Signal-based web applications like Whatsapp or Signal.
If you have comments, questions or suggestions, you can contact the authors of the paper: Jonathan Protzenko (firstname.lastname@example.org), Benjamin Beurdouche (email@example.com), Denis Merigoux (firstname.lastname@example.org) and Karthikeyan Bhargavan (email@example.com).