Provable Security at Implementation Level (PSI)
The goal of this project is to develop theoretical models in which formally provable security guarantees can be made concerning the implementation (both in hardware and in software) of cryptographic algorithms and protocols. Furthermore, this project investigates the security of existing implementations under these models, and designs new, provably secure implementations if existing alternatives fall short of being provably secure.
In recent years, provable security has become the standard way of designing cryptographic protocols. Nevertheless, successful attacks on practical systems implementing these supposedly provably secure protocols are continuing to be published. Only rarely are these the consequence of errors contained in the security proof. More commonly, they are due to real-world adversaries breaking the cryptography by stepping outside of the model (e.g. timing- and power-analysis attacks), or one that bypasses the cryptography altogether by exploiting vulnerabilities in the surrounding software (e.g. buffer-overflow attacks). Heuristic methods to counteract such attacks exist, but relying on these to implement a provably secure primitive wastes the strong guarantees offered by the security proof. Instead, this project advocates to maintain a high security standard throughout the implementation, and intends to develop protocols and implementation techniques of which the security can be evaluated in a mathematically rigorous way.