一种基于进程代数的安全协议验证消解算法

• 作 者: 刘万伟 周倜 李梦君 李舟军
• 机 构: 国防科技大学计算机学院
• 出 处: 计算机工程与科学
• 发表日期: 2006年7期
• 关键词: 安全协议 进程代数 消解 保密性 认证性 security protocol process algebra reduce security authentic
• 基金项目: 国家自然科学基金资助项目（90104026,60073001）,国家863计划资助项目（2002AAl44040）

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证.本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻辑规则的方法,并提出了基于逻辑规则分类的高效逻辑程序消解算法,对安全协议认证性和保密性进行验证.