(De)Compositions of Cryptographic Schemes and their Applications to Protocols
The main result of this paper is that the Dolev-Yao model is a safe abstraction of the computational model for security protocols including those that combine asymmetric and symmetric encryption, signature and hashing. Moreover, message forwarding and private key transmission are allowed. To our knowledge this is the first result that deals with hash functions and the combination of these cryptographic primitives. A key step towards this result is a general definition of correction of cryptographic primitives, that unifies well known correctness criteria such as IND-CPA, IND-CCA, unforgeability etc.... and a theorem that allows to reduce the correctness of a composition of two cryptographic schemes to the correctness of each one.
Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation
Recently, it has been proved that computational security can be automatically verified using the Dolev-Yao abstraction. We extend these results by adding a widely used component for cryptographic protocols: Diffie-Hellman exponentiation. Thus our main result is: if the Decisional Diffie-Hellman assumption is verified and the cryptographic primitives used to implement the protocol are secure, then safety in the symbolic world implies safety in the computational world. Therefore, it is possible to prove automatically safety in the computational world.
Probabilistic Opacity for a Passive Adversary and its Application to Chaum's Voting Scheme
A predicate is opaque for a given system, if an adversary will never be able to establish truth or falsehood of the predicate for any observed computation. This notion has been essentially introduced and studied in the context of transition systems whether describing the semantics of programs, security protocols or other systems. In this paper, we are interested in studying opacity in the probabilistic computational world. Indeed, in other settings, as in the Dolev-Yao model for instance, even if an adversary is $99\%$ sure of the truth of the predicate, it remains opaque as the adversary cannot conclude for sure. In this paper, we introduce a computational version of opacity in the case of passive adversaries called cryptographic opacity. Our main result is a composition theorem: if a system is secure in an abstract formalism and the cryptographic primitives used to implement it are secure, then this system is secure in a computational formalism. Security of the abstract system is the usual opacity and security of the cryptographic primitives is IND-CPA security. To illustrate our result, we give two applications: a short and elegant proof of the classical Abadi-Rogaway result and the first computational proof of Chaum's visual electronic voting scheme.