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

S. Gnesi, D. Latella, G. Lenzini

Research output: Contribution to conferencePaperAcademic

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 languageEnglish
Number of pages13
Publication statusPublished - 2000
Externally publishedYes
EventCAV Workshop on Formal Methods and Computer Security, FMCS 2000 - Chicago, United States
Duration: 1 Jul 20001 Jul 2000

Other

OtherCAV Workshop on Formal Methods and Computer Security, FMCS 2000
Abbreviated titleFMCS
CountryUnited States
CityChicago
Period1/07/001/07/00

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