Alice and Bob Meet Equational Theories

David Basin; Michel Keller; Saša Radomirović; Ralf Sasse

doi:10.1007/978-3-319-23165-5_7

Alice and Bob Meet Equational Theories

David Basin
, Michel Keller
, Saša Radomirović
, Ralf Sasse (Lead / Corresponding author)

Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

10 Citations (Scopus)

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	https://doi.org/10.1007/978-3-319-23165-5_7
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	http://meseguer-fest.ifi.uio.no/index.php?n=Main.Home (Link to Symposium website)

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-23165-5_7

Cite this

Basin, D., Keller, M., Radomirović, S., & Sasse, R. (2015). Alice and Bob Meet Equational Theories. In N. Martí-Oliet, P. Csaba Ölveczky, & C. Talcott (Eds.), Logic, Rewriting and Concurrency : Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday (pp. 160-180). (Lecture Notes in Computer Science ; Vol. 9200). Springer International Publishing. https://doi.org/10.1007/978-3-319-23165-5_7

Basin, David ; Keller, Michel ; Radomirović, Saša et al. / Alice and Bob Meet Equational Theories. Logic, Rewriting and Concurrency : Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday. editor / Narciso Martí-Oliet ; Peter Csaba Ölveczky ; Carolyn Talcott . Switzerland : Springer International Publishing, 2015. pp. 160-180 (Lecture Notes in Computer Science ).

@inproceedings{55dbfd74ee4e4cc1ba6f26add1d3a41a,

title = "Alice and Bob Meet Equational Theories",

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.",

author = "David Basin and Michel Keller and Sa{\v s}a Radomirovi{\'c} and Ralf Sasse",

note = "No funding info; Logic, Rewriting, and Concurrency : Festschrift Symposium in Honor of Jos{\'e} Meseguer ; Conference date: 23-09-2015 Through 25-09-2015",

year = "2015",

doi = "10.1007/978-3-319-23165-5\_7",

language = "English",

isbn = "9783319231648",

series = "Lecture Notes in Computer Science ",

publisher = "Springer International Publishing",

pages = "160--180",

editor = "Mart{\'i}-Oliet, \{Narciso \} and \{Csaba {\"O}lveczky\}, \{Peter \} and \{Talcott \}, \{Carolyn \}",

booktitle = "Logic, Rewriting and Concurrency",

address = "Switzerland",

url = "http://meseguer-fest.ifi.uio.no/index.php?n=Main.Home",

}

Basin, D, Keller, M, Radomirović, S & Sasse, R 2015, Alice and Bob Meet Equational Theories. in N Martí-Oliet, P Csaba Ölveczky & C Talcott (eds), Logic, Rewriting and Concurrency : Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday. Lecture Notes in Computer Science , vol. 9200, Springer International Publishing, Switzerland, pp. 160-180, Logic, Rewriting, and Concurrency, Urbana, Illinois, United States, 23/09/15. https://doi.org/10.1007/978-3-319-23165-5_7

Alice and Bob Meet Equational Theories. / Basin, David; Keller, Michel; Radomirović, Saša et al.
Logic, Rewriting and Concurrency : Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday. ed. / Narciso Martí-Oliet; Peter Csaba Ölveczky; Carolyn Talcott . Switzerland: Springer International Publishing, 2015. p. 160-180 (Lecture Notes in Computer Science ; Vol. 9200).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Alice and Bob Meet Equational Theories

AU - Basin, David

AU - Keller, Michel

AU - Radomirović, Saša

AU - Sasse, Ralf

N1 - No funding info

PY - 2015

Y1 - 2015

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

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

UR - https://www.scopus.com/pages/publications/84960404863

U2 - 10.1007/978-3-319-23165-5_7

DO - 10.1007/978-3-319-23165-5_7

M3 - Conference contribution

AN - SCOPUS:84960404863

SN - 9783319231648

T3 - Lecture Notes in Computer Science

SP - 160

EP - 180

BT - Logic, Rewriting and Concurrency

A2 - Martí-Oliet, Narciso

A2 - Csaba Ölveczky, Peter

A2 - Talcott , Carolyn

PB - Springer International Publishing

CY - Switzerland

T2 - Logic, Rewriting, and Concurrency

Y2 - 23 September 2015 through 25 September 2015

ER -

Basin D, Keller M, Radomirović S, Sasse R. Alice and Bob Meet Equational Theories. In Martí-Oliet N, Csaba Ölveczky P, Talcott C, editors, Logic, Rewriting and Concurrency : Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday. Switzerland: Springer International Publishing. 2015. p. 160-180. (Lecture Notes in Computer Science ). Epub 2015 Aug 27. doi: 10.1007/978-3-319-23165-5_7

Alice and Bob Meet Equational Theories

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this