Machine-Checked Security Proofs of Cryptographic Signature Schemes
Machine-Checked Security Proofs of Cryptographic Signature Schemes
复制标题
密码签名方案的机器检查安全证明
DOI：
10.1007/11555827_9
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Sabrina Tarento
中科院分区：
文献类型：
--
作者：
Sabrina Tarento
形式化方法已广泛应用于密码协议的认证。然而，大多数这些作品都做出了完美的密码学假设，即假设没有办法在不知道密钥的情况下获得有关密文的明文的知识。不需要完美密码学假设的模型是通用模型和随机预言模型。这些模型提供了非标准的计算模型，其中可以推断破坏加密方案的计算成本。利用Coq形式化的Generic模型和Random Oracle模型的机器校验帐户，证明了依赖于循环群的密码系统（如ElGamal密码系统）对交互式Generic攻击的安全性，并证明了盲签名对交互式攻击的安全性。为了证明最后一步，我们使用一个通用的并行攻击来创建一个伪造签名。
Formal methods have been extensively applied to the certification 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.