基于认证测试的安全协议分析

微信服务号

微信订阅号

2025年4月1日 7:37 星期二

首页 > 过刊浏览>2006年第17卷第1期 >148-156

基于认证测试的安全协议分析
DOI:
                        
                    
CSTR:
                        
                    
作者:
                        杨明杨明
东南大学,计算机科学与工程系,网络室,江苏,南京,210096
在期刊界中查找
在百度中查找
在本站中查找
罗军舟罗军舟
东南大学,计算机科学与工程系,网络室,江苏,南京,210096
在期刊界中查找
在百度中查找
在本站中查找

                    
作者单位:
作者简介:
通讯作者:
中图分类号:
基金项目:Supported by the National Natural Science Foundation of China under Grant No.90412014 (国家自然科学基金); the Jiangsu Provincial Key Laboratory of Network and Information Security under Grant No. BM2003201 (江苏省"网络与信息安全"重点实验室);the Jiangsu Provincial High-Tech Rese

Analysis of Security Protocols Based on Authentication Test

Author:

YANG Ming
YANG Ming

在期刊界中查找
在百度中查找
在本站中查找
LUO Jun-Zhou
LUO Jun-Zhou

在期刊界中查找
在百度中查找
在本站中查找

Affiliation:

Fund Project:

摘要

图/表

访问统计

参考文献 [15]

相似文献 [20]

引证文献

资源附件

文章评论

摘要:

认证测试是一种新型的在Strand空间模型基础上发展而来的安全协议分析与辅助设计技术,可用于大部分协议的关联属性的分析;但是与Strand空间模型一样,它主要用于协议正确性证明,在协议为何不正确以及如何进行改进这个问题上处理分析能力较弱.在认证测试概念的基础上,结合逻辑分析的优点,提出了增强型认证测试EAT(enhanced authentication test)和Correspondence函数等概念来对安全协议进行关联属性的分析,很好地解决了这一问题与原有技术相比,该方法更为形式化,协议分析人员可以很方便地进行手动分析,并且更有利于协议分析自动化工具的实现.

关键词:网络安全;协议分析;Strand空间模型;认证测试;认证逻辑

Abstract:

Authentication Test is a new type of analysis and design method of security protocols based on Strand space model, and it can be used for most types of the security protocols. However, as a Strand space model, it is inclined to be used for the proof of correctness, and is relatively weaker for incorrectness analysis. This paper proposes the concepts of Enhanced Authentication Test (EAT) and the correspondence function that can solve the problem. Compared with the original concept, the new approach is more formal and can make protocol analysis easier both by hand and automatically.

Key words:network security;protocol analysis;Strand space model;authentication test;authentication logic

参考文献

[1]Fàbrega FJT,Herzog JC,Guttman JD.Strand spaces:Why is a security protocol correct? In:Proc.of the 1998 IEEE Symp.on Security and Privacy.Los Alamitos:IEEE Computer Society Press,1998.160-171.http://ieeexplore.ieee.org/iel4/5528/14832/00674832.pdf?.tp=&arnumber=674832&isnumber= 14832

[2]Fàbrega FJT,Herzog JC,Guttman JD.Strand spaces:Proving security protocols correct.Journal of Computer Security,1999,7(2-3):191-230.

[3]Paulson LC.The inductive approach to verifying cryptographic protocols.Journal of Computer Security,1998,6(1):85-128.

[4]Guttman JD,Fàbrega FJT.Authentication tests.In:Proc.of the 2000 IEEE Symp.on Security and Privacy.Los Alamitos:IEEE Computer Society Press,2000.96-109.http://ieeexplore.ieee.org/ie15/6864/18435/00848448.pdf?tp=&arnumber=848448& isnumber=18435

[5]Guttman JD,Fàbrega FJT.Authentication tests and the structure of bundles.Theoretical Computer Science,2002,283(2):333-380.

[6]Guttman JD.Security protocol design via authentication tests.In:Proc.of the 2002 IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,2002.92-103.http://ieeexplore.ieee.org/iel5/7957/21985/01021809.pdf?tp=&arnumber= 1021809&isnumber=21985

[7]Woo TYC,Lam SS.A semantic model for authentication protocols.In:Proc.of the 1993 IEEE Computer Society Symp.on Research in Security and Privacy.Los Alamitos:IEEE Computer Society Press,1993.178-194.http://ieeexplore.ieee.org/ie12/902/7168/00287633.pdf?.tp=&arnumber=287633&isnumber=7168

[8]Song DXD.Athena:A new efficient automatic checker for security protocol analysis.In:Proc.of the 12th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,1999.192-202.http://ieeexplore.ieee.org/ie15/6332/16921/00779773.pdf?.tp=&arnumber=779773&isnumber= 16921

[9]Song D,Berezin S,Perrig A.Athena:A novel approach to efficient automatic security protocol analysis.Journal of Computer Security,2001,9(1):47-74.

[10]Syverson P.Towards a strand semantics for authentication logic.Electronic Notes in Theoretical Computer Science,1999,20:143-157.http://citeseer.ist.psu.edu/syverson99towards.html

[11]Cervesato I,Durgin N,Kanovich M,Scedrov A.Interpreting strands in linear logic.In:Veith H,Heintze N,Clark E,eds.Proc.of the 2000 Workshop on Formal Methods and Computer Security.Chicago,2000.http://theory.stanford.edu/～iliano/papers/fmcs00.ps.gz

[12]Ji QG,Qing SH,Zhou YB,Feng DG.Study on strand space model theory.Journal of Computer Science and Technology,2003,18(5):553-570.

[13]Fan H,Feng DG.Security Protocol Theory and Method.Beijing:Science Press,2003.41-42 (in Chinese).

[14]Burrows M,Abadi M.A logic of authentication.ACM Trans.on Computer Systems,1990,8(1):18-36.

[13]范红,冯登国.安全协议理论与方法.北京:科学出版社,2003.41-42.

引用本文

杨明,罗军舟.基于认证测试的安全协议分析.软件学报,2006,17(1):148-156

复制

文章指标

点击次数:4485
下载次数: 5554
HTML阅读次数: 0
引用次数: 0

历史

收稿日期:2004-06-03
最后修改日期:2005-07-28
录用日期:
在线发布日期:
出版日期:

微信服务号

微信订阅号

引用本文

分享

文章指标

历史

文章二维码

微信服务号

微信订阅号

引用本文

分享

微信扫一扫：分享

文章指标

历史

文章二维码