安全协议的设计与逻辑分析
卿斯汉
©2003 Journal of Software 软 件 学 报 Vol.14, No.7
摘 要:
随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全协议形式化设计的可能性.
关键词: 安全协议;设计;逻辑分析;BAN类逻辑;串空间
密码学 -> 安全协议
安全协议: 实体之间认证、实体之间安全地分配密钥或其他各种秘密、确认发送和接收消息的非否认性
安全协议的形式化分析:
-- 基于知识与信念推理的模态逻辑方法
-- 基于通信状态机模型的研究方法
-- 基于知识推理的代数方法
-- 基于顺序通信进程的CSP方法
-- 串空间模型
the organization of this paper:
1) 第1节讨论基于知识与信念推理的模态逻辑方法,对BAN逻辑及其扩展: GNY逻辑[7]、AT逻辑[8]、VO逻辑[9]进行详尽的研究,比较它们的特点和优缺点.
2) 第2节讨论BAN类逻辑中:SVO逻辑[10],并研究安全协议的逻辑分析方法和串空间模型[4,5]相结合的问题.
3) 第3节讨论安全协议设计原则.然后,通过串空间模型的实例,说明形式化方法如何指导安全协议的正确设计.
4) 第4节是简短的结论,并讨论今后研究的若干方向.
1 安全协议的形式化分析方法
1.1 基于知识与信念推理的模态逻辑方法
1.2 BAN逻辑
BAN逻辑
2 BAN类逻辑分析方法与串空间模型
2.1 SVO逻辑
2.2 串空间模型与BAN类逻辑
模型论语义
串空间模型语义
3.2 应用形式化方法指导安全协议设计
4 结 论