Machine-Checked Security Proofs of Cryptographic Signature Schemes

12 years 1 months ago
Machine-Checked Security Proofs of Cryptographic Signature Schemes
Abstract. Formal methods have been extensively applied to the certiļ¬cation of cryptographic protocols. However, most of these works make the perfect cryptography assumption, i.e. the hypothesis that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. A model that does not require the perfect cryptography assumption is the generic model and the random oracle model. These models provide non-standard computational models in which one may reason about the computational cost of breaking a cryptographic scheme. Using the machine-checked account of the Generic Model and the Random Oracle Model formalized in Coq, we prove the safety of cryptosystems that depend on a cyclic group (like ElGamal cryptosystem), against interactive generic attacks and we prove the security of blind signatures against interactive attacks. To prove the last step, we use a generic parallel attack to create a forgery signature.
Sabrina Tarento
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Authors Sabrina Tarento
Comments (0)