一种不可否认协议形式化设计方法  

Formal Design Method for Non-repudiation Protocols

作　　者：刘晶[1] 伏飞[1] 肖军模[1] 陆阳[1] 

机构地区：[1]解放军理工大学通信工程学院,南京210007

出　　处：《计算机工程》2008年第4期164-166,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(69931040);江苏省自然科学基金资助项目(BK2004015)

摘　　要：针对目前尚无不可否认协议的形式化设计方法,提出一种基于逻辑的不可否认协议形式化设计方法,包括逻辑语言、定理、推理规则及合成规则。协议设计者用逻辑语言描述协议目标,由该目标出发,运用合成规则逐步推导出一个含可信第三方的不可否认协议。实例证明该方法可以很好地用于辅助不可否认协议的设计与改进。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. CMPI protocol is advanced by using the method, and result shows that the method is helpful to improve and redesign non-repudiation protocol.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]