A "Brutus" model checking of a spi-calculus dialect (Extended Abstract)

S. Gnesi; D. Latella; G. Lenzini

A "Brutus" model checking of a spi-calculus dialect (Extended Abstract)

S. Gnesi, D. Latella, G. Lenzini

Research output: Contribution to conference › Paper › Academic

12 Downloads (Pure)

Abstract

This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.

Original language	English
Number of pages	13
Publication status	Published - 2000
Externally published	Yes
Event	CAV Workshop on Formal Methods and Computer Security, FMCS 2000 - Chicago, United States Duration: 1 Jul 2000 → 1 Jul 2000

Other

Other	CAV Workshop on Formal Methods and Computer Security, FMCS 2000
Abbreviated title	FMCS
Country	United States
City	Chicago
Period	1/07/00 → 1/07/00

Access to Document

Gnesi00brutus
open
Final published version, 209 KB

Fingerprint Dive into the research topics of 'A "Brutus" model checking of a spi-calculus dialect (Extended Abstract)'. Together they form a unique fingerprint.

Cite this

@conference{72ec41e6e9db45b0985dc34664d3245c,

title = "A {"}Brutus{"} model checking of a spi-calculus dialect (Extended Abstract)",

abstract = "This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.",

author = "S. Gnesi and D. Latella and G. Lenzini",

year = "2000",

language = "English",

note = "CAV Workshop on Formal Methods and Computer Security, FMCS 2000, FMCS ; Conference date: 01-07-2000 Through 01-07-2000",

}

TY - CONF

T1 - A "Brutus" model checking of a spi-calculus dialect (Extended Abstract)

AU - Gnesi, S.

AU - Latella, D.

AU - Lenzini, G.

PY - 2000

Y1 - 2000

N2 - This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.

AB - This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.

M3 - Paper

T2 - CAV Workshop on Formal Methods and Computer Security, FMCS 2000

Y2 - 1 July 2000 through 1 July 2000

ER -