LySa - a process calculus

Papers

• [BBDNN03] C. Bodei, M. Buchholtz, P. Degano, H. Riis Nielson, F. Nielson: Automatic Validation of Protocol Narrations. In Proceedings of 16th IEEE Computer Foundations Workshop (CSFW 03). pp 126-140. IEEE Computer Society Press. 2003.
  Requires access to IEEE Xplore to download.
• [BNN04] M. Buchholtz, H. Riis Nielson, F. Nielson: A Calculus for Control Flow Analysis of Security Protocols. International Journal of Information Security. 2(3-4). pp 145-167. 2004.
  Copyright Springer-Verlag. The original publication is available at springerlink.com
• [BBDNN04a] C. Bodei, M. Buchholtz, P. Degano, F. Nielson, H. Riis Nielson: Control Flow Analysis Can Find New Flaws Too, Proceedings of Workshop on Issues in the Theory of Security (WITS 04), 2004.
• [B+04] C. Bodei, M. Buchholtz, P. Degano, M. Curti, C. Priami, F. Nielson, H. Riis Nielson: Performance Evaluation of Security Protocols Specified in LySa, Proceedings of the 2nd Workshop on Quantitative Aspects of Programming Languages (QAPL 04), ENTCS vol. 112, p 167-189, 2005.
• [BMPS04] M. Buchholtz, C. Montangero, L. Perrone, S. Semprini:For-LySa: UML for Authentication Analysis, Global Computing: IST/FET International Workshop, GC 2004, LNCS vol. 3267, p. 93-106, Springer Verlag, 2005
• [BBDNN05] C. Bodei, M. Buchholtz, P. Degano, F. Nielson, H. Riis Nielson: Static Validation of Security Protocols. Journal of Computer Security. To appear 2005.
• [BGHN05] M. Buchholtz, S. Gilmore, J. Hillston, and F. Nielson: Securing statically-verified communications protocols against timing attacks, Proceedings of First International Workshop on Practical Applications of Stochastic Modelling (PASM 04), To appear in ENTCS 2005
• [HSN05] S. M. Hansen, J. Skriver, and H. Riis Nielson: Using static analysis to validate the SAML single sign-on protocol, Proceedings of the 2005 workshop on Issues in the theory of security, p 27 - 40, ACM Press, 2005
• [buchholtz05] M. Buchholtz: Automated Analysis of Infinite Scenarios. Proceedings of Symposium on Trustworthy Global Computing 2005. To appear in LNCS.
• [BGHM05] M. Buchholtz, S. Gilmore, V. Haenel, C. Montangero, End-to-end integrated security and performance analysis on the DEGAS Choreographer platform, Formal Methods 2005. To appear in LNCS.

Software

• LySatool (version 2.02). Updated October 6, 2006.
  An ML implementation of the analysis from [BBDNN05] extented with an analysable meta-level as described in [buchholtz05].
• Choreographer. An integrated tool for security and performance analysis of UML models, which uses the LySatool as an analysis back-end. More information may be found in [BGHM05].