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

项目名称： 基于事件逻辑的安全协议形式化分析及验证

项目编号： No.61163005

项目类型： 地区科学基金项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 肖美华

作者单位： 华东交通大学

项目金额： 30万元

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

中文关键词： 安全协议；形式化分析；事件逻辑；基本密码原语理论；

英文摘要：

英文关键词： Security Protocols；Formal Method；Logic of Event；Theory of Basic Cryptographic Primitives；