4 ms·
BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game transformations CryptoVerif produces really only amount to negligible probability t
by Loq 7y ago
BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game transformations CryptoVerif produces really only amount to negligible probability transformations?
- bblipp 7y agoYes, there are hand-written (i.e. not mechanised) proofs that the transformations are sound. But there are no proofs about CryptoVerif's actual code.
- Loq 7y agoHave those handwritten proofs been published?
- bblipp 7y agoYes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.
- bblipp 7y agoThe proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetTDSC07.html https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
- Loq 7y agoThanks. Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.