摘要： 针对目前尚无不可否认协议的形式化设计方法，提出一种基于逻辑的不可否认协议形式化设计方法，包括逻辑语言、定理、推理规则及合成规则。协议设计者用逻辑语言描述协议目标，由该目标出发，运用合成规则逐步推导出一个含可信第三方的不可否认协议。实例证明该方法可以很好地用于辅助不可否认协议的设计与改进。

关键词: 不可否认协议, 形式化设计, 逻辑, 可信第三方

Abstract: A formal method based on logic for designing non-repudiation protocols with TTP is presented. The method includes logic language, inference rules and synthetic rules. Protocol designers describe the protocol goals using logic language, then iteratively choose synthetic rules to generate sub-goals which constitute a non-repudiation protocol. CMP1 protocol is advanced by using the method, and result shows that the method is helpful to improve and redesign non-repudiation protocol.

Key words: non-repudiation protocol, formal design, logic, Trusted Third Party(TTP)

中图分类号: 

• TP309