基于PDS的IKE安全协议形式化分析
- 格式：pdf
- 大小：113.09 KB
- 文档页数：3
文档推荐
-
一种形式化分析安全协议的新模型页数:5
下载文档原格式
合集下载
IKE协议与实现
IKE协议与实现一、IKE的作用当应用环境的规模较小时，可以用手工配置SA；当应用环境规模较大、参与的节点位置不固定时，IKE可自动地为参与通信的实体协商SA，并对安全关联库（SAD）维护，保障通信安全。
二、IKE的机制IKE属于一种混合型协议，由Internet安全关联和密钥管理协议（ISAKMP）和两种密钥交换协议OAKLEY与SKEME组成。
IKE创建在由ISAKMP定义的框架上，沿用了OAKLEY的密钥交换模式以及SKEME的共享和密钥更新技术，还定义了它自己的两种密钥交换方式。
IKE使用了两个阶段的ISAKMP：第一阶段，协商创建一个通信信道（IKE SA），并对该信道进行验证，为双方进一步的IKE通信提供机密性、消息完整性以及消息源验证服务；第二阶段，使用已建立的IKE SA建立IPsec SA（如图1所示）。
IKE共定义了5种交换。
阶段1有两种模式的交换：对身份进行保护的“主模式”交换以及根据基本ISAKMP文档制订的“野蛮模式”交换。
阶段2 交换使用“快速模式”交换。
IKE 自己定义了两种交换：1为通信各方间协商一个新的Diffie Hellman组类型的“新组模式”交换；2在IKE通信双方间传送错误及状态消息的ISAKMP信息交换。
1．主模式交换主模式交换提供了身份保护机制，经过三个步骤，共交换了六条消息。
三个步骤分别是策略协商交换、Diffie Hellman共享值、nonce交换以及身份验证交换（如图2所示）。
2．野蛮模式交换野蛮模式交换也分为三个步骤，但只交换三条消息：头两条消息协商策略，交换Diffie Hellman公开值必需的辅助数据以及身份信息；第二条消息认证响应方；第三条消息认证发起方，并为发起方提供在场的证据（如图3所示）。
3．快速模式交换快速模式交换通过三条消息建立IPsec SA：头两条消息协商IPsec SA的各项参数值，并生成IPsec 使用的密钥；第二条消息还为响应方提供在场的证据；第三条消息为发起方提供在场的证据（如图4所示）。
网络安全协议的形式化分析与验证教学课件作者李建华第三章基于模型检测技术的安全协议分析方法课件
另一种则是综合利用定理证明技术来推理所需的安全性质。
3.2.1 CSP的基本概念
1．事件
协议是通过实体间执行一系列的事件（Event）来执行的， 所有可能事件的集合记为∑。
一个典型的CSP事件表示为c.i.j.m，包括一个信道c、一个 消息源i、一个消息目的地j和一个消息m。
3.2.1 CSP的基本概念
3.2.1 CSP的基本概念
3．迹
一个进程的迹（Traces）模型描述了该进程所有可 能的事件序列。例如：
Traces(STOP)={< >}，其中< >是一个空序列，即不管 观察STOP进程多长时间，它都是什么也不做。
Traces(P.a→P□b→SKIP)={<a>n, <a>n<b>,<a>n<b,√>|nN}，其中ab表示a和b的串联，sn 是s的n个副本的串联；√是发送终止信号的事件，当该 信号在迹中出现时就是迹中的最后一个元素。
每一个进程都受到一个特定事件集合的控制。在CSP中，称这类事件 集 是X合和为Y进，程即字P一母定表同。意PX所|| Y有QX表中示的P与通Q信并，联而，Q并一且定P同和意Q所的有字Y母中表的分通别信。
3.2.1 CSP的基本概念
（11）成功终止 SKIP
成功终止通常是由一个进程主动产生的。
协议执行过程中，主体收发消息的动作会引起局部状态的改变，进而 也引起全局状态的改变；
在安全协议全局状态上定义安全属性或不变关系，则安全协议是否满 足安全目标等价于在系统可达的每个全局状态上安全属性或不变关系 是否都能得到满足。
引言
安全协议的模型检测分析方法取得了很大的成功，其优点 是自动化程度高，可以借助自动分析工具来完成分析过程 而不需要用户的参与，并且安全协议存在缺陷时能够自动 生成相应的攻击实例。
3.2.1 CSP的基本概念
1．事件
协议是通过实体间执行一系列的事件（Event）来执行的， 所有可能事件的集合记为∑。
一个典型的CSP事件表示为c.i.j.m，包括一个信道c、一个 消息源i、一个消息目的地j和一个消息m。
3.2.1 CSP的基本概念
3.2.1 CSP的基本概念
3．迹
一个进程的迹（Traces）模型描述了该进程所有可 能的事件序列。例如：
Traces(STOP)={< >}，其中< >是一个空序列，即不管 观察STOP进程多长时间，它都是什么也不做。
Traces(P.a→P□b→SKIP)={<a>n, <a>n<b>,<a>n<b,√>|nN}，其中ab表示a和b的串联，sn 是s的n个副本的串联；√是发送终止信号的事件，当该 信号在迹中出现时就是迹中的最后一个元素。
每一个进程都受到一个特定事件集合的控制。在CSP中，称这类事件 集 是X合和为Y进，程即字P一母定表同。意PX所|| Y有QX表中示的P与通Q信并，联而，Q并一且定P同和意Q所的有字Y母中表的分通别信。
3.2.1 CSP的基本概念
（11）成功终止 SKIP
成功终止通常是由一个进程主动产生的。
协议执行过程中，主体收发消息的动作会引起局部状态的改变，进而 也引起全局状态的改变；
在安全协议全局状态上定义安全属性或不变关系，则安全协议是否满 足安全目标等价于在系统可达的每个全局状态上安全属性或不变关系 是否都能得到满足。
引言
安全协议的模型检测分析方法取得了很大的成功，其优点 是自动化程度高，可以借助自动分析工具来完成分析过程 而不需要用户的参与，并且安全协议存在缺陷时能够自动 生成相应的攻击实例。
形式化分析方法
安全协议的形式化分析方法安全协议是采用密码技术来保障通信各方之间安全交换信息的一个规则序列。
其目的是在通信各方之间提供认证或为新的会话分配会话密钥。
尽管现有的安全协议是安全专家精心设计和详细审核过的但仍然可能存在一些不易发现的安全缺陷有些甚至数年后才被发现。
长期以来，形式化方法被公认为分析安全协议的有力武器。
目前分析安全协议的形式化方法主要有：（1）推理构造法，该方法基于知识和信念推理的模态逻辑，如K3P逻辑等，但K3P逻辑只能分析协议的认证性质而不能分析协议的保密性质；（2）攻击构造法，该方法从协议的初始状态开始，对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索，以期找到协议可能存在的错误。
这种方法主要有基于模型检测技术的模型检测器QRS( 验证语言、代数简化理论模型以及特定专家系统（如特殊目的NRL分析器和Interrogator），但这种方法无法解决状态空间爆炸问题；（3）证明构造法，该方法集成了以上两类方法的思想及多种技术，主要有Bolignano证明方法和Paulson方法等。
以上形式化分析方法的主要缺点是无法解决状态空间爆炸问题在很大程度上被限制在规模很小的协议分析中这显然不适应网络通信规模日益增大等发展的需要。
安全协议是建造网络安全环境的重要基石，是保证网络安全的核心技术。
设计和证明安全协议自身的正确性和安全性，成为网络安全的基础。
形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法，对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。
虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击，但是这些分析方法还存在许多缺陷。
有些形式化分析方法自身不太完善，存在一定的局限性，不能分析和验证某些类型安全协议的安全性；有些只能分析安全协议的不安全性，不能给出协议安全性的精确证明。
在总结安全协议现存各种缺陷的基础上，根据缺陷产生各种原因将缺陷分为：过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。
IKE协议的安全性问题
IKE协议的安全性问题
陈忠良
【期刊名称】《浙江大学学报（工学版）》
【年(卷),期】2002(036)003
【摘要】分析了因特网密钥交换协议(IKE)易于遭受的两种攻击:针对IKE主模式协议的变换载荷攻击和针对IKE主模式中预共享秘密认证协议的反射攻击.Zhou首先分析了IKE主模式协议易于遭受变换载荷攻击,并给出了简单的修改,但这种修改引入了反向的变换载荷攻击.通过对Zhou的修改引入的反向变换载荷攻击和反射攻击的分析,给出了彻底的修正方法,使IKE协议可以防范这两种攻击.
【总页数】5页(P306-309，319)
【作者】陈忠良
【作者单位】浙江大学,信息与电子工程系,浙江,杭州,310027
【正文语种】中文
【中图分类】TN918.91;TP393.08
【相关文献】
1.图书馆网络化建设中新一代协议存在的安全性问题 [J], 纪双龙
2.ML-IKEv2:一种多层IPSec协议中的密钥交换协议 [J], 邓柳;汤凯;乐康
3.论DHCP网络协议的安全性问题与解决 [J], 区咏莹
4.Linux下IKEv1和IKEv2协议的仿真分析 [J], 高翔;马红途
5.SNMP协议在网络性能监测中的应用及其安全性问题的研究 [J], 孙萍萍;吴伟
因版权原因，仅展示原文概要，查看原文内容请购买。
基于CPK的IKE协议的改进
基于CPK的IKE协议的改进
郭亚梅;杨尚森;李益发
【期刊名称】《微计算机信息》
【年(卷),期】2007(023)027
【摘要】本文在简要介绍和分析评述IPsec协议的基础上,基于CPK系统提出了对IPsec协议的改进,并对改进的协议利用逻辑化方法作了详细地安全性分析,指出了改进的协议在安全性和效率等方面所具有的优势,同时对应用环境作了说明.
【总页数】3页(P104-106)
【作者】郭亚梅;杨尚森;李益发
【作者单位】455002,安阳,安阳师范学院;471023,洛阳,洛阳大学现代教育技术中心;450002,郑州,信息工程大学信息工程学院
【正文语种】中文
【中图分类】TP393
【相关文献】
1.基于 CPK 数字签名的 TLS 改进协议* [J], 何青松;王珒;范月霞
2.基于CPK的IPSec协议的改进研究 [J], 何青松;何青林
3.基于CPK和改进ECDH算法的可证安全的认证协议 [J], 侯惠芳;王云侠
4.基于Kerberos对MIKEY协议密钥协商方式的改进 [J], 马利民; 张伟; 姜晓燕
5.基于改进IKE协议的移动IPv6的IPSec架构研究 [J], 张学文
因版权原因，仅展示原文概要，查看原文内容请购买。
网络安全认证协议形式化分析共26页
网络安全认证协议形式化分 析
26、机遇对于有准备的头脑有特别的 亲和力 。 27、自信是人格的核心。
28、目标的坚定是性格中最必要的力 量泉源 之一， 也是成 功的利 器之一 。没有 它，天 才也会 在矛盾 无定的 迷径中 ，徒劳 无功。- -查士 德斐尔 爵士。 29、困难就是机遇。--温斯顿．丘吉 尔。 30、我奋斗，所以我快乐。--格林斯 潘。
Messages meant for a principal cannot be read/accessed by others (secrecy); Guarantee genuineness of the sender of the message (authenticity); Integrity; Non-Repudiation (NRO, NRR); Fairness, etc.
Formal methods, a combination of a mathematical or logical model of a system and its requirements, together with an effective procedure for determining whether a proof that a system satisfies its requirements is correct.
21.08.2021
第二十次全国计算机安全学术交流会
8
Notation
(4) Properties
Lemma 1. B ⊦ m ∧ B ⊆ B’ ⇒ B’ ⊦ m Lemma 2. B ⊦ m’∧ B ∪ {m’ } ⊦ m ⇒ B ⊦ m Lemma 3. B ⊦ m ∧ X ⊑ m ∧ B ⊬ X ⇒ （Y: Y ∈ sub-msgs(m) :
26、机遇对于有准备的头脑有特别的 亲和力 。 27、自信是人格的核心。
28、目标的坚定是性格中最必要的力 量泉源 之一， 也是成 功的利 器之一 。没有 它，天 才也会 在矛盾 无定的 迷径中 ，徒劳 无功。- -查士 德斐尔 爵士。 29、困难就是机遇。--温斯顿．丘吉 尔。 30、我奋斗，所以我快乐。--格林斯 潘。
Messages meant for a principal cannot be read/accessed by others (secrecy); Guarantee genuineness of the sender of the message (authenticity); Integrity; Non-Repudiation (NRO, NRR); Fairness, etc.
Formal methods, a combination of a mathematical or logical model of a system and its requirements, together with an effective procedure for determining whether a proof that a system satisfies its requirements is correct.
21.08.2021
第二十次全国计算机安全学术交流会
8
Notation
(4) Properties
Lemma 1. B ⊦ m ∧ B ⊆ B’ ⇒ B’ ⊦ m Lemma 2. B ⊦ m’∧ B ∪ {m’ } ⊦ m ⇒ B ⊦ m Lemma 3. B ⊦ m ∧ X ⊑ m ∧ B ⊬ X ⇒ （Y: Y ∈ sub-msgs(m) :
IKE协议中存在的安全漏洞
IKE协议中存在的安全漏洞
肖磊;胡众义
【期刊名称】《温州大学学报（社会科学版）》
【年(卷),期】2004(017)003
【摘要】IKE(Internet key exchange)协议是IPSec协议中缺省的密钥管理协议,但是它的实现却相当复杂,所以可能出现安全漏洞.本文主要分析了IKE可能出现的一种安全漏洞.
【总页数】3页(P36-38)
【作者】肖磊;胡众义
【作者单位】温州大学现代教育技术中心;温州大学信息工程学院,浙江,温
州,325035
【正文语种】中文
【中图分类】U491.13
【相关文献】
1.SRTPMIKEY协议在TD-MBMS中业务和内容保护方案中的研究 [J], 曾俊威;彭大芹
2.一种存在于IKE协议中的DoS攻击安全漏洞 [J], 丁勇;彭志威;王育民
3.ML-IKEv2:一种多层IPSec协议中的密钥交换协议 [J], 邓柳;汤凯;乐康
4.Linux下IKEv1和IKEv2协议的仿真分析 [J], 高翔;马红途
5.802.11协议中RTS/CTS机制的安全漏洞分析 [J], 陈伟;俞雷;张迎周
因版权原因，仅展示原文概要，查看原文内容请购买。
网络安全协议的形式化分析与验证课件绪论
信息在开放网络环境中传输遭受到的攻击：
偷听攻击 截取攻击 伪造攻击 篡改攻击 …
网络安全直接关系到信息系统安全，是整个信息 基础结构的安全基础。
维护网络环境安全的技术：
密码技术：主要功能是提供安全的服务，通过使用密码 算法对消息明文进行加密以保证消息本身的安全从而保 证通信过程的安全可靠。 安全协议：是一个分布式算法，它规定了两个或多个通 信主体的安全性。安全协议利用密码技术实现开放网络 环境下的安全通信，达到信息安全的目的，广泛地应用 于身份认证、接入控制和密钥分配等领域。
3.完整性 含义：通常是指数据不能被篡改，或者至少针对数据的任 何篡改都能被检测出来。 目的：保护消息不被未授权地篡改、删除或替代。可以理 解为在储存的数据上再加上一层防止篡改的保护层。 常用方法：封装和签名。
4.不可否认性 含义：不可否认性主要是考虑如何保护通信的一方不被对方 欺骗，在协议执行过程中能够为用户提供证据，来证明协议 中某些步骤确实发生过，而且这些证据是不可伪造的。 不可否认性是电子商务协议的一个重要性质，是保证交易正 常进行的必要条件。 保证不可否认性最常用的技术是数字签名。
第一章
安全协议概述 形式化技术基础
绪 论
形式化方法在安全协议验证中的应用
小结
1.1
安全协议概述
安全协议的基本概念 安全协议的缺陷分析 安全协议的攻击手段 形式化分析方法的重要性
1.1
安全协议概述
信息安全最基本的目标:
实现信息的机密性 保证数据的完整性 实现身份或信息的鉴别性和不可抵赖性 对信息的授权和访问控制 保证信息资源的可用性 …
Internet密钥IKE协议安全性分析
Internet密钥IKE协议安全性分析作者：马萌王全成康乃林来源：《软件》2013年第07期摘要：为了应对Internet密钥交换协议面临的复杂多样的网络威胁和攻击手段，本文详细分析了IKE协议的基本思想和主要存在的四个方面的安全缺陷，为采取更加有效的信息安全技术和方法，堵塞可能的安全漏洞和隐患提供帮助，从而满足日益增长的网络安全应用要求。
关键词：Internet密钥交换协议；IPSec；IKE中图分类号：TP309 文献标识码：A DOI：10.3969/j.issn.1003-6970.2013.07.038本文著录格式：[1]马萌，王全成，康乃林.Internet密钥IKE协议安全性分析[J].软件，2013，34（7）：112-1140 引言在开放性的网络体系中，进行秘密、敏感信息传递时，首先要求通信双方拥有共享密钥，才能够按照安全性需求对数据进行机密性、完整性和身份认证保护。
为了应对Internet密钥交换协议面临的复杂多样的网络威胁和攻击手段，本文详细分析了IKE协议的基本思想和主要存在的四个方面的安全缺陷，为采取更加有效的信息安全技术和方法，堵塞可能的安全漏洞和隐患提供帮助，从而满足日益增长的网络安全应用要求。
1 IKE协议的基本思想IKE协议吸取ISAKMP协议、OAKLEY协议和SKEME协议各自的特点组合而成[1]，同时还重新定义了两种密钥交换方式[1]。
一次典型的IKE密钥协商交换可描述如下（第一阶段采用主模式和公钥签名身份验证）：（1）SA载荷交换，协商认证算法、加密算法等，交换Cookies对；（2）KE载荷，Nonce载荷交换，提供计算共享密钥的有关参数信息。
（3）通信双方分别计算共享密钥参数。
（4）通信双方进行身份验证，构建IKE SA；（5）进行IPSec SA载荷和选择符信息交换，协商IPSec SA的验证算法、加密算法，计算IPSec SA密钥参数，构建IPSec SA。
网络协议知识：IKEv协议的安全性和应用场景
网络协议知识：IKEv协议的安全性和应用场景随着互联网技术的不断发展，网络安全问题越来越受到重视，特别是在企业内网和跨企业网络间互联的场景下，安全性显得尤为关键。
为了保障互联网上的通信安全，一些安全协议逐渐被广泛应用在网络通信中。
其中，IKEv协议是一种常用的安全性协议，本文将对这一协议的安全性和应用场景进行探究和讨论。
一、IKEv协议的安全性1.加密性IKEv协议主要是通过使用IKE（Internet Key Exchange）协议来实现各种安全协议的自动协商、密钥交换和互认等功能。
在IKEv协议中，加密算法和密钥长度都是可以被灵活配置的。
一般情况下，IKEv协议使用的是高强度的加密算法，如AES算法、3DES算法等，这些加密算法在保证通信安全性的同时，能够有效地防止数据被窃听和篡改。
2.身份认证在VPN连接中，对于连接的两个终端必须能够互相明确身份才能建立安全通道，而IKEv协议正是通过使用数字证书和预共享密钥等认证机制来实现身份的验证。
数字证书是一种数字化身份证书，具有不可篡改和不可伪造的特点，能够有效地防止身份伪冒和欺骗等问题。
预共享密钥则是通过事先约定一个密钥，再在建立连接时共享，用于加强身份验证的安全性。
3.安全性升级随着计算机技术的快速发展，安全性协议和加密算法的攻破成为可能，进而导致一些安全漏洞的出现。
为了应对这种情况，IKEv协议允许在通信过程中实现安全协议和加密算法的升级和更换。
这样一来，即使某种加密算法被攻破，也不会对现有通信安全带来威胁，从而提高了整个系统的安全性。
二、IKEv协议的应用场景IKEv协议广泛应用于VPN连接、安全网关和远程访问等场景，下面分别介绍一下其主要应用场景：1. VPN连接在企业内网或跨企业间互联时，需要建立虚拟专线来实现安全通信。
VPN连接通过使用加密协议和身份验证机制，可以有效地防范数据泄露和篡改等问题，保障通信安全。
IKEv协议正是作为VPN连接中关键的安全协议之一，被广泛应用于企业内网、数据中心和跨机构联网中。
网络安全认证协议形式化分析
Formal methods, a combination of a mathematical or logical model of a system and its requirements, together with an effective procedure for determining whether a proof that a system satisfies its requirements is correct.
Model checking advantages (compare with theory proving): automatic; counterexample if violation
Use LTL (Linear temporal logic ) to specify properties
FDR (Lowe); Mur (Mitchell);
16.10.2020
.
8
Logic of Algorithmic Knowledge
Definition 1. Primitive propositions P0s for security: p, q ∈ P0s ::= sendi (m) Principal i sent message m recvi (m) Principal i received message m hasi (m) Principal i has message m
Submessage: sub-msgs(m) ≜ {m’ ∈ Msg | m’ ⊑ m }
16.10.2020
.
6
Notation
(3) Derivation (⊦, Dolev-Yao model)
m∈B ⇒B⊦m B ⊦ m ∧ B ⊦ m’ ⇒ B ⊦ m• m’ (pairing) B ⊦ m• m’ ⇒ B ⊦ m ∧ B ⊦ m’ (projection) B ⊦ m ∧ B ⊦ k ⇒ B ⊦ {m}k (encryption) B ⊦ {m}k ∧ B ⊦ k-1 ⇒ B ⊦ m (decryption)
Model checking advantages (compare with theory proving): automatic; counterexample if violation
Use LTL (Linear temporal logic ) to specify properties
FDR (Lowe); Mur (Mitchell);
16.10.2020
.
8
Logic of Algorithmic Knowledge
Definition 1. Primitive propositions P0s for security: p, q ∈ P0s ::= sendi (m) Principal i sent message m recvi (m) Principal i received message m hasi (m) Principal i has message m
Submessage: sub-msgs(m) ≜ {m’ ∈ Msg | m’ ⊑ m }
16.10.2020
.
6
Notation
(3) Derivation (⊦, Dolev-Yao model)
m∈B ⇒B⊦m B ⊦ m ∧ B ⊦ m’ ⇒ B ⊦ m• m’ (pairing) B ⊦ m• m’ ⇒ B ⊦ m ∧ B ⊦ m’ (projection) B ⊦ m ∧ B ⊦ k ⇒ B ⊦ {m}k (encryption) B ⊦ {m}k ∧ B ⊦ k-1 ⇒ B ⊦ m (decryption)
网络安全协议的形式化分析与验证教学课件ppt作者李建华第二章基于模态逻辑技术的安全协议分析方法
6．消息新鲜性规则
R15：
如果P相信X是新鲜的，那么P相信与X级联的整 个消息都是新鲜的。
7．密钥与秘密对称规则 R16： R17：
R18： R19：
2.1.3 应用实例
采用BAN逻辑分析安全协议 可按协议的形式化描述、定义初 始化假设、定义协议目标和推理 及验证4个步骤进行。
BAN逻辑协议形式化分析流 程如右图所示。
再由初始化假设A7，应用仲裁规则R5，可得 （2-7）
通过M4、M5，主体A、B均确信对方在线。由M4可知 由式（2-4）中的，应用消息意义规则R1，可得
（2-8）
再由信仰规则R9，可得
-9） 由式（2-4）中的，根据随机数验证规则R4，可得
） 同样，由M5可知，经过类似推理，可得
（2 （2-10
nGNY逻辑对协议进行分析的步骤如下：
n 对消息标记“不是由此首发”标识*，并进行理想化表示 。 n 给出系统初始化假设。 n 运用GNY推理规则对协议进行形式化分析与验证。
2.2.2 AT逻辑
n AT逻辑对BAN逻辑的改进包括以下几方面。
n 从语义的角度分析了BAN逻辑，对某些概念进行了修改，对BAN 逻辑中的若干定义和推理规则进行了整理，抛弃了其中语义和实现细 节混合的部分。 n 对某些逻辑构件引入了更加直接的定义，免除了对诚实性的隐含 假设。 n 引进了全部命题联结词，并将推理规则改写成公理的形式，使逻 辑语法更加清晰、简洁；同时也简化了推理规则，整个逻辑只有两条 基本推理规则，即MP（Modus Ponens）规则和Nec（ Necessitation）规则。
上述BAN逻辑的形式化过程也为协议的改进提供了方向 。
2.2 类BAN逻辑
Ø由于简单、直观，有较强的分析能力，能够发现认证协议中 的许多安全漏洞和冗余的信息流，BAN逻辑得到了广泛的应用 ，很快成为分析认证协议的常规方法。 Ø随着应用的深入，人们发现BAN逻辑也存在许多缺点，主要表 现在以下几方面： Ø 1．协议的理想化过程不规范 Ø 2．协议的初始化假设不合理 Ø 3．缺乏完备性 Ø 4．缺乏一个定义良好、确切的语义
无线网络安全协议的形式化分析方法
主要是提 供给一个参 与方关于其通 信对方 身份的一定确 信度
的一种方 式 ，认证协 议包含 了实体认证协议 、消息认证 协议
等其他协 议 ，并且认证 协议主要 是用来 防止 假 冒、否认 等相 关攻击 的。其次是认 证及秘钥交换 协议 ，这 主要是 为了给身
份 已经被 确认的参 与方建立一个 共享秘密 ， 目前这种 方式是
应用研发
式 化 分 析 方 法
金磊 ／ 新 疆 阿克 苏教 育 学院
摘 要 ：传统的有线 网络 由于受到环境等务件 的制约，在各方面都存在着亟需解决的问题 ，那 么，发展可行的无线通信 网络技 术 也 就成 为 网络发 展 的 必然趋 势 。本 丈对 无 线 网络 安全 协议 的形式 化 方 法进行 了全 面的概 述 ，分析 了无 线 网络 的安全威胁以及具体表现，着重探讨 了无线网络安全协议的形式化分析方法。
无 线移 动设 备 在存 储 能力 ， 以及计 算 能力 等其 他 的方 面都
存 在一 定 的局 限性 ，也 就 导致 在有 线环 境 下 ，许 多安 全方 案 以及 安 全 技 术 并 不 能 够 直 接 的在 无 线 环 境 中应 用 ， 比 如 ： 防火墙 通 过无 线 电波进 行 的 网络通 信 并不 具 备一 定 的 相 关作 用 ，而任 何 人在 特 定 的区域 范 围 内都能 够截 获 或者 是插 入 网络数 据 ，导致无 线 网络面 临着 一些 安全威 胁 ］ 。 而针 对 于安全 威胁 ，我们 可 以将 其分 为故 意威 胁 和偶 然威胁 这两种形 式，而故 意威 胁又可 以进 一步分 为主动故 意 威胁和 被动故意 威胁 ，无 线网络安全威胁 ，主要表 现在 以下 几个方 面 。首先 ，攻击者伪装 成为合法 的用户 ，通 过无线接 入非法 访 问网络 资源 ，从 而给 无线 网络 带来安全 威胁 ，这 是
网络协议的形式化分析
网络协议的形式化分析网络协议的形式化分析网络协议的形式化分析【1】摘要：随着形式化方法和技术的日趋完善，网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础，渗透到网络协议分析、综合、测试等各环节的软件工程方法。
本文从网络协议的基本要素、协议的形式化模型介绍了网络协议，并从协议的性质描述、不变性分析、可达性分析、基于有序二叉判决图的符号模型检验对网络协议进行了形式化设计与验证，最后进行了测试。
关键词：网络协议形式化分析符号模型检验协议一词最早出现在通信系统，协议历史拥有像通信一样古老的历史。
从古至今，人们一直都在不断的探索研究，怎样才能建立一个能够在快速在远距离上传输信息的系统。
如果想要实现信息在远距离间传递，不光需要硬件设备，也就是发送和接收信号的设备，还需要建立一整套能够规定信号所代表的意义以及传递接收信号方式的规则、标准或者约定，这个规则就是协议。
1 网络协议的基本要素一套完整的，能够确保计算机网络可以顺利进行数据通信的网络协议要包括下边的五点基本要素：(1)协议所提供的服务。
(2)对协议运行环境所进行的假设。
(3)用来实现协议的消息词汇。
(4)对该词汇中每个消息的编码。
(5)用来控制消息一致性的过程规则。
实现计算机之间高度自动化数据通信的网络协议，一般都会极其复杂。
借鉴对复杂系统问题分析研究的思想，分层结构对于理解和设计网络协议有着重要的作用。
“七层”协议结构模型是目前网络协议的标准体系结构，也成为了网络协议开发的基础。
2 协议的形式化模型协议分析和设计其中一项核心技术就是形式化模型。
网络协议的形式化规格可以在形式化模型的基础上实现，从而为协议的形式化分析与验证、协议综合、协议测试、以及协议实现等提供良好的基础。
形式化模型包括以下几点。
2.1 协议的有限状态机模型有限状态机包括有限状态集、输入集和状态转移规则集;有限状态集，用于描述系统中的不同状态;输入集用于表征系统所接收的不同输入信息;状态转移规则集用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。
网络安全认证协议形式化分析
hasi (m) Principal i has message m
05
Logic of Algorithmic Knowledge
Definition 2. An interpreted security system S = (R, ∏R), where ∏R is a system for security protocols, and ∏R is the following interpretation of the primitive propositions in R.
Properties
Notation
第二十次全国计算机安全学术交流会
Lemma 1. B ⊦ m ∧ B ⊆ B’ ⇒ B’ ⊦ m
Lemma 2. B ⊦ m’∧ B ∪ {m’ } ⊦ m ⇒ B ⊦ m
Lemma 3. B ⊦ m ∧ X ⊑ m ∧ B ⊬ X ⇒ （Y: Y ∈ sub-msgs(m) : X ⊑ Y∧ B ⊦ Y）∧ （b: b ∈ B : Y ⊑ b）∧ （Z, k: Z ∈ Msg ∧ k ∈ Key : Y = {Z}k ∧ B ⊬ k-1）
*
*
Notation
(1) Messages a ∈Atom ::= C | N | k | m ∈ Msg ::= a | m• m | {m}k (2) Contain Relationship (⊑) m ⊑ a ≜ m = a m ⊑ m1• m2 ≜ m = m1• m2 ∨ m ⊑ m1∨ m ⊑ m2 m ⊑ {m1}k ≜ m = {m1}k ∨ m ⊑ m1 Submessage: sub-msgs(m) ≜ {m’ ∈ Msg | m’ ⊑ m }
Verification Using SPIN/Promela
IKEv2协议的分析与改进
(1)
{SK_d | SK_ai | SK_ar | SK_ei | SK_er | SK_pi | SK_pr } =
prf+ (SKEYSEED, Ni | Nr | SPIi | SPIr)
(2)
其中，子密钥的值顺序地取自 prf+的生成比特值；g^ir 是一
个取自 Diffie-Hellman 交换的共享秘密值；Ni 和 Nr 是交换的
在密钥交换过程中由于kerkei分别由服务器和客户端产生因此双方根据式1生成的skeyseed以及用来加密和认证的密钥只有通信双方知道攻击者无法获得密钥而消息3和消息4使用新生成的密钥进行加密所以攻击者无法解密消息3和消息4从而不能获得idiidr以及双方产生的auth避免了通信双方的身份泄漏和离线字典攻击
<Msg Octets_r>)
其中，“Key Pad for IKEv2”是 17 Byte 的字符串，用于抵御
字典攻击；Shared Secret 是预共享密钥；AUTH_i 和 AUTH_r
分别为发起方和响应方产生的 AUTH 值。
3 IKEv2 协议的分析与改进
IKEv2 协议无论采用数字签名认证方式还是预共享密钥
输，采用数字签名认证时，需要传输数字证书载荷。
2.2 密钥材料的生成 IKEv2 从 IKE_SA_INIT 交 换 的 nonce 和 建 立 的
Diffie-Hellman 共享密钥中计算出一个主密钥 SKEYSEED。
SKEYSEED 被进一步用来计算其他 7 个密钥材料：SK_ai 和
SK_ar 用于认证后续交换的消息；SK_ei 和 SK_er 用于加解
nonce 值；prf 是 IKEv2 协商的伪随机函数。各算法的密钥材
- 1、下载文档前请自行甄别文档内容的完整性，平台不提供额外的编辑、内容补充、找答案等附加服务。
- 2、"仅部分预览"的文档,不可在线预览部分如存在完整性等问题,可反馈申请退款(可完整预览的文档不适用该条件!)。
- 3、如文档侵犯您的权益，请联系客服反馈,我们会尽快为您处理(人工客服工作时间：9:00-18:30)。
Ｖ Ｚ ３５ Ｎ ｏ ３ ． ．
Ａｕ ２ ｇ． ００７
文章 编 号 ：Ｏ Ｏ ２ ６ （ ０ ７ ０ —０ ３ —０ １０一 ３７２０）３ ０３ ３
基于 Ｐ ＤＳ的 Ｉ ＫＥ安 全 协议 形 式 化 分 析
王 惠斌 ， 青 美 ， 跃 飞 常 祝
（ ． 放 军信 息 工 程 大 学 信 息 工 程 学 院 ， 州 ４ ０ ０ ；． １解 郑 ５ ０ ２ ２ 河南 司 法 警 官 职 业 学 院 信 息 技 术 系 ， 州 ４ ０ ０ ） 郑 ５０ ２
维普资讯
第 ３ ５卷 第 ３期 ２０ ０ ７年 ８月
河南师范大学学报（ 自然科 学版 ）
Ｊｏ ｒ ａ ｆ Ｈｅ ａ ｒ ｌＵｎｖ ｒｉ （ ｔ ｒ ｌＳ ｉｎ ｅ ｕ ｎ ｌ ｎ ｎ Ｎｏｍａ ｉｅｓｔ Ｎａ ｕ ａ ｃｅｃ ） ｏ ｙ
其核心语句 为：
Ｉ— Ｒ ： 。 ＋ ｇ
Ｒ— Ｉ ： ｇ ＳＩ ＋ ， ＧＲ（Ｈ Ｍ Ａ ＣＫ（ ， ，ＤＲ）） ｇ ｇ Ｉ Ｉ一－ ： ＳＩ ｌ （ Ｍ Ａ ＣＫ（ 。 ｇ Ｉ ） ，Ｒ Ｇ （Ｈ ｇ ， ， Ｄ１ ）
３ ＰＤＳ 禾 口ＰＣＩ
Ｐ Ｓ是一 个 协 议衍 生 推 导 系 统 ， 从 基 本 的 成 分 出 发 ， 用 一 系 列 的 组 合 （ ｏ ｏｉｏ ） 精 练 （ ｅｉｅ ｎ ） 和 转 换 Ｄ 它 使 Ｃ ｍｐ ｓ ｉ 、 ｔｎ Ｒ ｆ ｍｅ ｔ 、 ｎ
２ Ｉ 协议 ＫＥ
因特 网密 钥 交 换 协 议 （ＫＥ 是 用 于 Ｉ Ｓ ｃ 全 协 议 认 证 密 钥 交 换 协 议 的 ＩＴＦ Ｉｔｒｅ Ｅ ｇｎ ｅｉｇＴ ｓ ｏｃ 联 网 工 Ｉ ） Ｐｅ安 Ｅ （ｎｅｎ ｔ ｎ ｉｅｒ ａｋＦ ｒｅ互 ｎ 程任务组） 当前 标 准Ⅲ ， Ｉ Ｓｃ协 议 族 的 关 键 组 成 部 分 ， 因特 网 的 安 全 通 信 和 安 全 服 务 中发 挥 着 非 常 重 要 的 作 用 ， 安 全 是 Ｐｅ 在 其
文献标 识 码 ： Ａ
１ 安全 协议 的分 析与 设计
计 算 机 网络 是 信 息 社 会 的基 石． 当前 ， 息 安 全 已成 为 制 约 计 算 机 网 络 应 用 的 一 个 瓶 颈 ， 且 随 着 计 算 机 网 络 的 迅 猛 发 信 并
展 而 日益 变 得 突 出． 息 的 安 全 性 已经 不 是 仅 仅 依 赖 一 个 好 的加 密 算 法 就 可 以 得 以解 决 的 问 题 ， 需 要 一 些 综 合 的 安 全 理 信 它 论 、 全 措施 和 安 全 技 术 来 保 证 ［ ． 这 些 理 论 、 施 和 技 术 中 ， 全 协议 起 着 至 关 重 要 的作 用 ． 实 际 应 用 中 ， 们 需 要 可 信 安 １在 ］ 措 安 在 人
的机 制 来 为 通 信 实 体 进 行 身 份 认 证 和分 发 密 钥 ， 就迫 使 人 们 研 究 和 设 计 出 了 各 种 安 全 协 议 ． 而 已有 的 安 全 协 议 往 往 被 证 这 然
实 并 不 如 它 们 的设 计 者 所 期 望 的那 样 安 全 ， 量 的 实例 说 明 ， 大 即使 参 加 认 证 协议 的 主 体 只 有 ２个 或 ３个 ， 在整 个 协 议 中 交 换 的 消 息 只有 ３条 或 ５条 ， 计 一 个 正 确 且 没 有 安 全 缺 陷 的认 证 协 议 也 是 很 困难 的． 设 为 了保 证 安 全 协 议 的安 全 性 ， 种 有 效 的途 径 是采 用 形 式 化 方 法 对 协议 进 行 全 面 、 格 的分 析 和验 证 ． 一 严 安全协议形式化分析从 ８ Ｏ年 代 起 至 今 ， 展 极 为 迅 速 ， 弓 了 为 数 众 多 的学 者 和 研 究 人 员 致 力 于 该 项 工 作 ， 发 吸 Ｉ 目前 已成 为 安 全 协 议 研 究 领 域 的 一 个 极 为 重 要 的 、 具 理 论深 度 的 前 沿 问 题 ． 颇 综 合 各 种 理 论 和 方 法 ，ｔｎｏｄ大 学 的 Ａｎ ｐ ｍ Ｄ ｔ Ｓａ ｆｒ ｕ ａ ａｔ 士 等 人 最 近 发 展 了一 套 安 全 协 议 形 式 化 设 计 系统 Ｐ Ｓ ｒｔｃｌ ａ博 Ｄ （Ｐ ｏｏ ｏ Ｄ ｒ ａｉｎＳ ｓｅ 和 协 议 组 合 逻 辑 系统 （ ｒｔｃｌ ｏ ｏ ｉｏ ｏ ｉ） Ｃ ２］ 可 用 于 安 全 协 议 的形 式 化 设 计 和 分 析 ． ｅｉ ｔ ｙ ｔｍ） ｖ ｏ Ｐ ｏｏｏ ｍｐ ｓ ｉｎＬ ｇｃＰ Ｉ 。 ， Ｃ ｔ ｌ
摘 要 ： 绍了支持复杂协议形式化并 行推导的 Ｐ 介 ＤＳ协议衍 生推导 系统 和 Ｉ ＫＥ协议 ． 出了使 用 Ｐ Ｓ形 式 给 Ｄ
化 衍 生 Ｉ Ｅ协 议 的核 心 认 证 部 分 的 方 法 ． Ｋ
关 键词 ： 安全协议 ； 化分 析 ； Ｅ协议 ；Ｄ 形式 Ｉ Ｋ ＰＳ
中图分 类号 ： Ｐ ９ Ｔ ３３
性的重要性不容置疑．
Ｉｔｒｅ 密 钥 交 换 协 议 是 无 可 信 第 三方 参 与 的 公 钥 协 议 ． 协 议 主 要 是 为 通 信 用 户 双 方 提 供 身 份 认 证 方 法 、 用 的 密 钥 、 ｎｅｎ ｔ 该 采
数 据 加 密 方 式 等 问 题 ， 过 协 商 后 达 成 一 致 意 见 的 协议 ． 经
（ ａ ｓ ｒ ｔ ｎ 等 工 作 ， 持 复 杂 协 议 的并 行 推 导 ． Ｔｒｎ ｆ ｍａｉ ） ｏ ｏ 支
Ｐ Ｓ包 含 一 个称 之 为 基 件 （ｏ ｏ ｅ ｔ的 基 本 构 件 集 合 和 一 个 从 旧 协议 构造 新 协 议 的 操 作 集 合 ． 些 操 作 可