Numerous attacks have been found on cryptographic protocols that were long thought to be secure. Formal logic-based approaches to verify protocol security have helped to find such attacks; however, these approaches have limited applicability, in particular with respect to more powerful attackers as those modeled by computational complexity or those capable of detecting side channel leakage.
To solve this, our project aims at integrating the logical / formal approaches with (A) complexity theory and (B) information theory. The first direction aims at establishing the foundations of logical verification for security in the computational sense, with the ultimate goal of automatically finding attacks that probabilistic polynomial-time adversaries can carry out on protocols. The second direction aims at developing frameworks and techniques for evaluating and reducing information leakage caused by adaptive attackers.