bblipp

4 ms·

1. 1.▲
   by bblipp 7y ago

   - CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1]; - There is no verified kernel. All algorithms, including an equational prover for simplification of games, are implemented in ~30k to 40k LOC of O
2. 2.▲
   by bblipp 7y ago

   The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
3. 3.▲
   by bblipp 7y ago

   Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.
4. 4.▲
   by bblipp 7y ago

   Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.
5. 5.▲
   by bblipp 7y ago

   Yes, there are hand-written (i.e. not mechanised) proofs that the transformations are sound. But there are no proofs about CryptoVerif's actual code.
6. 6.▲
   by bblipp 7y ago

   Games is the terminology of cryptographers, that's why we use it in our work; we need it to interface with this community. The reason this term is used in cryptography might be historical, but also, speaking of an adversary that shou
7. 7.▲
   by bblipp 7y ago

   CryptoVerif [1] is called “automatic” because 1) it generates intermediate games automatically during the proof [see footnote1 for a brief explanation of “games”]. This is in contrast to the other major tool that works in the computational
8. 8.▲
   by bblipp 7y ago

   I am one of the authors of the paper. Feel free to ask questions about our work, I'll try to monitor this thread and come back to answer.