Abstract
This work introduces a formal analysis of the non-repudiation property for security protocols. Protocols are modelled in the process calculus LySa, using an extended syntax with annotations. Non-repudiation is verified using a Control Flow Analysis, following the same approach introduced by M. Buchholtz and H. Gao for authentication and freshness analyses.
The result is an analysis that can statically check the protocols to predict if they are secure during their execution and which can be fully automated.
Work partially supported by PRIN 07 MUR Project 200793N42R SOFT.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Bella, G., Paulson, L.C.: Mechanical proofs about a non-repudiation protocol. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 91–104. Springer, Heidelberg (2001)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Journal of Computer Security, 347–390 (2005)
Braghin, C., Cortesi, A., Focardi, R.: Information flow security in boundary ambients. Inf. Comput. 206(2-4), 460–489 (2008)
Brusò, M., Cortesi, A.: Non-repudiation analysis using LYSA with annotations, CS Tech. Report, Univ. Ca Foscari. Tech. rep. (2008), http://www.unive.it/nqcontent.cfm?a_id=5144#rapporti08
Buchholtz, M., Lyngby, K.: Automated analysis of security in networking systems. Ph. d. thesis proposal, Tech. rep. (2004), http://www.imm.dtu.dk/~mib/thesis
Cederquist, Corin, Dashti: On the quest for impartiality: Design and analysis of a fair non-repudiation protocol. In: ICIS 2005. LNCS. Springer, Heidelberg (2005)
Dolev, D., Yao, A.C.: On the security of public key protocols. Tech. rep., Stanford, CA (1981)
Gao, H.: Analysis Of Protocols By Annotations. Ph. D. Thesis, Informatics and Mathematical Modelling, Technical University of Denmark (2008)
Gollmann, D.: Computer security. John Wiley & Sons, Inc., New York (1999)
Kremer, S., Raskin, J.F.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 551–565 (2001)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)
Schneider, S.: Formal analysis of a non-repudiation protocol. In: 11th IEEE Computer Security Foundations Workshop, p. 54 (1998)
Schneider, S., Holloway, R.: Security properties and csp. In: IEEE Symp. Security and Privacy, pp. 174–187. IEEE Computer Society Press, Los Alamitos (1996)
Zhou, J., Gollmann, D.: A fair non-repudiation protocol. IEEE Computer Society Press, Los Alamitos (1996)
Zhou, J., Gollmann, D.: Evidence and non-repudiation. J. Netw. Comput. Appl. 20(3), 267–281 (1997), http://dx.doi.org/10.1006/jnca.1997.0056
Zhou, J., Gollmann, D.: Towards verification of non-repudiation protocols. In: Proceedings of International Refinement Workshop and Formal Methods Pacific. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Brusò, M., Cortesi, A. (2009). Non-repudiation Analysis with LySa . In: Gritzalis, D., Lopez, J. (eds) Emerging Challenges for Security, Privacy and Trust. SEC 2009. IFIP Advances in Information and Communication Technology, vol 297. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01244-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-01244-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01243-3
Online ISBN: 978-3-642-01244-0
eBook Packages: Computer ScienceComputer Science (R0)