Back to University of Twente portal
A BRUTUS Logic for a Spi-Calculus Dialect
Gnesi, S. and Latella, D. and Lenzini, G. (2000) A BRUTUS Logic for a Spi-Calculus Dialect. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 254Kb |
| 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. |
| Item Type: | Report |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Link to this item: | http://purl.utwente.nl/publications/64070 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page