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.