## Towards an external checker for EasyCrypt

Organisatsiooni nimi

Cryptography

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.

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

Juhendaja

Dominique Unruh

Suhtlemiskeel(ed)

inglise keel

Nõuded kandideerijale

Tase

Magister

Märksõnad

### Kandideerimise kontakt

Nimi

Dominique Unruh

Tel

E-mail