Soundness of Formal Encryption in the Presence of Active Adversaries

D Micciancio, B Warinschi

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

146 Citations (Scopus)

Abstract

We present a general method to prove security properties of cryptographic protocols against active adversaries, when the messages exchanges by the honest parties are arbitrary expressions built using encryption and concatenation operations. The method allows to express security properties and carry out proofs using a simple logic based language, where messages are represented by syntactic expressions, and does not require dealing with probability distributions or asymptotic notation explicitly. Still, we show that the method is sound, meaning that logic statements can be naturally interpreted in the computational setting in such a way that if the statement holds true for any abstract (symbolic) execution of the protocol in the presence of a Dolev-Yao adversary, then its computational intepretation is also correct in the standard computational model where the adversary is an arbitrary probabilistic polynomial time program. This is the first result showing how to translate security proofs from the logic setting to the standard computational setting for the case of poweful active adversaries that have total control of the communication network.
Translated title of the contributionSoundness of Formal Encryption in the Presence of Active Adversaries
Original languageEnglish
Title of host publicationTheory of Cryptography Conference - TCC 2004
PublisherSpringer Berlin Heidelberg
Pages133 - 151
Number of pages19
Volume2656
DOIs
Publication statusPublished - 2004

Bibliographical note

ISBN: 9783540210009
Publisher: Springer
Name and Venue of Conference: Theory of Cryptography: First Theory of Cryptography Conference, TCC 2004, Cambridge, MA, USA, 19-21 February
Conference Organiser: International Association for Cryptographic Research

Fingerprint

Dive into the research topics of 'Soundness of Formal Encryption in the Presence of Active Adversaries'. Together they form a unique fingerprint.

Cite this