Abstract
Cryptographic protocols are the backbone of secure communication over open networks and their correctness is therefore crucial. Tool-supported formal analysis of cryptographic protocol designs increases our confidence that these protocols achieve their intended security guarantees. We propose a method to automatically translate textbook style Alice&Bob protocol specifications into a format amenable to formal verification using existing tools. Our translation supports specification modulo equational theories, which enables the faithful representation of algebraic properties of a large class of cryptographic operators.
Original language | English |
---|---|
Title of host publication | Logic, Rewriting and Concurrency |
Subtitle of host publication | Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday |
Editors | Narciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott |
Place of Publication | Switzerland |
Publisher | Springer International Publishing |
Pages | 160-180 |
Number of pages | 21 |
ISBN (Electronic) | 9783319231655 |
ISBN (Print) | 9783319231648 |
DOIs | |
Publication status | Published - 2015 |
Event | Logic, Rewriting, and Concurrency: Festschrift Symposium in Honor of José Meseguer - University of Illinois at Urbana-Champaign, Department of Computer Science , Urbana, United States Duration: 23 Sept 2015 → 25 Sept 2015 http://meseguer-fest.ifi.uio.no/index.php?n=Main.Home (Link to Symposium website) |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer International Publishing |
Volume | 9200 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | Logic, Rewriting, and Concurrency |
---|---|
Country/Territory | United States |
City | Urbana |
Period | 23/09/15 → 25/09/15 |
Internet address |
|
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science