Therefore there is a demand to bridge the gap between two methods in order to have better security-proof tools. One idea is to prove that some Dolev-Yao style cryptographic primitives used in formal tools are computationally sound for arbitrary active attacks in arbitrary reactive environments, i.e universally composable. As a consequence, protocols that use such primitives can also be proved secure by formal tools.
In this paper, we prove that a homomorphic encryption used together with a non-interactive zero-knowledge proof in Dolev-Yao style are sound abstractions for the real implementation under certain conditions. It helps to automatically design and analyze a class of protocols that use homomorphic encryptions together with non-interactive zero-knowledge proofs, such as e-voting.Category / Keywords: justifying Dolev-Yao model,universally composable, cryptographic library, threshold homomorphic encryption Date: received 25 Aug 2008, last revised 25 Aug 2008 Contact author: ngothanglong at yahoo com Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation Note: The first submission missed the references Version: 20080827:152521 (All versions of this report) Discussion forum: Show discussion | Start new discussion