Non-repudiation analysis using LySa with annotations

摘要

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 of Buchholtz and Cao for authentication and freshness analyses.rnThe 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.