Alice and Bob Meet Equational Theories

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)


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 languageEnglish
Title of host publicationLogic, Rewriting and Concurrency
Subtitle of host publicationEssays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday
EditorsNarciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott
Place of PublicationSwitzerland
PublisherSpringer International Publishing
Number of pages21
ISBN (Electronic)9783319231655
ISBN (Print)9783319231648
Publication statusPublished - 2015
EventLogic, 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 201525 Sept 2015 (Link to Symposium website)

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceLogic, Rewriting, and Concurrency
Country/TerritoryUnited States
Internet address

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Alice and Bob Meet Equational Theories'. Together they form a unique fingerprint.

Cite this