We have also not formally verified the Electron framework’s isolation code. We have not formally verified the soundness of the cryptographic primitives themselves, although writing them in Defensive JavaScript does provide type safety. We consciously never invested any time at all in improving PSCL’s constant time performance because we are well-aware that in the context of the JavaScript runtimes out there, this is pretty much a complete pipe dream.īoth of these things were addressed in our paper, hosted in the same GitHub repository under which this issue was posted. This has been known by us since day 1 and is simply not a goal of our work. Second, the issue complains about PSCL not having a constant time Curve25519 implementation. So I’m not sure why the author of the GitHub issue believed this. The issue begins by claiming that PSCL is supposed to be “formally verified.” In our work on ProScript, we never targeted the cryptographic primitives themselves for verification, and this is not claimed anywhere. Other libraries can be wrapped to do this, and indeed Cryptocat, in many instances, will not use PSCL but actually wrap around native Node.js cryptographic primitives. So, PSCL’s main contribution was actually just a matter of namespace recognition by the ProScript-to-formal-model compiler. For example, if the ProScript compiler sees a call to PSCL’s X25519 implementation, it will automatically translate it to a standard Diffie-Hellman construction in ProVerif.
#Cryptocat forgot password code
PSCL functions used in ProScript code are detected by the ProScript compiler as it produces the applied pi model of the implementation, giving it the ability to convert each call to a cryptographic primitive to a call to the corresponding symbolic function in ProVerif. To quote the original secure messaging paper : In that context, PSCL itself plays a minor role. The main goal of the ProScript research was to try and see how we can write web-based cryptographic protocol implementations that we can automatically translate to formal models. ProScript was again used to implement a reference TLS 1.3 implementation which we also translated and formally verified, providing the first formally verified models for TLS 1.3 drafts before the protocol’s final release.
#Cryptocat forgot password verification
We’ve published research based on ProScript being used to write secure messaging implementations which can then be translated into formal verification models. In this context, “formal verification” strictly means verifying the flow of the protocol logic (eg. ProScript is a functional, strict subset of JavaScript designed specifically for illustrating cryptographic protocol implementations in JavaScript, so that they can then be automatically translated into applied-pi calculus models and formally verified in the symbolic model. It is a shim library based on DJCL that we wrote as a component to help test out ProScript. “PSCL” stands for ProScript Cryptography Library. Thanks for the invitation to this discussion board.
I would like to clarify the context behind this issue.
I am the author responsible for Cryptocat.
0 kommentar(er)
