Non-repudiation analysis with LYSA with annotations

M. Brusò, A. Cortesi

Research output: Contribution to journalArticleAcademicpeer-review


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 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. Keywords: Static analysis; Control flow analysis; Security; Process calculus.
Original languageEnglish
Pages (from-to)352-377
JournalComputer Languages, Systems and Structures
Issue number4
Publication statusPublished - 2010


Dive into the research topics of 'Non-repudiation analysis with LYSA with annotations'. Together they form a unique fingerprint.

Cite this