基于事件逻辑的安全协议形式化分析及验证

安全协议是保障网络信息安全的重要基础，安全协议的分析和验证是当前计算机科学研究的重要课题之一。本研究基于事件逻辑，提出协议基本密码原语理论，设计包含有一阶谓词逻辑公理系统、协议动作公理、时态推导、推理规则、不变式规则的安全协议安全性分析与验证系统S，并保证系统S的可靠性（Soundness）及完备性（Completeness）；阐明基于基本密码原语理论的安全协议不同性质 （认证性、秘密性、非否认性）统一框架表示机理，以及与模型检测技术中线性时态逻辑刻画性质的互模拟关系；在以协议描述语言PDL作为可接受输入语言的安全协议分析与验证系统平台下，不仅对公开密钥及对称密钥协议、而且对IEEE802.11i等实用协议进行分析及验证。上述研究旨在为安全协议的理论化分析、实用化设计和自动化验证等方面探索新的方法和途径。

安全协议是保障网络信息安全的重要基础，安全协议的分析和验证是当前计算机科学研究的重要课题之一。本项目基于事件逻辑，提出了协议基本密码原语理论TBCP；开发了基于TBCP的密码协议安全性分析与验证系统；提出了认证事件逻辑（Authentication Event Logic）理论分析网络安全协议，认证事件逻辑不仅体现协议基本密码原语的抽象构建，而且能表达产生随机数Nonce 的新鲜性（Freshness）、原子性（Atoms）、独立性(Independence)，基本密码原语及操作：消息发送（Send）、消息接收(Receive)、加密(Encrypt)、解密(Decrypt)、数据签名(Sign)、验证(Verify)、诚实主体(Honest)、Property R等。上述理论，适用于公开密钥及对称密钥协议的安全性分析。. 运用事件逻辑理论，依据我们开发的基于知识算法逻辑以及我们自定义的安全协议描述语言（Protocol Description Language，缩写为ProDL）作为可接受输入语言的网络安全协议验证模型生成系统，研究公开密钥及对称密钥协议安全性验证问题。安全协议验证模型生成系统中采用了多项优化策略，包括偏序归约、静态分析、语法重定序、类型检查等，有效地缓解了模型检测过程中状态爆炸问题，显著提高了验证模型的可靠性和开发效率。本项目研究表明，针对认证协议安全性分析，事件逻辑理论比知识算法逻辑更具优势 （无需显式地刻画入侵者模型、协议主体数不受限制），同时，运用事件逻辑理论对安全电子交易协议SET进行了形式化验证及改进，研究与实现了基于事件逻辑与CAPICOM体系的电子签章系统。上述研究为安全协议的理论化分析、实用化设计和自动化验证等方面探索新的方法和途径。