International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Anupam Datta

Affiliation: CMU

Publications

Year
Venue
Title
2015
EPRINT
2013
ASIACRYPT
2008
JOFC
2007
EPRINT
Inductive Proof Method for Computational Secrecy
We investigate inductive methods for proving secrecy properties of network protocols, in a ``computational" setting applying a probabilistic polynomial-time adversary. As in cryptographic studies, our secrecy properties assert that no probabilistic polynomial-time distinguisher can win a suitable game presented by a challenger. Our method for establishing secrecy properties uses inductive proofs of computational trace-based properties, and axioms and inference rules for relating trace-based properties to non-trace-based properties. We illustrate the method, which is formalized in a logical setting that does not require explicit reasoning about computational complexity, probability, or the possible actions of the attacker, by giving a modular proof of computational authentication and secrecy properties of the Kerberos V5 protocol.
2006
TCC
2006
EPRINT
Key Exchange Protocols: Security Definition, Proof Method and Applications
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since key indistinguishability and other previous specifications of secure key exchange suffer from specific compositionality problems, we develop a suitable specification of acceptable key generation. This definition is based on a simple game played by an adversary against a key exchange protocol and a conventional challenger characterizing secure encryption (or other primitives of interest). The method is illustrated using a sample protocol.
2006
EPRINT
On the Relationships Between Notions of Simulation-Based Security
Several compositional forms of simulation-based security have been proposed in the literature, including universal composability, black-box simulatability, and variants thereof. These relations between a protocol and an ideal functionality are similar enough that they can be ordered from strongest to weakest according to the logical form of their definitions. However, determining whether two relations are in fact identical depends on some subtle features that have not been brought out in previous studies. We identify the position of a ``master process" in the distributed system, and some limitations on transparent message forwarding within computational complexity bounds, as two main factors. Using a general computational framework, called Sequential Probabilistic Process Calculus (SPPC), we clarify the relationships between the simulation-based security conditions. We also prove general composition theorems in SPPC. Many of the proofs are carried out based on a small set of equivalence principles involving processes and distributed systems. This gives us results that carry over to a variety of computational models.
2006
EPRINT
Inductive Trace Properties for Computational Security
Protocol authentication properties are generally trace-based, meaning that authentication holds for the protocol if authentication holds for individual traces (runs of the protocol and adversary). Computational secrecy conditions, on the other hand, often are not trace based: the ability to computationally distinguish a system that transmits a secret from one that does not is measured by overall success on the \textit{set} of all traces of each system. This presents a challenge for inductive or compositional methods: induction is a natural way of reasoning about traces of a system, but it does not appear applicable to non-trace properties. We therefore investigate the semantic connection between trace properties that could be established by induction and non-trace-based security requirements. Specifically, we prove that a certain trace property implies computational secrecy and authentication properties, assuming the encryption scheme provides chosen ciphertext security and ciphertext integrity. We also prove a similar theorem for computational secrecy assuming Decisional Diffie-Hellman and a chosen plaintext secure encryption scheme.
2005
TCC
2005
EPRINT
Games and the Impossibility of Realizable Ideal Functionality
A cryptographic primitive or a security mechanism can be specified in a variety of ways, such as a condition involving a game against an attacker, construction of an ideal functionality, or a list of properties that must hold in the face of attack. While game conditions are widely used, an ideal functionality is appealing because a mechanism that is indistinguishable from an ideal functionality is therefore guaranteed secure in any larger system that uses it. We relate ideal functionalities to games by defining the \textit{set} of ideal functionalities associated with a game condition and show that under this definition, which reflects accepted use and known examples, bit commitment, a form of group signatures, and some other cryptographic concepts do not have any realizable ideal functionality.