International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Peeter Laud

Publications

Year
Venue
Title
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
EPRINT
2014
EPRINT
2014
EPRINT
2014
EPRINT
2014
EPRINT
2008
EPRINT
{Threshold Homomorphic Encryption in the Universally Composable Cryptographic Library
Peeter Laud Long Ngo
Protocol security analysis has become an active research topic in recent years. Researchers have been trying to build sufficient theories for building automated tools, which give security proofs for cryptographic protocols. There are two approaches for analysing protocols: formal and computational. The former, often called Dolev-Yao style, uses abstract terms to model cryptographic messages with an assumption about perfect security of the cryptographic primitives. The latter mathematically uses indistinguishability to prove that adversaries with computational resources bounds cannot gain anything significantly. The first method is easy to be automated while the second one can give sound proofs of security. 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.
2006
EPRINT
Computationally Sound Secrecy Proofs by Mechanized Flow Analysis
Michael Backes Peeter Laud
We present a novel approach for proving secrecy properties of security protocols by mechanized flow analysis. In contrast to existing tools for proving secrecy by abstract interpretation, our tool enjoys cryptographic soundness in the strong sense of blackbox reactive simulatability/UC which entails that secrecy properties proven by our tool are automatically guaranteed to hold for secure cryptographic implementations of the analyzed protocol, with respect to the more fine-grained cryptographic secrecy definitions and adversary models. Our tool is capable of reasoning about a comprehensive language for expressing protocols, in particular handling symmetric encryption and asymmetric encryption, and it produces proofs for an unbounded number of sessions in the presence of an active adversary. We have implemented the tool and applied it to a number of common protocols from the literature.
2005
EPRINT
Universally Composable Time-Stamping Schemes with Audit
We present a universally composable time-stamping scheme based on universal one-way hash functions. The model we use contains an ideal auditing functionality (implementable in the Common Reference String model), the task of which is to check that the rounds' digests are correctly computed. Our scheme uses hash-trees and is just a slight modification of the known schemes of Haber-Stornetta and Benaloh-de Mare, but both the modifications and the audit functionality are crucial for provable security. The scheme turns out to be nearly optimal -- we prove that in every universally composable auditable time-stamping scheme, almost all time stamp requests must be communicated to the auditor.
2000
EPRINT
Accountable Certificate Management using Undeniable Attestations
This paper initiates a study of accountable certificate management methods, necessary to support long-term authenticity of digital documents. Our main contribution is a model for accountable certificate management, where clients receive attestations confirming inclusion/removal of their certificates from the database of valid certificates. We explain why accountability depends on the inability of the third parties to create contradictory attestations. After that we define an undeniable attester as a primitive that provides efficient attestation creation, publishing and verification, so that it is intractable to create contradictory attestations. We introduce authenticated search trees and build an efficient undeniable attester upon them. The proposed system is the first accountable long-term certificate management system. Moreover, authenticated search trees can be used in many security-critical applications instead of the (sorted) hash trees to reduce trust in the authorities, without decrease in efficiency. Therefore, the undeniable attester promises looks like a very useful cryptographic primitive with a wide range of applications.
1998
CRYPTO