|Towards an external checker for EasyCrypt|
|Kokkuvõte||When checked by humans, the security of proofs for cryptographic protocols are inherently error-prone. One way out is to use formal (i.e., computer-aided) verification. Probably the most popular tool today for this purpose is EasyCrypt, which allows to interactively design a proof that the computer will be able to understand and check.|
However, EasyCrypt is complex monolithic software. To increase the trust in EasyCrypt, we would like to “export” the proof steps performed in a proof in some file format that is as simple as possible, and then be able to verify them step-by-step with an external tool (or possibly using a general purpose theorem prover like Isabelle/HOL).
The purpose of this thesis is to develop such an export and a prototype for such a checker. This will involve understanding the EasyCrypt source code and patching it to support suitable export.
|Lõputöö kaitsmise aasta||2019-2020|
|Märksõnad||#tcs #crypto #verification|