Paper 2005/020

(De)Compositions of Cryptographic Schemes and their Applications to Protocols

R. Janvier, Y. Lakhnech, and L. Mazare


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.

Note: This revision includes a new simplified proof of the reduction theorem.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Unpublished
SecurityCryptographic ProtocolsFormal EncryptionProbabilistic EncryptionDolev-Yao ModelComputational Model
Contact author(s)
laurent mazare @ imag fr
2005-06-10: last of 3 revisions
2005-02-01: received
See all versions
Short URL
Creative Commons Attribution


      author = {R.  Janvier and Y.  Lakhnech and L.  Mazare},
      title = {(De)Compositions of Cryptographic Schemes and their Applications to Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2005/020},
      year = {2005},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.