检索结果-南通市图书馆

计算机工程与应用 2010年第19期46卷 100-102页

作者：李廷元秦志光刘晓东张选芳电子科技大学计算机科学与工程学院成都610054 中国民用航空飞行学院计算机学院四川广汉618307

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Need-ham-schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。

关键词：安全协议形式化分析串空间模型认证测试方法 needham-schroeder协议

在线全文

学校读者我要写书评

暂无评论

一种安全协议的逻辑分析与改进

华中科技大学学报（自然科学版） 2004年第7期32卷 4-6页

作者：石曙东李芝棠华中科技大学计算机科学与技术学院湖北武汉430074

采用BAN逻辑对著名的needham schroeder(NS)协议建立理想化协议模型 ,利用协议的初始假设和BAN逻辑的公设分析NS协议的安全性 .分析结果表明 ,该协议只有增加初试假设 ,即用户B获得的会话密钥是新的会话密钥的前提下才能达到认证的目标。

关键词：安全协议 BAN逻辑 needham-schroeder协议

在线全文

学校读者我要写书评

暂无评论

一种改进的NSSK认证协议及其实现方法

小型微型计算机系统 2018年第3期39卷 468-473页

作者：于金刚赵治刚中国科学院大学北京100049

为了保障开源的网络通讯产品如实时消息系统、网络电话等能够在高安全领域得以应用,本文对著名的needhamschroeder(NS)认证协议进行改进和优化,优化后的协议通过采用使接收方与密钥分发中心通信、在密钥分发中心返回的消息中添加发送方... 详细信息

为了保障开源的网络通讯产品如实时消息系统、网络电话等能够在高安全领域得以应用,本文对著名的needhamschroeder(NS)认证协议进行改进和优化,优化后的协议通过采用使接收方与密钥分发中心通信、在密钥分发中心返回的消息中添加发送方身份和各方发送的临时值的方式,达到了确保消息新鲜性、通信双方身份及会话中共享密钥可靠性的目的,同时避免了原生NS协议存在的旧消息重传攻击和身份冒充缺陷.利用模态逻辑BAN逻辑,对改进版的协议进行理想化建模、定义初始假设集合及安全目标集合,并在此基础上使用推理规则,证明了该改进协议完全能够达到认证协议的安全目标.通过硬件及其对应的工具包,实现了该认证协议,并在实际应用中验证.

关键词： needham-schroeder协议形式化验证 BAN逻辑

基于事件逻辑的可证明网络安全协议形式化分析

在线全文

学校读者我要写书评

暂无评论

基于事件逻辑的可证明网络安全协议形式化分析

作者：刘欣倩华东交通大学

学位级别：硕士

形式化方法是分析网络安全协议的一种重要方法,也是信息安全领域的研究热点。形式化方法基于严格的数学概念和逻辑方法,对协议进行描述,在描述过程中可发现协议安全属性的不明确或不完整,有效地降低分析过程复杂度,使协议的安全分析简... 详细信息

形式化方法是分析网络安全协议的一种重要方法,也是信息安全领域的研究热点。形式化方法基于严格的数学概念和逻辑方法,对协议进行描述,在描述过程中可发现协议安全属性的不明确或不完整,有效地降低分析过程复杂度,使协议的安全分析简单、规范、实用。定理证明是形式化方法的一种,目的是证明无穷并发状态下网络安全协议是安全的。事件逻辑是在并发与分布式系统下描述协议和算法的逻辑,是定理证明中一种非常重要的逻辑方法。本文以事件逻辑为基础,对其进行扩展,提出强认证理论。针对needham-schroeder(NS)协议和Neuman-Stubblebine协议进行形式化描述及认证性证明。论文主要工作包括:1、基于事件逻辑,对安全协议的七种动作(生成挑战数、发送消息、接收消息、加密、解密、签名和验证)进行形式化描述,同时给出协议中密钥、挑战数和协议消息的形式化描述。定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出强认证理论。2、对两个主体的NS协议进行研究,针对协议漏洞,对其增加时间戳,避免了重放攻击,运用事件逻辑对改进后的协议进行形式化描述,通过对发送者和接收者的认证证明,说明强认证理论适用于两方的网络安全协议;对三个主体的Neuman-Stubblebine协议进行研究,运用事件逻辑对协议基本序列进行合法定义,证明发送者是安全的而接收者是不安全的,不能达到双向身份认证,说明强认证理论也适用于三方的网络安全协议。3、通过以上分析,认证协议可以通过只对协议诚实主体动作的推理来证明其认证性,事件逻辑适用于多个主体的网络安全协议认证性分析。

关键词：形式化方法事件逻辑强认证理论 needham-schroeder协议 Neuman-Stubblebine协议

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

用户认证协议的安全分析

甘肃科技 2016年第8期32卷 11-13页

作者：齐爱琴西北民族大学数学与计算机科学学院甘肃兰州730000

认证是网络安全中最重要的一个安全目标,所有其他的安全属性例如完整性、不可否认性、可信性等都依赖于通信双方的认证。因此,很多安全认证协议被提出。而判断协议是否有效的方法主要是模拟。模拟只能证明协议在制定的模拟环境下是否可... 详细信息

认证是网络安全中最重要的一个安全目标,所有其他的安全属性例如完整性、不可否认性、可信性等都依赖于通信双方的认证。因此,很多安全认证协议被提出。而判断协议是否有效的方法主要是模拟。模拟只能证明协议在制定的模拟环境下是否可以达到安全目标。而对于正常真实的各种情况无法真正反应。本文提出了模型检测的方法来对其中一种用户认证协议进行了验证,通过模型检测协议的安全属性可以检测系统能达到的任何状态,比模拟的结果更有效。

关键词： needham-schroeder协议规范化 Casper和FDR2

在线全文

学校读者我要写书评

暂无评论

一种描述协议的新模型:线索空间模型

桂林电子工业学院学报 2003年第1期23卷 27-30页

作者：郑卓远周娅桂林电子工业学院计算机系广西桂林541004

线索空间模型是一种新的安全协议模型 ,它可利用线索空间图证明 needham- schroeder协议的某些安全特性。在描述和分析此过程协议存在的漏洞同时并对协议进行了改进。线索空间模型同其他模型相比 ,最大优点就是简洁直观。

关键词：线索空间模型协议束通信 needham-schroeder协议