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.

The 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.