A BRUTUS Logic for a Spi-Calculus Dialect

S. Gnesi, D. Latella, G. Lenzini

Research output: Book/ReportReportOther research output

10 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 languageEnglish
Place of PublicationPisa, Italy
PublisherInstituto Elaborazione dell'Informazione CNR
Publication statusPublished - Dec 2000
Externally publishedYes

Fingerprint

Temporal logic
Specification languages
Network protocols
Algebra
Cryptography
Specifications
Testing

Keywords

  • Security protocols
  • Security properties
  • Spi-calculus
  • Temporal logics
  • Model checking

Cite this

Gnesi, S., Latella, D., & Lenzini, G. (2000). A BRUTUS Logic for a Spi-Calculus Dialect. Pisa, Italy: Instituto Elaborazione dell'Informazione CNR.
Gnesi, S. ; Latella, D. ; Lenzini, G. / A BRUTUS Logic for a Spi-Calculus Dialect. Pisa, Italy : Instituto Elaborazione dell'Informazione CNR, 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 = "Security protocols, Security properties, Spi-calculus, Temporal logics, Model checking",
author = "S. Gnesi and D. Latella and G. Lenzini",
year = "2000",
month = "12",
language = "English",
publisher = "Instituto Elaborazione dell'Informazione CNR",
address = "Italy",

}

Gnesi, S, Latella, D & Lenzini, G 2000, A BRUTUS Logic for a Spi-Calculus Dialect. Instituto Elaborazione dell'Informazione CNR, Pisa, Italy.

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

Pisa, Italy : Instituto Elaborazione dell'Informazione CNR, 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, G.

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 - Security protocols

KW - Security properties

KW - Spi-calculus

KW - Temporal logics

KW - Model checking

M3 - Report

BT - A BRUTUS Logic for a Spi-Calculus Dialect

PB - Instituto Elaborazione dell'Informazione CNR

CY - Pisa, Italy

ER -

Gnesi S, Latella D, Lenzini G. A BRUTUS Logic for a Spi-Calculus Dialect. Pisa, Italy: Instituto Elaborazione dell'Informazione CNR, 2000.