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.
Non-repudiation Analysis with LYSA
CORTESI, Agostino
2009-01-01
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 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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
sec2009.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Accesso chiuso-personale
Dimensione
230.48 kB
Formato
Adobe PDF
|
230.48 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
