- 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…
The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.
Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.
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.
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…
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…
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.
- 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…
The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.
Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.
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.
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…
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…
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.