密码协议分析的信任多集方法

被引：4

作者：

董玲

陈克非

来学嘉

机构：

[1] 上海交通大学计算机科学与工程系

来源：

软件学报 | 2009年 / 20卷 / 11期

关键词：

密码协议; 安全性分析; 形式化方法; 自动化;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

提出了一种基于逻辑的信任多集方法,它与已有的密码协议安全性分析方法本质上不同:每个参与主体建立的新信任只应依赖于该主体已拥有的信任和接收或发送的包含了信任的新鲜性标识符的消息本身.在基于匹配对话和不可区分性的计算模型下,证明了给出的保证密码协议单方认证安全、双方认证安全、单方密钥安全和双方密钥安全的充分必要条件分别满足4个可证安全定义.实例研究和对比分析表明,信任多集方法有以下特点:首先,安全性分析结果要么证明了一个密码协议是安全的,要么指出了密码协议安全属性的缺失,由安全属性的缺失能够直接导出构造攻击的结构;其次,分析方法与密码协议和攻击者能力的具体形式化描述无关;最后,不仅可用于手工分析,而且便于开发出自动验证系统.

引用

页码：3060 / 3076

页数：17

共 8 条

[1]

Towards a completeness result for model checking of security protocols[J] . Gavin Lowe.Journal of Computer Security . 1999 (2‐3)

[2] AN ATTACK ON THE NEEDHAM-SCHROEDER PUBLIC-KEY AUTHENTICATION PROTOCOL [J].

LOWE, G .

INFORMATION PROCESSING LETTERS, 1995, 56 (03) :131-133

[3] A LOGIC OF AUTHENTICATION [J].

BURROWS, M ;

ABADI, M ;

NEEDHAM, R .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1990, 8 (01) :18-36

[4] EFFICIENT AND TIMELY MUTUAL AUTHENTICATION. [J].

Otway, Dave ;

Rees, Owen .

Operating Systems Review (ACM), 1987, 21 (01) :8-10

[5] USING ENCRYPTION FOR AUTHENTICATION IN LARGE NETWORKS OF COMPUTERS [J].

NEEDHAM, RM ;

SCHROEDER, MD .

COMMUNICATIONS OF THE ACM, 1978, 21 (12) :993-999

[6]

Modern Cryptography: Theory and Practice .2 Mao W B. . 2004

[7]

Protocol independence through disjoint encryption .2 Guttman J D,Thayer F J. Proceedings of 13th Computer Security Foundations Workshop . 2000

[8]

Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels .2 Canetti R,Krawczyk H. Proceedings of the Advances in Cryptology-EUROCRYPT2001 . 2001

← 1 →