Alice and Bob meet equational theories

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

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

3 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 languageEnglish
Title of host publicationLogic, Rewriting and Concurrency
EditorsPeter Csaba Ölveczky, Carolyn Talcott, Narciso Martí-Oliet
PublisherSpringer
Pages160-180
Number of pages21
ISBN (Electronic)9783319231655
ISBN (Print)9783319231648
DOIs
Publication statusPublished - 2015
EventConference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday - Champaign, United States
Duration: 23 Sep 201525 Sep 2015

Publication series

NameLecture Notes in Computer Science
Volume9200
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceConference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday
CountryUnited States
CityChampaign
Period23/09/1525/09/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Alice and Bob meet equational theories'. Together they form a unique fingerprint.

Cite this