Synthesizing Secure Protocols

Veronique Cortier, Bogdan Warinschi, Eugen Zalinescu

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

11 Citations (Scopus)


We propose a general transformation that maps a cryptographic protocol that is secure in an extremely weak sense (essentially in a model where no adversary is present) into a protocol that is secure against a fully active adversary which interacts with an unbounded number of protocol sessions, and has absolute control over the network. The transformation works for arbitrary protocols with any number of participants, written with usual cryptographic primitives. Our transformation provably preserves a large class of security properties that contains secrecy and authenticity. An important byproduct contribution of this paper is a modular protocol development paradigm where designers focus their effort on an extremely simple execution setting – security in more complex settings being ensured by our generic transformation. Conceptually, the transformation is very simple, and has a clean, well motivated design. Each message is tied to the session for which it is intended via digital signatures and on-the-fly generated session identifiers, and prevents replay attacks by encrypting the messages under the recipient’s public key.
Translated title of the contributionSynthesizing Secure Protocols
Original languageEnglish
Title of host publicationEuropean Symposium On Research In Computer Security - ESORICS 2007
PublisherSpringer Berlin Heidelberg
Publication statusPublished - 2007

Bibliographical note

Other page information: 406-421
Conference Proceedings/Title of Journal: 12th European Symposium On Research In Computer Security -- ESORICS'07
Other identifier: 2000757

Fingerprint Dive into the research topics of 'Synthesizing Secure Protocols'. Together they form a unique fingerprint.

Cite this