Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Latella D., Lenzini G. A BRUTUS logic for a spi-calculus dialect. Internal note IEI-B4-27, 2000.
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 temporallogic 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 fiexible medium of security properties expression, and to enlarge the BRUTUS model checker with a widely used specification language for cryptographic protocols.
Subject Security protocols
Model checking
D.2.4 Software/Program Verification
F.3.1 Specifying and Verifying and Reasoning about Programs

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional