Non-repudiation analysis with LYSA

A. Cortesi, M. Brusò

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of the IFIP 24th International Information Security Conference (IFIP SEC'09, Pafos, Cyprus, Greece, May 18-20, 2009)
EditorsD. Gritzalis, J. Lopez
Place of PublicationBoston
PublisherSpringer
Pages318-329
ISBN (Print)978-3-642-01243-3
DOIs
Publication statusPublished - 2009

Publication series

NameIFIP Conference Proceedings
Volume297
ISSN (Print)1571-5736

Fingerprint

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

Cite this