Academic Information
Currently, I am a PhD student at the Chair for Logic and Verification supervised by Prof. Nipkow. My interest is the formalisation and automation of mathematics using interactive theorem provers like Isabelle. Special interests lie in the verification of cryptography, especially post-quantum lattice-based cryptography (eg. CRYSTALS-Kyber) and hardness results of underlying problems.
Before starting as a doctoral candidate, I did both my Masters and Bachelors degree in Mathematics at TUM. During my studies, I spent a semester abroad in Kyoto, Japan, and Exeter, UK.
Furthermore, I have working experience in engeneering of sensors and measurement systems at Micro-Epsilon and in software developement at Atix AG.
From 2021 to 2024, I have been part of the ConVeY DFG Research Training Group.
Please note that with my marriage I changed my last name from Kreuzer to Heidler.
Contact
| {k.kreuzer} AT [tum.de] | |
| Office | MI 00.09.059 |
| Address | Katharina Heidler TUM LS21 Boltzmannstr. 3 85748 Garching Germany |
Publications
Kreuzer, K. (preprint 2023). Verification of the (1–δ)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform. Cryptology ePrint Archive, Paper 2023/027. https://eprint.iacr.org/2023/027
Kreuzer, K., Nipkow, T. (2023). Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. In: Pientka, B., Tinelli, C. (eds) Automated Deduction – CADE 29. CADE 2023. Lecture Notes in Computer Science(), vol 14132. Springer, Cham. https://doi.org/10.1007/978-3-031-38499-8_21
Kreuzer, K. (preprint 2023). Verification of Correctness and Security Properties for CRYSTALS-KYBER. Cryptology ePrint Archive, Paper 2023/087. https://eprint.iacr.org/2023/087
AFP entries
K. Kreuzer, M. Eberl. Van der Waerden’s Theorem. Archive of Formal Proofs, June 2021. https://isa-afp.org/entries/Van_der_Waerden.html, Formal proof development.
T. Ammer, K. Kreuzer. Number Theoretic Transform. Archive of Formal Proofs, August 2022. https://isa-afp.org/entries/Number_Theoretic_Transform.html, Formal proof development.
U. Sulejmani, M. Eberl, K. Kreuzer. The Hales–Jewett Theorem. Archive of Formal Proofs, September 2022. https://isa-afp.org/entries/Hales_Jewett.html, Formal proof development.
K. Kreuzer. CRYSTALS-Kyber. Archive of Formal Proofs, September 2022. https://isa-afp.org/entries/CRYSTALS-Kyber.html, Formal proof development.
K. Kreuzer. CRYSTALS-Kyber Security. Archive of Formal Proofs, December 2023. https://isa-afp.org/entries/CRYSTALS-Kyber_Security.html, Formal proof development.