Advertisement

Model–Based Testing of Cryptographic Protocols

  • Dean Rosenzweig
  • Davor Runje
  • Wolfram Schulte
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)

Abstract

Modeling is a popular way of representing the behavior of a system. A very useful type of model in computing is an abstract state machine which describes transitions over first order structures. The general purpose model-based testing tool SpecExplorer (used within Microsoft, also available externally) uses such a model, written in AsmL or Spec#, to perform a search that checks that all reachable states of the model are safe, and also to check conformance of an arbitrary .NET implementation to the model. Spec Explorer provides a variety of ways to cut down the state space of the model, for instance by finitizing parameter domains or by providing predicate abstraction. It has already found subtle bugs in production software.

First order structures and abstract state machines over them are also a useful way to think about cryptographic protocols, since models formulated in these terms arise by natural abstraction from computational cryptography.

In this paper we explain this abstraction process, ‘experiments as structures’, and argue for its faithfulness. We show how the Dolev–Yao intruder model fits into SpecExplorer. In a word, the actions of the Dolev–Yao intruder are the ‘controllable’ actions of the testing framework, whereas the actions of protocol participants are the ‘observable’ actions of the model. The unsafe states are the states violating say Lowe’s security guarantees. Under this view, the general purpose software testing tool quickly finds known attacks, such as Lowe’s attack on the Needham–Schroeder protocol.

Keywords

Encryption Scheme Turing Machine Cryptographic Protocol Negligible Probability Pairing Scheme 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [ABS05]
    Adão, P., Bana, G., Scedrov, A.: Computational and information theoretic soundness and completeness of formal encryption. In: 18th IEEE Computer Security Foundations Workshop – CSFW 2005 (2005)Google Scholar
  2. [AJ01]
    Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 82. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. [AR02]
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)zbMATHMathSciNetGoogle Scholar
  4. [Ban04]
    Bana, G.: Soundness and Completeness of Formal Logics of Symmetric Encryption. PhD thesis, University of Pennsylvania (2004)Google Scholar
  5. [BDPR98]
    Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among notions of security for public–key encryption schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, p. 26. Springer, Heidelberg (1998)Google Scholar
  6. [BG00]
    Blass, A., Gurevich, Y.: Background, reserve, and gandy machines. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, p. 1. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. [BG03]
    Blass, A., Gurevich, Y.: Algortihms: A quest for absolute definitions. Bulletin of the European Association for Theoretical Computer Science 81, 195–225 (2003)zbMATHMathSciNetGoogle Scholar
  8. [BG04a]
    Blass, A., Gurevich, Y.: Ordinary interactive small–step algorithms I. Technical Report MSR-TR-2004-16, Microsoft Research (2004)Google Scholar
  9. [BG04b]
    Blass, A., Gurevich, Y.: Ordinary interactive small–step algorithms II. Technical Report MSR-TR-2004-88, Microsoft Research (2004)Google Scholar
  10. [Gur00]
    Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic 1(1), 77–111 (2000)CrossRefMathSciNetGoogle Scholar
  11. [Gur05]
    Gurevich, Y.: Interactive algorithms 2005. Technical Report MSR-TR-2005-73, Microsoft Research (2005)Google Scholar
  12. [HG03]
    Horvitz, O., Gligor, V.: Weak key authenticity and the computational completeness of formal encryption. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 530–547. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. [MW04a]
    Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway language of encrypted expressions. Journal of Computer Security 12(1), 99–130 (2004)Google Scholar
  14. [MW04b]
    Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. [RR05]
    Rosenzweig, D., Runje, D.: Some things algorithms cannot do. Technical Report MSR-TR-2005-52, Microsoft Research (2005)Google Scholar
  16. [RRS03]
    Rosenzweig, D., Runje, D., Slani, N.: Privacy, abstract encryption and protocols: an ASM model – Part I. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 372–390. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. [AsmL]
  18. [Spec#]
    Rosenzweig, D., Runje, D., Slani, N.: Privacy, abstract encryption and protocols: an ASM model – Part I. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 372–390. Springer, Heidelberg (2003)Google Scholar
  19. [SpecExp]

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Dean Rosenzweig
    • 1
    • 2
  • Davor Runje
    • 2
  • Wolfram Schulte
    • 1
  1. 1.Microsoft ResearchUSA
  2. 2.University of ZagrebCroatia

Personalised recommendations