BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game tra...

bblipp · on May 13, 2019

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 · on May 13, 2019

Have those handwritten proofs been published?

bblipp · on May 14, 2019

The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E.

Loq · on May 14, 2019

Thanks.

Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.

bblipp · on May 13, 2019

Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.