Gollmann, DieterDieterGollmann1132276268Gourjon, Marc OlivierMarc OlivierGourjon2024-11-152024-11-152024Technische Universität Hamburg (2024)https://hdl.handle.net/11420/49904The protection of cryptographic implementations against side-channel attacks is essential. Masking is a commonly used countermeasure but manifold pitfalls render this method insecure in practice. This doctoral thesis considers formal verification for qualitative assessments of physical side-channel resilience during development. We show that verification allows masking larger software implementations attaining security in practice at reduced overhead. The work contributes to formal modeling of physical leakage, the first approach to verify model completeness, security reductions and resilient post-quantum cryptography.Der Schutz kryptografischer Implementierungen vor Seitenkanalangriffen ist äußerst wichtig. Die “Masking” Gegenmaßnahme wird dazu oft verwendet, resultiert aber häufig in unsicheren Implementierungen. Diese Arbeit untersucht formale Verifikation als Mittel zur Bewertung der praktischen Seitenkanalresistenz. Sie zeigt, dass formale Verifikation die Entwicklung sicherer Software bei verbesserter Laufzeit ermöglicht und auf größere Anwendungen skaliert. Die Arbeit verbessert die formale Modellierung physikalischer Seitenkanäle, ermöglicht Sicherheitsreduktionen, sowie die Überprüfung der Vollständigkeit eines Models und trägt zu resistenter Post-Quanten-Kryptographie bei.enhttps://creativecommons.org/licenses/by/4.0/Information securityCryptographySide-channelLeakage modelVerifiable securityFormal verificationComputer Science, Information and General Works::005: Computer Programming, Programs, Data and SecurityDoctoral Thesis10.15480/882.1360410.15480/882.13604Eisenbarth, ThomasThomasEisenbarthOther