A BRUTUS Logic for a Spi-Calculus Dialect

S. Gnesi, D. Latella, Gabriele Lenzini

Research output: Book/ReportReportOther research output

8 Downloads (Pure)

Abstract

In the field of process algebras, the spi-calculus, a modified version of the π-calculus with encryption primitives, is indicated as an expressive specification language for cryptographic protocols. In spi-calculus basic security properties, such as secrecy and integrity can be formalized as may-testing equivalences which do not seem easily extendible to express other kinds of interesting properties such as, for example, anonymity. When, as a language for properties specification, temporal logics are used a more expressive power can be reached making possible to represent a wider class of properties. Recently, within the BRUTUS model checker, a first order temporal logic has been defined, making possible to express both basic and advanced properties, such as different kinds of authenticity and anonymity. In this work we define a spi-calculus dialect on which the BRUTUS logic can be interpreted with a double in our opinion, potential advantage: to provide the spi-calculus like languages with a temporal logics as a flexible medium of security properties expression, and to enlarge the BRUTUS model checker with a widely used specification language for cryptographic protocols.
Original languageUndefined
Publication statusPublished - Dec 2000
Externally publishedYes

Publication series

Name
No.TR-B4

Keywords

  • IR-64070
  • EWI-1005

Cite this

Gnesi, S., Latella, D., & Lenzini, G. (2000). A BRUTUS Logic for a Spi-Calculus Dialect.
Gnesi, S. ; Latella, D. ; Lenzini, Gabriele. / A BRUTUS Logic for a Spi-Calculus Dialect. 2000.
@book{1991f0e607ba408abe59349a2942b099,
title = "A BRUTUS Logic for a Spi-Calculus Dialect",
abstract = "In the field of process algebras, the spi-calculus, a modified version of the π-calculus with encryption primitives, is indicated as an expressive specification language for cryptographic protocols. In spi-calculus basic security properties, such as secrecy and integrity can be formalized as may-testing equivalences which do not seem easily extendible to express other kinds of interesting properties such as, for example, anonymity. When, as a language for properties specification, temporal logics are used a more expressive power can be reached making possible to represent a wider class of properties. Recently, within the BRUTUS model checker, a first order temporal logic has been defined, making possible to express both basic and advanced properties, such as different kinds of authenticity and anonymity. In this work we define a spi-calculus dialect on which the BRUTUS logic can be interpreted with a double in our opinion, potential advantage: to provide the spi-calculus like languages with a temporal logics as a flexible medium of security properties expression, and to enlarge the BRUTUS model checker with a widely used specification language for cryptographic protocols.",
keywords = "IR-64070, EWI-1005",
author = "S. Gnesi and D. Latella and Gabriele Lenzini",
note = "Imported from DIES",
year = "2000",
month = "12",
language = "Undefined",
number = "TR-B4",

}

Gnesi, S, Latella, D & Lenzini, G 2000, A BRUTUS Logic for a Spi-Calculus Dialect.

A BRUTUS Logic for a Spi-Calculus Dialect. / Gnesi, S.; Latella, D.; Lenzini, Gabriele.

2000.

Research output: Book/ReportReportOther research output

TY - BOOK

T1 - A BRUTUS Logic for a Spi-Calculus Dialect

AU - Gnesi, S.

AU - Latella, D.

AU - Lenzini, Gabriele

N1 - Imported from DIES

PY - 2000/12

Y1 - 2000/12

N2 - In the field of process algebras, the spi-calculus, a modified version of the π-calculus with encryption primitives, is indicated as an expressive specification language for cryptographic protocols. In spi-calculus basic security properties, such as secrecy and integrity can be formalized as may-testing equivalences which do not seem easily extendible to express other kinds of interesting properties such as, for example, anonymity. When, as a language for properties specification, temporal logics are used a more expressive power can be reached making possible to represent a wider class of properties. Recently, within the BRUTUS model checker, a first order temporal logic has been defined, making possible to express both basic and advanced properties, such as different kinds of authenticity and anonymity. In this work we define a spi-calculus dialect on which the BRUTUS logic can be interpreted with a double in our opinion, potential advantage: to provide the spi-calculus like languages with a temporal logics as a flexible medium of security properties expression, and to enlarge the BRUTUS model checker with a widely used specification language for cryptographic protocols.

AB - In the field of process algebras, the spi-calculus, a modified version of the π-calculus with encryption primitives, is indicated as an expressive specification language for cryptographic protocols. In spi-calculus basic security properties, such as secrecy and integrity can be formalized as may-testing equivalences which do not seem easily extendible to express other kinds of interesting properties such as, for example, anonymity. When, as a language for properties specification, temporal logics are used a more expressive power can be reached making possible to represent a wider class of properties. Recently, within the BRUTUS model checker, a first order temporal logic has been defined, making possible to express both basic and advanced properties, such as different kinds of authenticity and anonymity. In this work we define a spi-calculus dialect on which the BRUTUS logic can be interpreted with a double in our opinion, potential advantage: to provide the spi-calculus like languages with a temporal logics as a flexible medium of security properties expression, and to enlarge the BRUTUS model checker with a widely used specification language for cryptographic protocols.

KW - IR-64070

KW - EWI-1005

M3 - Report

BT - A BRUTUS Logic for a Spi-Calculus Dialect

ER -

Gnesi S, Latella D, Lenzini G. A BRUTUS Logic for a Spi-Calculus Dialect. 2000.