Towards a mechanization of cryptographic protocol verification

  • Dominique Bolignano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We revisit the approach defined in [2] for the formal verification of cryptographic protocols so as to allow for some mechanization in the verification process. In the original approach verification uses theorem proving. Here we show that for a wide range of practical situations and properties it is possible to perform the verification on a finite and safe abstract model.


Model Check Security Property Formal Verification Proof Obligation Cryptographic Protocol 
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.
    J.-P. Banâtre and D. Le Métayer. Gamma and the chemical reaction model: ten years after. In Coordination programming: mechanisms, models and semantics. World Scientific Publishing, IC Press, 1996.Google Scholar
  2. 2.
    D. Bolignano. Formal verification of cryptographic protocols. In Proceedings of the third ACM Conference on Computer and Communication Security, 1996.Google Scholar
  3. 3.
    D. Bolignano. Towards the Formal Verification of Electronic Commerce Protocols. In Proceedings of the 10 th IEEE Computer Security Foundations Workshop. IEEE, June 1997.Google Scholar
  4. 4.
    Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.Google Scholar
  5. 5.
    Ranee Cleaveland, Punish Iyer, and Daniel Yankelevich. Optimality in abstractions of model checking. In Proceedings of SAS'95. LNCS, 1995.Google Scholar
  6. 6.
    Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In E.-R. Olderog, editor, Proceedings of the IFIP WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), IFIP Transactions, Amsterdam, June 1994. North-Holland/Elsevier.Google Scholar
  7. 7.
    G.Leduc, O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur, and D. Zanetti. Specification and verification of a ttp protocol for the conditional access to services. In Proceedings of the 12th Workshop on the Application of Formal Methods to System Development (Univ Montreal), 1996.Google Scholar
  8. 8.
    S. Graf. Verification of a distributed cache memory by using abstractions. In Workshop on Computer-Aided Verification, CAV'94, Stanford. LNCS 818, Springer Verlag, jun 1994.Google Scholar
  9. 9.
    Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, volume 1051 of Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.Google Scholar
  10. 10.
    C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design Volume 6, Issue 1, 1995.Google Scholar
  11. 11.
    G.Lowe. An attack on the needham-schroeder public-key protocol. In Information Processing Letters, 1995.Google Scholar
  12. 12.
    S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Dominique Bolignano
    • 1
  1. 1.DyadeLe Chesnay CedexFrance

Personalised recommendations