Alice and Bob: Reconciling Formal Models and Implementation

Omar Almousa, Sebastian Alexander Mödersheim, Luca Viganò

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

387 Downloads (Pure)


This paper defines the “ultimate” formal semantics for Alice and Bob notation, i.e., what actions the honest agents have to perform, in the presence of an arbitrary set of cryptographic operators and their algebraic theory. Despite its generality, this semantics is mathematically simpler than any previous attempt. For practical applicability, we introduce the language SPS and an automatic translation to robust real-world implementations and corresponding formal models, and we prove this translation correct with respect to the semantics.
Original languageEnglish
Title of host publicationProgramming Languages with Applications to Biology and Security : Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday
Publication date2015
ISBN (Print)978-3-319-25526-2
ISBN (Electronic)978-3-319-25527-9
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Alice and Bob: Reconciling Formal Models and Implementation'. Together they form a unique fingerprint.

Cite this