Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach

ABSTRACT

In the Horn theory based approach for cryptographic protocol analysis, cryptographic protocols and (Dolev-Yao) intruders are modeled by Horn theories and security analysis boils down to solving the derivation problem for Horn theories. This approach and the tools based on this approach, including ProVerif, have been very successful in the automatic analysis of cryptographic protocols w.r.t. an unbounded number of sessions. However, dealing with the algebraic properties of operators such as the exclusive OR (XOR) has been problematic. In particular, ProVerif cannot deal with XOR.

In this paper, we show how to reduce the derivation problem for Horn theories with XOR to the XOR-free case. Our reduction works for an expressive class of Horn theories. A large class of intruder capabilities and protocols that employ the XOR operator can be modeled by these theories. Our reduction allows us to carry out protocol analysis by tools, such as ProVerif, that cannot deal with XOR, but are very efficient in the XOR-free case. We implemented our reduction and, in combination with ProVerif, applied it in the automatic analysis of several protocols that use the XOR operator. In one case, we found a new attack.

REFERENCES

• 1: CCA Basic Services Reference and Guide: CCA Basic Services Reference and Guide, 2003. Available at http://www-306.ibm.com/security/cryptocards/pdfs/CCA_Basic_Services_241_Revised_20030918.pdf.
• 2: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 3: Bruno Blanchet. Automatic verification of correspondences for security protocols, 2008. Report arXiv:0802.3444v1. Available at http://arxiv.org/abs/0802.3444v1.
• 4: Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming, 75(1):3--51, 2008.
• 5: Mike Bond, Attacks on Cryptoprocessor Transaction Sets, Proceedings of the Third International Workshop on Cryptographic Hardware and Embedded Systems, p.220-234, May 14-16, 2001
• 6: J.A. Bull and D.J. Otway. The authentication protocol. Technical Report DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03, Defence Research Agency, Malvern, UK, 1997.
• 7: Yannick Chevalier , Ralf Küsters , Michaël Rusinowitch , Mathieu Turuani, An NP Decision Procedure for Protocol Insecurity with XOR, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.261, June 22-25, 2003
• 8: J. Clulow. The design and analysis of cryptographic APIs for security devices, 2003. Master's thesis, University of Natal, Durban.
• 9: H. Comon-Lundh and V. Cortier. New Decidability Results for Fragments of First-order Logic and Application to Cryptographic Protocols. In Proc. of RTA 2003, vol. 2706 of LNCS, pages 148--164. Springer, 2003.
• 10: H. Comon-Lundh , V. Shmatikov, Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.271, June 22-25, 2003
• 11: Hubert Comon-Lundh , Véronique Cortier, Security properties: two agents are sufficient, Science of Computer Programming, v.50 n.1-3, p.51-71, March 2004 [doi>10.1016/j.scico.2003.12.002]
• 12: Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: How to get rid of some algebraic properties. In Proc. of RTA 2005, vol. 3467 of LNCS, pages 294--307. Springer, 2005.
• 13: Veronique Cortier , Stephanie Delaune , Graham Steel, A Formal Theory of Key Conjuring, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.79-96, July 06-08, 2007 [doi>10.1109/CSF.2007.5]
• 14: V. Cortier, G. Keighren, and G. Steel. Automatic Analysis of the Security of XOR-Based Key Management Schemes. In Proc. of TACAS 2007, vol. 4424 of LNCS, pages 538--552. Springer, 2007.
• 15: R. Küsters and T. Truderung. On the Automatic Analysis of Recursive Security Protocols with XOR. In Proc. of STACS 2007, vol. 4393 of LNCS, pages 646--657. Springer, 2007.
• 16: R. Küsters and T. Truderung. Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach. Implementation, 2008. Available at http://infsec.uni-trier.de/software/KuestersTruderung-XORPROVERIF-2008.zip.
• 17: R. Küsters and T. Truderung. Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach. Report arXiv:0808.0634v1, 2008. Available at http://arxiv.org/abs/0808.0634v1.
• 18: V. Shoup and A. Rubin. Session key distribution using smart cards. In Proc. of EUROCRYPT 1996, vol. 1070 of LNCS, pages 321--331. Springer, 1996.
• 19: Graham Steel. Deduction with XOR constraints in security API modelling. In CADE, vol. 3632 of LNCS, pages 322--336. Springer, 2005.
• 20: K.N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational Horn clauses. In Proc. of CADE 2005, vol. 3328 of LNCS, pages 337--352. Springer, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Security, Verification

Keywords:
algebraic properties, security protocols