Cryptographically Faithful Proofs of Security Protocols

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.