基于计算语义的安全协议验证逻辑

作     者：唐朝京 鲁智勇 冯超 TANG Chao-jing;LU Zhi-yong;FENG Chao

作者机构：国防科技大学电子科学与工程学院湖南长沙410073 中国洛阳电子装备试验中心河南洛阳471003 

基　　金：国家自然科学基金(No.61301236 No.61303061) 

出 版 物：《电子学报》 (Acta Electronica Sinica)

年 卷 期：2014年第42卷第6期

页      码：1179-1185页

摘      要：提出了一个基于计算语义的安全协议验证逻辑,能准确描述安全协议中的各种计算行为和通信行为.设计了基于该逻辑的证明系统,能对密码学中常用加密算法的各类安全属性规范直接描述,具有密码学可靠性.发现了计算协议组合逻辑在加密算法安全性建模时存在的不可靠性,并提出了解决方法.通过对Needham-Schroeder-Lowe协议安全性的证明,验证了逻辑的证明能力.与大部分验证方法不同的是,本逻辑属于由密码学算法安全性到协议安全性的正向推理方法,兼具符号方法的易用性和计算方法的可靠性.

主 题 词：加密算法 安全性 形式逻辑 计算语义 

学科分类：0839[0839] 08[工学] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.0372-2112.2014.06.022

馆 藏 号：203131980...