4 ms·
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.
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.
- 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'.