Introducing Commutative and Associative Operators in Cryptographic Protocol Analysis

  • Ivan Cibario Bertolotti
  • Luca Durante
  • Riccardo Sisto
  • Adriano Valenzano
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


Many formal techniques for the verification of cryptographic protocols rely on the abstract definition of cryptographic primitives, such as shared, private, and public key encryption. This approach prevents the analysis of those protocols that explicitly use commutative and associative algebraic operators to build their messages such as, for example, the Diffie-Hellman key-exchange protocol. This paper investigates the possibility of handling operators which exhibit special properties by considering a stand-alone extension to the way most known popular techniques handle messages exchanged during the protocol sessions. Such an extension makes the new operators tractable by automatic model checking techniques. The properties examined in this paper are commutativity and associativity.


Canonical Form Cryptographic Protocol Commutative Operator Associative Operator Closure Rule 
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.


  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols. The spi calculus. Information and Computation 148(1), 1–70 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Boreale, M., Buscemi, M.G.: A framework for the analysis of security protocols. In: Proceedings of CONCUR 2001. Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Boreale, M., Nicola, R.D., Pugliese, R.: Proof techniques for cryptographic processes. In: Proceedings of 14th IEEE LICS, pp. 157–166. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  4. 4.
    Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. To appear in Proc. of 18th IEEE LICS 2003 (2003) Google Scholar
  5. 5.
    Bertolotti, I.C., Durante, L., Sisto, R., Valenzano, A.: A new knowledge representation strategy for cryptographic protocol analysis. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 284–298. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Clarke, E.M., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proceedings of IFIP PROCOMET, pp. 87–106. Chapman & Hall, London (1998)Google Scholar
  7. 7.
    Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9(4), 443–487 (2000)CrossRefGoogle Scholar
  8. 8.
    Comon-Lundh, H., Shmatikov, V.: Constraint solving and insecurity decision in presence of exclusive or. To appear in Proc. of 18th IEEE LICS 2003 (June 2003) Google Scholar
  9. 9.
    Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Theory 22(6), 644–654 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  12. 12.
    Lowe, G.: Casper: a compiler for the analysis of security protocols. In: Proceedings of 10th IEEE CSFW, pp. 18–30. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  13. 13.
    Lowe, G.: Towards a completeness result for model checking security protocols. Journal of Computer Security 7(2–3), 89–146 (1999)CrossRefGoogle Scholar
  14. 14.
    Marrero, W., Clarke, E.M., Jha, S.: A model checker for authentication protocols. In: DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)Google Scholar
  15. 15.
    Meadows, C., Narendran, P.: A unification algorithm for the group Diffie-Hellman protocol. In: Proceedings of WITS 2002 (2002) Google Scholar
  16. 16.
    Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie-Hellman exponentiation. To appear in Proc. of 16th IEEE CSFW (June 2003) Google Scholar
  17. 17.
    Millen, J.K., Clark, S.C., Freedman, S.B.: The Interrogator: Protocol security analysis. IEEE Transactions on Software Engineering 13(2), 274–288 (1987)CrossRefGoogle Scholar
  18. 18.
    Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 149–163. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  19. 19.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)CrossRefGoogle Scholar
  20. 20.
    Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proceedings of 14th IEEE CSFW, pp. 174–187. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  21. 21.
    Schneider, S.: Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering 24(9), 741–758 (1998)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Ivan Cibario Bertolotti
    • 1
  • Luca Durante
    • 1
  • Riccardo Sisto
    • 2
  • Adriano Valenzano
    • 1
  1. 1.IEIIT – CNRItaly
  2. 2.Dipartimento di Automatica e InformaticaPolitecnico di TorinoTorinoItaly

Personalised recommendations