Seminarthema: Formalization of Cryptography Using CryptHOL

Formalization of Cryptography Using CryptHOL

Typ:	Seminarthema
Betreuer:	Michael Kirsten
Links:	Paper

In diesem Thema geht es um die flexible Formalisierung kryptographischer Protokolle und die formale Verifikation von deren Sicherheit im CryptHOL-Framework. Dabei lassen sich verschiedene kryptographische Konzepte umsetzen, bspw. spielbasiert [1] oder modular und konstruktiv [2].
Innerhalb des Seminars soll das CryptHOL-Framework vorgestellt, sowie dessen Tauglichkeit für verschiedene kryptographische Konzepte bewertet und verglichen werden. Dies kann darüberhinaus beispielhaft anhand einer Fallstudie [3], die verschiedene solche Konzepte vereint, dargestellt werden.

1. David Basin, Andreas Lochbihler and S. Reza Sefidgar: CryptHOL: Game-Based Proofs in Higher-Order Logic (Journal of Cryptology 33, 2020, Paper)
2. Andreas Lochbihler, S. Reza Sefidgar, David Basin and Ueli Maurer: Formalizing Constructive Cryptography using CryptHOL (32nd Computer Security Foundations Symposium (CSF 2019), IEEE, 2019, Paper)
3. David Butler, Andreas Lochbihler, David Aspinall and Adria Gascón: Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL (Journal of Automated Reasoning 65, 2021, Paper)