Weakening the Dolev-Yao model through probability

ABSTRACT

The Dolev-Yao model has been widely used in protocol verification and has been implemented in many protocol verifiers. There are strong assumptions underlying this model, such as perfect cryptography: the aim of the present work is to propose an approach to weaken this hypothesis, by means of probabilistic considerations on the strength of cryptographic functions. Such an approach may effectively be implemented in actual protocol verifiers. The Yahalom protocol is used as an easy example to show this approach.

REFERENCES

• 1: M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102--146, Jan. 2005.
• 2: M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and Proofs of Protocol Security: A Progress Report. In 21st International Conference on Computer Aided Verification (CAV'09), Lecture Notes on Computer Science, Grenoble, France, July 2009. Springer Verlag. To appear.
• 3: M. Abadi and C. Fournet. Mobile Values, New Names, and Secure Communication. In POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 104--115, New York, NY, USA, 2001. ACM.
• 4: M. Abadi and A.D. Gordon. A Calculus for Cryptographic Protocols: The spi calculus. In Fourth ACM Conference on Computer and Communications Security, pages 36--47. ACM Press, 1997.
• 5: M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (the Computational Soundness of Formal Encryption). J. Cryptology, 15(2):103--127, 2002.
• 6: M. Baudet. Random Polynomial-time Attacks and Dolev-Yao Models. Journal of Automata, Languages and Combinatorics, 11(1):7--21, 2006.
• 7: B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop, pages 86--100, 2001.
• 8: D. Dolev and A.C. Yao. On the Security of Public-Key Protocols. IEEE Transaction on Information Theory, 2(29):198--208, March 1983.
• 9: O. Goldreich. Modern Cryptography, Probabilistic Proofs, and Pseudorandomness. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1998.
• 10: G. Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Inf. Process. Lett., 56(3):131--133, 1995.
• 11: G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In TACAs '96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pages 147--166, London, UK, 1996. Springer-Verlag.
• 12: R. Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, June 1999.
• 13: J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A Probabilistic Polynomial-Time Calculus for Analysis of Cryptographic Protocols. In Electronic Notes in Theoretical Computer Science, 2001.
• 14: R. Zunino and P. Degano. A Note on the Perfect Encryption Assumption in a Process Calculus. In FoSSaCS, pages 514--528, 2004.
• 15: R. Zunino and P. Degano. Weakening the Perfect Encryption Assumption in Dolev-Yao Adversaries. Theor. Comput. Sci., 340(1):154--178, 2005.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

General Terms:
Verification

Keywords:
protocol verification