Automated Analysis of Infinite Scenarios

  • Mikael Buchholtz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)


The security of a network protocol crucially relies on the scenario in which the protocol is deployed. This paper describes syntactic constructs for modelling network scenarios and presents an automated analysis tool, which can guarantee that security properties hold in all of the (infinitely many) instances of a scenario. The tool is based on control flow analysis of the process calculus LySa and is applied to the Bauer, Berson, and Feiertag protocol where is reveals a previously undocumented problem, which occurs in some scenarios but not in other.


Automate Analysis Security Protocol Security Property Parallel Composition Static Authentication 
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.
    Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS security protocol analysis tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349–353. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Bauer, R.K., Berson, T.A., Feiertag, R.J.: A key distribution protocol using event markers. ACM Transactions on Computer Systems 1(3), 249–255 (1983)CrossRefGoogle Scholar
  3. 3.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001, pp. 82–96. IEEE, Los Alamitos (2001)Google Scholar
  4. 4.
    Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Automatic validation of protocol narration. In: CSFW 2003, pp. 126–140. IEEE, Los Alamitos (2003)Google Scholar
  5. 5.
    Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Static validation of security protocols. JSC (2004) (to appear), Preliminary version at
  6. 6.
    Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. Springer, Heidelberg (2003)Google Scholar
  7. 7.
    Buchholtz, M.: Automated analysis of security in networking systems. Ph. D. thesis proposal (December 2004), Available from
  8. 8.
    Buchholtz, M.: Implementing control flow analysis for security protocols. DEGAS Report WP6-IMM-I00-Pub-003, Draft (2003)Google Scholar
  9. 9.
    Buchholtz, M., Nielson, F., Nielson, H.R.: A calculus for control flow analysis of security protocols. IJIS 2(3-4), 145–167 (2004)CrossRefGoogle Scholar
  10. 10.
    Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 140–154. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Comon-Lundh, H., Cortier, V.: Security properties: Two agents are sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 99–113. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Denker, G., Millen, J., Rueß, H.: The CAPSL integrated protocol environment. Technical Report SRI-CLS-2000-02, SRI International (2000)Google Scholar
  13. 13.
    Durante, A., Focardi, R., Gorrieri, R.: A compiler for analyzing cryptographic protocols using noninterference. TSEM 9(4), 488–528 (2000)CrossRefGoogle Scholar
  14. 14.
    Gordon, A.D., Jeffrey, A.: Authenticity by Typing for Security Protocols. In: CSFW 2001, pp. 145–159. IEEE, Los Alamitos (2001)Google Scholar
  15. 15.
    Information technology - security techniques - key management - part 2. mechanisms using symmetric techniques ISO/IEC 11770-2. International Standard (1996)Google Scholar
  16. 16.
    Lowe, G.: Casper: A compiler for the analysis of security protocols. JCS 6(1), 53–84 (1998)Google Scholar
  17. 17.
    Nielson, F., Nielson, H.R., Hansen, R.R.: Validating firewalls using Flow Logics. TCS 283(2), 381–418 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    Nielson, F., Nielson, H.R., Seidl, H.: Cryptographic analysis in cubic time. In: TOSCA 2001. ENTCS, vol. 62. Elsevier, Amsterdam (2001)Google Scholar
  19. 19.
    Nielson, F., Nielson, H.R., Seidl, H.: A succinct solver for ALFP. NJC 9, 335–372 (2002)zbMATHMathSciNetGoogle Scholar
  20. 20.
    Riis Nielson, H., Nielson, F.: Flow logic: a multi-paradigmatic approach to static analysis. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 223–244. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Stoller, S.D.: A bound on attacks on authentication protocols. In: Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science (TCS 2002), pp. 588–600. Kluwer, Dordrecht (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Mikael Buchholtz
    • 1
  1. 1.Informatics and Mathematical ModellingTechnical University of DenmarkKgs. Lyngby

Personalised recommendations