Non-repudiation analysis with LYSA with annotations

M. Brusò; A. Cortesi

doi:10.1016/j.cl.2010.04.002

Non-repudiation analysis with LYSA with annotations

M. Brusò, A. Cortesi

Mathematics and Computer Science

Research output: Contribution to journal › Article › Academic › peer-review

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. Keywords: Static analysis; Control flow analysis; Security; Process calculus.

Original language	English
Pages (from-to)	352-377
Journal	Computer Languages, Systems and Structures
Volume	36
Issue number	4
DOIs	https://doi.org/10.1016/j.cl.2010.04.002
Publication status	Published - 2010

Access to Document

10.1016/j.cl.2010.04.002

Cite this

@article{e35f8bd74c2c4660b19b5a23d15b25b0,

title = "Non-repudiation analysis with LYSA with annotations",

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. Keywords: Static analysis; Control flow analysis; Security; Process calculus.",

author = "M. Brus{\`o} and A. Cortesi",

year = "2010",

doi = "10.1016/j.cl.2010.04.002",

language = "English",

volume = "36",

pages = "352--377",

journal = "Computer Languages, Systems and Structures",

issn = "1477-8424",

publisher = "Elsevier",

number = "4",

}

TY - JOUR

T1 - Non-repudiation analysis with LYSA with annotations

AU - Brusò, M.

AU - Cortesi, A.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1016/j.cl.2010.04.002

DO - 10.1016/j.cl.2010.04.002

M3 - Article

SN - 1477-8424

VL - 36

SP - 352

EP - 377

JO - Computer Languages, Systems and Structures

JF - Computer Languages, Systems and Structures

IS - 4

ER -

Non-repudiation analysis with LYSA with annotations

Abstract

Access to Document

Fingerprint

Cite this