Extending Dolev-Yao with Assertions

  • R. Ramanujam
  • Vaishnavi Sundararajan
  • S. P. Suresh
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8880)


Cryptographic protocols often require principals to send certifications asserting partial knowledge of terms (for instance, that an encrypted secret is 0 or 1). Such certificates are themselves modelled by cryptographic primitives or sequences of communications. For logical analysis of such protocols based on the Dolev-Yao model [12], we suggest that it is useful to separate terms and assertions about them in communications. We propose a perfect assertion assumption by which the underlying model ensures the correctness of the assertion when it is generated. The recipient may then rely on the certificate but may only forward it as second-hand information. We use a simple propositional modal assertion language involving disjunction (for partial knowledge) and formulas of the form A says α (for delegation). We study the complexity of the term derivability problem and safety checking in the presence of an active intruder (for bounded protocols). We show that assertions add complexity to verification, but when they involve only boundedly many disjunctions, the complexity is the same as that of the standard Dolev-Yao model.


Knowledge State Trusted Third Party Disjunctive Normal Form Cryptographic Protocol Protocol State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Needham, R.M.: Prudent engineering practices for cryptographic protocols. IEEE Transactions on Software Engineering 22, 6–15 (1996)CrossRefGoogle Scholar
  2. 2.
    Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol. 963, pp. 236–247. Springer, Heidelberg (1995)Google Scholar
  3. 3.
    Backes, M., Hriţcu, C., Maffei, M.: Type-checking zero-knowledge. In: ACM Conference on Computer and Communications Security, pp. 357–370 (2008)Google Scholar
  4. 4.
    Backes, M., Maffei, M., Unruh, D.: Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. In: IEEE Symposium on Security and Privacy, pp. 202–215 (2008)Google Scholar
  5. 5.
    Baskar, A., Naldurg, P., Raghavendra, K.R., Suresh, S.P.: Primal Infon Logic: Derivability in Polynomial Time. In: Proceedings of FSTTCS 2013. LIPIcs, vol. 24, pp. 163–174 (2013)Google Scholar
  6. 6.
    Baskar, A., Ramanujam, R., Suresh, S.P.: A dexptime-complete dolev-yao theory with distributive encryption. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 102–113. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)CrossRefGoogle Scholar
  8. 8.
    Benaloh, J.: Cryptographic capsules: A disjunctive primitive for interactive protocols. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol. 263, pp. 213–222. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  9. 9.
    Comon, H., Shmatikov, V.: Intruder Deductions, Constraint Solving and Insecurity Decisions in Presence of Exclusive or. In: Proceedings of LICS 2003, pp. 271–280 (June 2003)Google Scholar
  10. 10.
    Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)Google Scholar
  11. 11.
    Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), 435–487 (2009)Google Scholar
  12. 12.
    Dolev, D., Yao, A.: On the Security of public-key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Fuchsbauer, G., Pointcheval, D.: Anonymous consecutive delegation of signing rights: Unifying group and proxy signatures. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol. 5458, pp. 95–115. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Gurevich, Y., Neeman, I.: Infon logic: the propositional case. ACM Transactions on Computational Logic 12(2), 9:1–9:28 (2011)Google Scholar
  15. 15.
    Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of abelian groups with distributive encryption. Information and Computation 205(4), 581–623 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Ramanujam, R., Sundararajan, V., Suresh, S.P.: Extending Dolev-Yao with assertions. Technical Report (2014),
  17. 17.
    Rjaskova, Z.: Electronic voting schemes. Master’s Thesis, Comenius University (2002)Google Scholar
  18. 18.
    Rusinowitch, M., Turuani, M.: Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete. Theoretical Computer Science 299, 451–475 (2003)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • R. Ramanujam
    • 1
  • Vaishnavi Sundararajan
    • 2
  • S. P. Suresh
    • 2
  1. 1.Institute of Mathematical Sciences ChennaiIndia
  2. 2.Chennai Mathematical InstituteChennaiIndia

Personalised recommendations