通信学报2011，Vol.32Issue(3)：18-26,9.
密码学可靠的不可否认协议辅助验证方法
Computationally sound mechanized proof for a non-repudiation protocol
摘要
Abstract
A cryptographically sound computer-aided approach for the Zhou-Gollmann protocol was proposed.Firstly,the protocol was formalized in the computational model, and a cryptography-based attack to the protocol was presented.Secondly, a deficiency in formalizing the fairness property in prior works was discovered.The Zhou-Gollmann protocol was proved to be secure when the encryption scheme satisfies both indistinguishability under chosen plaintext attack and integrity of plaintext, and the signature scheme is unforgeable under chosen message attack.The proof was conducted by combining manual proof with the mechanized prover CryptoVerif.Compared with current approaches, this approach is both sound and with high efficiency.关键词
小可否认协议/计算模型/密码学可靠性/辅助验证Key words
non-repudiation protocol/ computational model/ cryptographically sound/ computer-aided proof分类
信息技术与安全科学引用本文复制引用
冯超,陈岳兵,张权,唐朝京..密码学可靠的不可否认协议辅助验证方法[J].通信学报,2011,32(3):18-26,9.基金项目
国家自然科学基金资助项目(60872052) （60872052）
