An Abstraction and Refinement Framework for Verifying Security Protocols Based on Logic Programming

  • MengJun Li
  • Ti Zhou
  • ZhouJun Li
  • HuoWang Chen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4846)


Using depth(k) abstract domain, we present an abstraction and refinement framework for verifying security protocols based on logic programming. The solved-form fixpoint of the logic program model is abstracted by depth(k) abstract domain, which guarantees termination of the verification algorithm; If the result of the verification algorithm with the abstract solved-form fixpoint shows there exists counterexamples, but the result of the verification algorithm with the logic rules in abstract solved-form fixpoint which are not abstracted shows there exists no counterexamples, then the abstracted solved-form fixpoint is refined by increasing the value of term depth bound k. With this framework, all of the verification, constructing counterexamples and refinement can be implemented in a mechanized way.


abstraction and refinement security protocol 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE Press, Cape Breton, Nova Scotia (2001)CrossRefGoogle Scholar
  2. 2.
    Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 242–259. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. In: 29th ACM Symposium on Principles of Programming Languages, pp. 33–44. ACM Press, Portland (2002)CrossRefGoogle Scholar
  4. 4.
    Allamigeon, X., Blanchet, B.: Reconstruction of Attacks against Cryptography Protocols. In: 18th IEEE Computer Security Foundations Workshop, pp. 140–154. IEEE Press, Aix-en-Provence (2005)CrossRefGoogle Scholar
  5. 5.
    Blanchet, B., Podelski, A.: Verification of cryptographic protocols: tagging enforces termination. Theor. Comput. Sci. 333(1-2), 67–90 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Gori, R., Lastres, E., Moreno, R., Spot, F.: Approximation of the Well-Founded Semantics for Normal Logic Programs using Abstract Interpretation. In: Freire-Nistal, J.L., Falaschi, M., Villares-Ferro, M. (eds.) Proceedings of the APPIA-GULP-PRODE 1998 Conference, A Coruña, Spain, pp. 433–441 (1998)Google Scholar
  7. 7.
    Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Heintze, N., Clarke, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols, Trento (1999)Google Scholar
  8. 8.
    Cousot, P., Cousot, R.: Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programing Languages, pp. 238–252. ACM Press, Los Angeles (1977)CrossRefGoogle Scholar
  9. 9.
    Bozga, L., Lakhnech, Y., Périn, M.: Pattern-Based Abstraction for Verifying Secrecy in Protocols. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 299–314. Springer, Heidelberg (2003)Google Scholar
  10. 10.
    Bozga, L., Lakhnech, Y., Périn, M.: HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)Google Scholar
  11. 11.
    Oehl, F., Cécé, G., Kouchnarenko, O., Sinclair, D.: Automatic Approximation for the Verification of Cryptographic Protocols. In: Pezzé, M. (ed.) ETAPS 2003 and FASE 2003. LNCS, vol. 2621, pp. 34–48. Springer, Heidelberg (2003)Google Scholar
  12. 12.
    Backes, M., Maffei, M., Cortesi, A.: Causality-based Abstraction of Multiplicity in Security Protocols. In: 20th IEEE Computer Security Foundation Symposium, pp. 355–369. IEEE Press, Venice (2007)CrossRefGoogle Scholar
  13. 13.
    Li, M., Li, Z., Chen, H.W.: Spvt: An efficient verification tool for security protocol. Chinese Journal of Software 17(4), 898–906 (2006)zbMATHCrossRefGoogle Scholar
  14. 14.
    Li, M., Li, Z., Chen, H.W.: Security protocol’s extended horn logic model and its verification method. Chinese Journal of Computers 29(9), 1667–1678 (2006)Google Scholar
  15. 15.
    Zhou, T., Li, M., Li, Z., Chen, H.W.: Automatically Constructing Counter- examples of Security Protocols based on the extended Horn Logic Model. Chinese Journal of computer research and development 44(9), 1518–1531 (2007)CrossRefGoogle Scholar
  16. 16.
    Clark, J., Joacob, J.: A survey on authentification protocol (1997),

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • MengJun Li
    • 1
  • Ti Zhou
    • 1
  • ZhouJun Li
    • 2
  • HuoWang Chen
    • 1
  1. 1.School of Computer Science, National University of Defense Technology, ChangSha, 410073China
  2. 2.School of Computer Science & Engineering, Beihang University, BeiJing 100083China

Personalised recommendations