Skip to main content
SpringerLink
Log in

Deduction with XOR Constraints in Security API Modelling

  • Conference paper
Automated Deduction – CADE-20 (CADE 2005)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3632))

Included in the following conference series:

Abstract

We introduce XOR constraints, and show how they enable a theorem prover to reason effectively about security critical subsystems which employ bitwise XOR. Our primary case study is the API of the IBM 4758 hardware security module. We also show how our technique can be applied to standard security protocols.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Antoniou, G., Ohlbach, H.J.: TERMINATOR. In: International Joint Conference on Artificial Intelligence, pp. 916–919 (1983)

    Google Scholar 

  2. Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 462–476. Springer, Heidelberg (1992)

    Google Scholar 

  3. Basin, D., Mödersheim, S., Viganò, L.: An on-the-fly model-checker for security protocol analysis. In: Proceedings of the, European Symposium on Research in Computer Security, pp. 253–270, Extended version available as Technical Report 404, ETH Zurich (2003)

    Google Scholar 

  4. Bond, M.: Understanding Security APIs. PhD thesis, University of Cambridge (2004)

    Google Scholar 

  5. Bond, M., Anderson, R.: API level attacks on embedded systems. IEEE Computer Magazine, 67–75 (October 2001)

    Google Scholar 

  6. Bundy, A. (ed.): CADE 1994. LNCS, vol. 814. Springer, Heidelberg (1994)

    MATH  Google Scholar 

  7. Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Kolaitis [15], pp. 261–270

    Google Scholar 

  8. Chevalier, Y., Vigneron, L.: Automated unbounded verification of security protocols. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 324–337. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Clulow, J.: The design and analysis of cryptographic APIs for security devices. Master’s thesis, University of Natal, Durban (2003)

    Google Scholar 

  10. Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Kolaitis [15], pp. 271–281

    Google Scholar 

  11. Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: CCS 2004: Proceedings of the 11th ACM conference on Computer and communications security, pp. 278–287. ACM Press, New York (2004)

    Chapter  Google Scholar 

  12. Ganapathy, V., Seshia, S.A., Jha, S., Reps, T.W., Bryant, R.E.: Automatic discovery of API-level exploits. In: ICSE 2005: Proceedings of the 27th International Conference on Software Engineering, New York, NY, USA, May 2005, pp. 312–321. ACM Press, New York (2005)

    Chapter  Google Scholar 

  13. Godoy, G., Nieuwenhuis, R.: Superposition with completely built-in abelian groups. J. Symb. Comput. 37(1), 1–33 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  14. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Kolaitis, P.G.: Proceedings 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, June 22-25. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  16. Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Computers and Security 11(1), 75–89 (1992)

    Article  Google Scholar 

  17. Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56(3), 131–133 (1995)

    Article  MATH  Google Scholar 

  18. Lowe, G.: Breaking and fixing the Needham Schroeder public-key protocol using FDR. In: Proceedings of TACAS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Google Scholar 

  19. Millen, J.K.: On the freedom of decryption. Inf. Process. Lett. 86(6), 329–333 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  20. Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 477–491. Springer, Heidelberg (1992)

    Google Scholar 

  21. R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: No AC-unifiers needed. In: Bundy [6], pages 545–559.

    Google Scholar 

  22. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier and MIT Press (2001)

    Google Scholar 

  23. Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6, 85–128 (1998)

    Google Scholar 

  24. Steel, G.: Visualising first-order proof search. In: Workshop on User Interfaces for Theorem Provers (UITP 2005), Edinburgh, Scotland, April 2005, pp. 179–189 (2005)

    Google Scholar 

  25. Vigneron, L.: Associative-commutative deduction with constraints. In: Bundy [6], pp. 530–544

    Google Scholar 

  26. Weidenbach, C., et al.: System description: Version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 378–382. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Informatics, University of Edinburgh, Edinburgh, EH8 9LE, Scotland

    Graham Steel

Authors
  1. Graham Steel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technical University of Catalonia, Barcelona

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Steel, G. (2005). Deduction with XOR Constraints in Security API Modelling. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_24

Download citation

  • DOI: https://doi.org/10.1007/11532231_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28005-7

  • Online ISBN: 978-3-540-31864-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation