Symbolic Partial Model Checking for Security Analysis

  • Fabio Martinelli
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2776)


In this paper, we present a symbolic version of the Hennessy-Milner logic for expressing security properties. The models of the logic are CryptoCCS processes with their symbolic semantics. We study the model checking problem and partial model checking techniques for the logic.


Normal Form Model Check Inference System Security Protocol Security Property 
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.
    Basu, S., Ramakrishnan, C.: Compositional analysis for verification of parameterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 315–330. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM (1985)Google Scholar
  3. 3.
    Ingólfsdóttir, A., Lin, H.: A symbolic approach to value-passing processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 427–478. North- Holland, Amsterdam (2001)CrossRefGoogle Scholar
  4. 4.
    Kindred, D., Wing, J.M.: Fast, automatic checking of security protocols. In: Second USENIX Workshop on Electronic Commerce, Oakland, California, pp. 41–52 (1996)Google Scholar
  5. 5.
    Lowe, G.: Breaking and fixing the Needham Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)Google Scholar
  6. 6.
    Marchignoli, D., Martinelli, F.: Automatic verification of cryptographic protocols through compositional analysis techniques. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 148. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Martinelli, F.: Encoding several authentication properties as properties of the intruder’s knowledge. Tech. Rep. IAT-B4-2001-20. Submitted for publicationGoogle Scholar
  8. 8.
    Martinelli, F.: Symbolic semantics and analysis for crypto-ccs with (almost) generic inference systems. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 519–531. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Martinelli, F.: Formal Methods for the Analysis of Open Systems with Applications to Security Properties. PhD thesis, University of Siena (December 1998)Google Scholar
  10. 10.
    Martinelli, F.: Languages for description and analysis of authentication protocols. In: Proceedings of 6th ICTCS, pp. 304–315. World Scientific, Singapore (1998)Google Scholar
  11. 11.
    Martinelli, F.: Analysis of security protocols as open systems. Theoretical Computer Science 290(1), 1057–1106 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Martinelli, F., Petrocchi, M., Vaccarelli, A.: PaMoChSA: A tool for verification of security protocols based on partial model checking. In: Tool Demo at the 1st International School on Formal Methods for the Design of Computer, Communication and Software Systems: Process Algebras (2001)Google Scholar
  13. 13.
    Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  14. 14.
    Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, Reading (2000)Google Scholar
  15. 15.
    Schneider, S.: Verifying authentication protocols with CSP. In: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  16. 16.
    Stirling, C.: Modal and temporal logics for processes. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 149–237. Springer, Heidelberg (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Fabio Martinelli
    • 1
  1. 1.Istituto di Informatica e Telematica – C.N.R.PisaItaly

Personalised recommendations