Extending Dolev-Yao with Assertions
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 , 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.
KeywordsKnowledge State Trusted Third Party Disjunctive Normal Form Cryptographic Protocol Protocol State
Unable to display preview. Download preview PDF.
- 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.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.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.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
- 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.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.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
- 14.Gurevich, Y., Neeman, I.: Infon logic: the propositional case. ACM Transactions on Computational Logic 12(2), 9:1–9:28 (2011)Google Scholar
- 16.Ramanujam, R., Sundararajan, V., Suresh, S.P.: Extending Dolev-Yao with assertions. Technical Report (2014), http://www.cmi.ac.in/~spsuresh/dyassert.pdf
- 17.Rjaskova, Z.: Electronic voting schemes. Master’s Thesis, Comenius University (2002)Google Scholar