This work introduces a forma lanalysis of the non-repudiatio 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 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 using LySa with annotations

CORTESI, Agostino
2010-01-01

Abstract

This work introduces a forma lanalysis of the non-repudiatio 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 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  
CL_2010.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 412.1 kB
Formato Adobe PDF
412.1 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/22229
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact