### Abstract

Original language | English |
---|---|

Place of Publication | Pisa, Italy |

Publisher | Instituto Elaborazione dell'Informazione CNR |

Publication status | Published - Dec 2000 |

Externally published | Yes |

### Fingerprint

### Keywords

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

### Cite this

*A BRUTUS Logic for a Spi-Calculus Dialect*. Pisa, Italy: Instituto Elaborazione dell'Informazione CNR.

}

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

Research output: Book/Report › Report › Other 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 -