Customizing Protocol Specifications for Detecting Resource Exhaustion and Guessing Attacks

  • Bogdan Groza
  • Marius Minea
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


Model checkers for security protocols often focus on basic properties, such as confidentiality or authentication, using a standard model of the Dolev-Yao intruder. In this paper, we explore how to model other attacks, notably guessing of secrets and denial of service by resource exhaustion, using the AVANTSSAR platform with its modelling language ASLan. We do this by adding custom intruder deduction rules and augmenting protocol transitions with constructs that keep track of these attacks. We compare several modelling variants and find that writing deductions in ASLan as Horn clauses rather than transitions using rewriting rules is crucial for verification performance. Providing automated tool support for these attacks is important since they are often neglected by protocol designers and open up other attack possibilities.


Model Checker Transition Rule Security Protocol Horn Clause Decryption Oracle 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 398–412. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. International Journal of Information Security 7(1), 3–32 (2008)CrossRefzbMATHGoogle Scholar
  3. 3.
    AVANTSSAR: Deliverable 2.3 (update): ASLan++ specification and tutorial (2011),
  4. 4.
    Basin, D.A., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. Internat. J. of Information Security 4(3), 181–208 (2005)CrossRefGoogle Scholar
  5. 5.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 82–96 (2001)Google Scholar
  6. 6.
    Corin, R., Doumen, J.M., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. In: Proc. 2nd Int’l. Workshop on Security Issues with Petri Nets and other Computational Models (WISP), pp. 47–63 (2004)Google Scholar
  7. 7.
    Corin, R., Malladi, S., Alves-Foss, J., Etalle, S.: Guess what? Here is a new tool that finds some new guessing attacks. In: Proc. Workshop on Issues in the Theory of Security, pp. 62–71 (2003)Google Scholar
  8. 8.
    Diffie, W., van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Designs, Codes and Cryptography 2(2), 107–125 (1992)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Ding, Y., Horster, P.: Undetectable on-line password guessing attacks. Operating Systems Review 29(4), 77–86 (1995)CrossRefGoogle Scholar
  10. 10.
    Groza, B., Minea, M.: A formal approach for automated reasoning about off-line and undetectable on-line guessing (short paper). In: Sion, R. (ed.) FC 2010. LNCS, vol. 6052, pp. 391–399. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    Groza, B., Minea, M.: Formal modelling and automatic detection of resource exhaustion attacks. In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, ASIACCS (2011)Google Scholar
  12. 12.
    Hankes Drielsma, P., Mödersheim, S., Viganò, L.: A formalization of off-line guessing for security protocol analysis. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 363–379. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Lowe, G.: Some new attacks upon security protocols. In: Proc. of the 9th IEEE Computer Security Foundations Workshop, pp. 162–169 (1996)Google Scholar
  14. 14.
    Lowe, G.: Analysing protocols subject to guessing attacks. Journal of Computer Security 12(1), 83–98 (2004)CrossRefGoogle Scholar
  15. 15.
    Matsuura, K., Imai, H.: Modification of internet key exchange resistant against denial-of-service. In: Pre-Proceedings of Internet Workshop, pp. 167–174 (2000)Google Scholar
  16. 16.
    Meadows, C.: A cost-based framework for analysis of denial of service networks. Journal of Computer Security 9(1/2), 143–164 (2001)CrossRefGoogle Scholar
  17. 17.
    Ramachandran, V.: Analyzing DoS-resistance of protocols using a cost-based framework. Tech. Rep. DCS/TR-1239, Yale University (2002)Google Scholar
  18. 18.
    Smith, J., González Nieto, J.M., Boyd, C.: Modelling denial of service attacks on JFK with Meadows’s cost-based framework. In: Proc. of the 4th Australasian Information Security Workshop, pp. 125–134 (2006)Google Scholar
  19. 19.
    Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Zorn, G.: Microsoft PPP CHAP extensions, version 2 (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Bogdan Groza
    • 1
  • Marius Minea
    • 1
  1. 1.Politehnica University of Timişoara and Institute e-Austria TimişoaraRomania

Personalised recommendations