LySa

LySa - a process calculus
LySa is a process calculus for security protocols developed in collaboration between University of Pisa and Technical University of Denmark during the European Union IST/FET project DEGAS.

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].
For-LySa Extractor. An automatic tool for extracting LySa processes from UML models of security protocols as described in [BMPS04].
Choreographer. An intergrated 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].

Last updated October 6, 2006 by Elsebeth Strøm

LySa - a process calculus LySa is a process calculus for security protocols developed in collaboration between University of Pisa and Technical University of Denmark during the European Union IST/FET project DEGAS.
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]. For-LySa Extractor. An automatic tool for extracting LySa processes from UML models of security protocols as described in [BMPS04]. Choreographer. An intergrated 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].

Last updated October 6, 2006 by Elsebeth Strøm