论文部分内容阅读
协议是指两个或者两个以上的参与者为完成某一项特定任务相互约定的执行步骤和执行规则。协议的定义包含三层含义:(1)协议至少有两个参与者;(2)协议在参与者之间表现为消息交换和消息处理交替进行的一系列步骤;(3)协议的执行是为了能够完成某项任务或达成某种共识。 安全协议就是建立在密码体制基础上的—种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。 安全协议的正确性对网络应用的安全至关重要。安全协议攻击者的破坏和安全协议无穷多个会话的并发交叠运行使得安全协议运行时往往难以实现它的设计目标。形式化方法已被证明是分析和验证安全协议的有效手段,安全协议的形式化分析与验证已经成为当前形式化方法领域的一个研究热点。 本文以安全协议作为研究对象,以有效的形式化验证方法作为主要研究内容。本文的主要贡献包括: (1) 安全协议形式化建模、安全协议形式化验证方法和安全协议反例的自动构造算法。 Bruno Blanchet提出了基于Horn逻辑的安全协议模型,它是由基于线性逻辑的安全模型经过抽象解释和程序变换、并对带存在量词的公式进行Skolem化而得到的一个安全协议模型。基于进程代数的安全协议模型使用一组变换规则也可以转换为基于Horn逻辑的安全协议模型。在基于Horn逻辑的安全协议模型,没有描述消息的发送者和接受者,无法区分安全协议诚实角色与安全协议攻击者的形式化刻画。 在对基于Horn逻辑的安全协议模型进行深入分析的基础上,本文提出了基于Horn逻辑的安全协议扩展模型和基于进程代数的安全协议扩展模型。基于Bruno Blanchet的验证方法,本文提出了基于Horn逻辑的安全协议扩展模型的安全协议验证方法,从该方法的验证过程中能自动构造不满足安全性质的安全协议反例。 基于Horn逻辑的安全协议模型是对基于线性逻辑的安全模型进行抽象解释得到的模型。如果安全协议的验证过程表明基于Horn逻辑的安全协议模型满足安全性质,抽象解释保证安全协议满足安全性质;如果安全协议的验证过程表明基于Horn逻辑的安全协议模型不满足安全性质,由于抽象解释可能引入了虚假攻击,抽象解释并不保证安全协议一定不满足安全性质。自动构造不满足安全性质的安全协议反例有助于辨识虚假攻击,有助于分析安全协议出现漏洞的原因,以便对安全协议进行校正。基于Horn逻辑的安全协议扩展模型的安全协议验证过程,本文提出了不满足安全性质的安全协议反例的自动构造算法。