Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)*

By Martín Abadi, Phillip Rogaway. Journal of Cryptology, 2000

684 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition

View Paper: https://www.semanticscholar.org/paper/1d13d758485f3ecc43e3711bd46d3e435065eb4d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

Citations in the corpus

A computationally sound mechanized prover for security protocols (2006, background): “Since the seminal paper by Abadi and Rogaway [3], there has been much interest in relating both frameworks (see for example [1] [8] [11] [21] [25] [26] [35] [36]), to show the soundness of the Dolev-Yao model with respect to the computational model, and thus obtain automatic proofs of protocols in t”
Modern Cryptography: Theory and Practice (2003, background): “EC_Multiply(P, 14) = EC_exp(P + P, 7) (in step 2) = [2]P + EC_Multiply([2]P + [2]P, 3) (in step 3) = [2]P + [4]P + EC_Multiply([4]P + [4]P, 1) (in step 3) = [2]P + [4]P + [8]P + EC_Multiply([8]P + [8]P, 0) (in step 3)”
A model for asynchronous reactive systems and its application to secure message transmission (2001, background): “Instead they abstract from most cryp tographic details, and therefore there is no guarantee that a formally proven protocol is actually secure if implemented with a cryptographically secure primitive [1, 26].”
Universally composable signature, certification, and authentication (2004, background): “The works of Abadi and Rogaway [ar00], and Micciancio and Warinschi [mw04] can be regarded as steps in this direction.”
Formal certification of code-based cryptographic proofs (2009, methodology): “Although the s ymbolic model assumes perfect cryptography, soundness results suc h a [1] relate the symbolic model with the computational model, pro vided the cryptographic primitives are secure.”
Opacity generalised to transition systems (2005, background): “A closely related notion was introduced in [2], where it was shown to be sound in the computational model, and its generalisation including the case of equational theories appears in [1].”
Composition and integrity preservation of secure reactive systems (2000, background): “A formal abstraction specifically for symmetric encryption with cryptographic semantics has been described in [2](1), but without considering its use within a system.”