Book chapter
Alice and Bob: Reconciling Formal Models and Implementation
In
Lecture Notes in Computer Science
—
2015, pp. 66-85
Abstract
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2015 |
| Pages: | 66-85 |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | Essays Dedicated To Pierpaolo Degano on the Occasion of His 65th Birthday |
| ISBN: | 3319255266 , 3319255274 , 9783319255262 and 9783319255279 |
| ISSN: | 03029743 and 16113349 |
| Types: | Book chapter |
| DOI: | 10.1007/978-3-319-25527-9_7 |
| ORCIDs: | Mödersheim, Sebastian Alexander |
