应用逻辑推导图方法对一个不可否认协议的分析  

ANALYSIS OF A NON-REPUDIATION PROTOCOL USING LOGICAL DEDUCTION MAP ANALYSIS METHOD OF SECURITY PROTOCOL

作　　者：王涛[1] 刘永杰 

机构地区：[1]华南师范大学计算机学院,广东广州510631 [2]广东南方电视台,广东广州510600

出　　处：《华南师范大学学报（自然科学版）》2008年第1期46-51,共6页Journal of South China Normal University(Natural Science Edition)

基　　金：广东省自然科学基金资助项目(06330905)

摘　　要：以之前所提出基于模态逻辑的协议推导分析方法为基础,用Java专家系统外壳(JESS)实现了协议推导分析工具,对一个具体的不可否认协议进行分析,以验证逻辑推导图方法的作用.分析结果清晰地显示各协议内容对协议目标实现的作用,并以此为基础说明协议内容中的冗余.通过与传统协议分析方法进行比较,说明了这一方法可以更清晰地说明协议内容对协议目标的贡献作用.同时,也在分析过程中指出了SVO逻辑协议分析方法对假设的过度依赖性这一缺陷.Security protocol analysis method usually can＇ t clarify the function of a protocol factor to the realization of protocol goal. With the protocol deduction analysis method based on modal logic, using Java Expert System Shell （JESS）, a protocol deduction analysis tool is realized and used in the analysis of a non - repudiation protocol, which shows the functions of protocol factors to the realization of protocol goal and leads to the determination of redundancy in this protocol. Comparing with the result before, this method can clarify the contributions of protocol factors. On the other hand, it is presented that the modal - logic based protocol analyzing method is over dependency on assumptions.

关 键 词：安全协议 形式化分析 SVO逻辑 自动推导 JESS 

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