Cryptographically Faithful Proofs of Security Protocols
Status
This project started in February 2004 and ended in July 2008.
Researchers
Dr. Michael Backes, Uni Saarland
Prof. Dr. David Basin, Information Security Group, ETH
Prof. Dr. Birgit Pfitzmann, IBM Zurich Research Laboratory, Zurich, Switzerland
Dr. Christoph Sprenger, Information Security Group, ETH
Dr. Michael Waidner, Fraunhofer SIT
Background and Motivation
Computational security definitions are formulated in terms of a probabilistic polynomial-time attacker having a negligible probability of success to break a given protocol or primitive. Cryptographers typically reduce protocol security proofs to the security of the underlying cryptographic primitives. Such proofs are often long, difficult and prone to human errors due to the lack of tool assistance. On the other hand, tools do exist for protocol verification in symbolic Dolev-Yao models. However, since these models abstract completely from computational issues and assume that cryptography is perfect (i.e., unbreakable), they usually lack a rigorous cryptographic justification. We aim at combining the best of both worlds: tool-supported symbolic proofs with strong cryptographic guarantees.
Publications & Further Information
Christoph Sprenger and David Basin
Cryptographically-sound Protocol-model Abstractions
In Proceedings of Computer Security Foundations (CSF ’08), IEEE Computer Society, 2008.
Christoph Sprenger and David Basin
Cryptographically-sound Protocol-model Abstractions
In Proceedings of Logic in Computer Science (LICS ’08), IEEE Computer Society, 2008.
Christoph Sprenger and David Basin
A monad-based modeling and verification toolbox with application to security protocols
Theorem Proving in Higher-Order Logics (TPHOLs), Lecture Notes in Computer Science, vol. 4732, pp. 301-317, Springer-Verlag, 2007
Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann and Michael Waidner
Cryptographically Sound Theorem Proving
In Proceedings of Computer Security Foundations Workshop, CSFW06, Venice, pp. 153-166, July 2006.