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.
- M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102--146, Jan. 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (the Computational Soundness of Formal Encryption). J. Cryptology, 15(2):103--127, 2002.Google ScholarDigital Library
- M. Baudet. Random Polynomial-time Attacks and Dolev-Yao Models. Journal of Automata, Languages and Combinatorics, 11(1):7--21, 2006.Google Scholar
- B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop, pages 86--100, 2001. Google ScholarDigital Library
- D. Dolev and A.C. Yao. On the Security of Public-Key Protocols. IEEE Transaction on Information Theory, 2(29):198--208, March 1983.Google ScholarDigital Library
- O. Goldreich. Modern Cryptography, Probabilistic Proofs, and Pseudorandomness. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1998. Google ScholarDigital Library
- G. Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Inf. Process. Lett., 56(3):131--133, 1995. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, June 1999. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Zunino and P. Degano. A Note on the Perfect Encryption Assumption in a Process Calculus. In FoSSaCS, pages 514--528, 2004.Google ScholarCross Ref
- R. Zunino and P. Degano. Weakening the Perfect Encryption Assumption in Dolev-Yao Adversaries. Theor. Comput. Sci., 340(1):154--178, 2005. Google ScholarDigital Library
Index Terms
- Weakening the Dolev-Yao model through probability
Recommendations
Limits of the BRSIM/UC soundness of Dolev–Yao-style XOR
The abstraction of cryptographic operations by term algebras, called Dolev–Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev–Yao models can be sound ...
A dolev-yao-based definition of abuse-free protocols
ICALP'06: Proceedings of the 33rd international conference on Automata, Languages and Programming - Volume Part IIWe propose a Dolev-Yao-based definition of abuse freeness for optimistic contract-signing protocols which, unlike other definitions, incorporates a rigorous notion of what it means for an outside party to be convinced by a dishonest party that it has ...
Equivocating Yao: Constant-Round Adaptively Secure Multiparty Computation in the Plain Model
Yao's circuit garbling scheme is one of the basic building blocks of cryptographic protocol design. Originally designed to enable two-message, two-party secure computation, the scheme has been extended in many ways and has innumerable applications. ...
Comments