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

^*Corresponding author for this work

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

9 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
Editors	Peter Csaba Ölveczky, Carolyn Talcott, Narciso Martí-Oliet
Publisher	Springer
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	Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday - Champaign, United States Duration: 23 Sept 2015 → 25 Sept 2015

Publication series

Name	Lecture Notes in Computer Science
Volume	9200
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday
Country/Territory	United States
City	Champaign
Period	23/09/15 → 25/09/15

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

Cite this

@inproceedings{33eb463218264cfe86fb9e432eb05457,

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

year = "2015",

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

language = "English",

isbn = "9783319231648",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "160--180",

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

booktitle = "Logic, Rewriting and Concurrency",

address = "United States",

note = "Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday ; Conference date: 23-09-2015 Through 25-09-2015",

}

Basin, D, Keller, M, Radomirović, S & Sasse, R 2015, Alice and Bob meet equational theories. in PC Ölveczky, C Talcott & N Martí-Oliet (eds), Logic, Rewriting and Concurrency. Lecture Notes in Computer Science, vol. 9200, Springer, pp. 160-180, Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday, Champaign, United States, 23/09/15. https://doi.org/10.1007/978-3-319-23165-5_7

TY - GEN

T1 - Alice and Bob meet equational theories

AU - Basin, David

AU - Keller, Michel

AU - Radomirović, Saša

AU - Sasse, Ralf

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 - http://www.scopus.com/inward/record.url?scp=84960404863&partnerID=8YFLogxK

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 - Ölveczky, Peter Csaba

A2 - Talcott, Carolyn

A2 - Martí-Oliet, Narciso

PB - Springer

T2 - Conference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday

Y2 - 23 September 2015 through 25 September 2015

ER -

Alice and Bob meet equational theories

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this