一种形式化分析安全协议的新模型
- 格式：pdf
- 大小：168.35 KB
- 文档页数：5
文档推荐
-
一种形式化分析安全协议的新模型页数:5
下载文档原格式
合集下载
一种适于带时间戳安全协议的形式化分析方法_范玉涛
C G E I ) [3]， Σ 是一个有限的非空颜色集； P是 其中： T 是 一 个 有 限 变 迁 集 ；A 是 一 个 一个有限位置集；
这样的安全协议， 由于这种协议使用时间
信息作为时间戳包含在所传递的消息中， 因此特别 需要保证时间相关的安全属性。 本文基于 CPN 模型检测方法， 提出一种适用于
WMF 协议在共享密钥体制下使用了时间戳来
Var(t ) = {v|v Î Var(G (t )) Ú $a Î A(t ) v Î Var( E (a))}
保证会话密钥通过服务器到达接收端。这里的时间 戳表示消息发送的时间， S 和 B 在接收到消息时检查 时间戳是否新鲜， 如果超过了限定的范围， 则认为会 话失效。具体协议描述如下： A→ S： A.{Ta， B， K}KA ， S S→ B： {Ts， A， K}KB， S 第一步， 发 起 者 A 向 服 务 器 S 发 送 消 息 A.{Ta， B， K}KA ， S， 在消息中包含了 A 的身份识别消息， 用 A 和 S 之间的密钥 KA ， S 加密， 同时包含了消息产生 的时间 （Ta） ， 接收者的身份 （B） ， 以及 A 希望和 B 共 享的密钥 K。第二步， 可信服务器转发给 B 一个消息， 包含当前时间 （Ts） ， 发起者身份， 以及将共享的密钥 K， 全部用密钥 KB， S 加密。在这两步中， 接收者必须 检查消息中包含的时间戳以保证消息的新鲜性 [5]。
4
带有时间戳的安全协议的 CPN 检测
为了验证本文所提出的方法的有效性， 以下以
函数，I:P ® Expers 满足 "p Î P:[Type( I ( p)) = C ( p) MS ， 该 函数把每个位置 p 映射为不包含变量的表达式。
这样的安全协议， 由于这种协议使用时间
信息作为时间戳包含在所传递的消息中， 因此特别 需要保证时间相关的安全属性。 本文基于 CPN 模型检测方法， 提出一种适用于
WMF 协议在共享密钥体制下使用了时间戳来
Var(t ) = {v|v Î Var(G (t )) Ú $a Î A(t ) v Î Var( E (a))}
保证会话密钥通过服务器到达接收端。这里的时间 戳表示消息发送的时间， S 和 B 在接收到消息时检查 时间戳是否新鲜， 如果超过了限定的范围， 则认为会 话失效。具体协议描述如下： A→ S： A.{Ta， B， K}KA ， S S→ B： {Ts， A， K}KB， S 第一步， 发 起 者 A 向 服 务 器 S 发 送 消 息 A.{Ta， B， K}KA ， S， 在消息中包含了 A 的身份识别消息， 用 A 和 S 之间的密钥 KA ， S 加密， 同时包含了消息产生 的时间 （Ta） ， 接收者的身份 （B） ， 以及 A 希望和 B 共 享的密钥 K。第二步， 可信服务器转发给 B 一个消息， 包含当前时间 （Ts） ， 发起者身份， 以及将共享的密钥 K， 全部用密钥 KB， S 加密。在这两步中， 接收者必须 检查消息中包含的时间戳以保证消息的新鲜性 [5]。
4
带有时间戳的安全协议的 CPN 检测
为了验证本文所提出的方法的有效性， 以下以
函数，I:P ® Expers 满足 "p Î P:[Type( I ( p)) = C ( p) MS ， 该 函数把每个位置 p 映射为不包含变量的表达式。
一种描述协议的新模型:线索空间模型
一种描述协议的新模型：线索空间模型
郑卓远;周娅
【期刊名称】《桂林电子科技大学学报》
【年(卷),期】2003(023)001
【摘要】线索空间模型是一种新的安全协议模型,它可利用线索空间图证明Needham-Schroeder协议的某些安全特性.在描述和分析此过程协议存在的漏洞同时并对协议进行了改进.线索空间模型同其他模型相比,最大优点就是简洁直观,是形式化技术的一个重要的研究方向.
【总页数】4页(P27-30)
【作者】郑卓远;周娅
【作者单位】桂林电子工业学院,计算机系,广西,桂林,541004;桂林电子工业学院,计算机系,广西,桂林,541004
【正文语种】中文
【中图分类】TP309
【相关文献】
1.局部网络通信协议形式描述的新混合模型 [J], 李腊元
2.一种基于EFSM的变电站通信协议一致性测试模型描述方法 [J], 王延安;余义传;张丹;肖登明
3.一种理性安全协议的博弈逻辑描述模型 [J], 刘海;彭长根;张弘;任祉静
4.一种新的安全协议及其串空间模型分析 [J], 皮建勇;杨雷;刘心松;李泽平
5.实例化空间:一种新的安全协议验证逻辑的语义模型 [J], 苏开乐;岳伟亚;陈清亮;ZHENG Xi-Zhong
因版权原因，仅展示原文概要，查看原文内容请购买。
tamarin prover安全协议语法
tamarin prover安全协议语法Tamarin Prover是一种用于分析安全协议的形式化验证工具，它采用了自定义的安全协议语法。
本文将对Tamarin Prover的安全协议语法进行详细介绍和解释。
Tamarin Prover的安全协议语法基于应用层代理逻辑，并通过一种称为符号执行的方法进行协议分析。
这使得Tamarin Prover能够检测协议中可能存在的安全漏洞和攻击。
在Tamarin Prover中，安全协议被建模为一组规则，这些规则描述了协议中的消息传递和状态变化。
每个规则包含一个或多个前提条件和一个结果，前提条件描述了规则应用的条件，结果描述了规则应用之后的状态变化。
在安全协议语法中，可以定义以下几种类型的规则：1. 规则：这是最基本的规则类型，描述了消息的传递和处理。
规则可以定义消息的发送、接收和处理的行为。
例如，以下是一个简单的规则示例：rule["发送M1到B","接收M2来自B"]-->["发送M3到C","接收M4来自C"];这个规则表示在发送消息M1到B并接收消息M2来自B之后，发送消息M3到C并接收消息M4来自C。
2. 初始化规则：这种规则描述了协议开始运行时的初始状态。
它定义了初始化的条件和协议的起始状态。
以下是一个初始化规则的示例：rule["初始条件"]-->["初始状态"];这个规则表示协议在初始状态下满足所定义的初始条件。
3. 超级规则：这种规则允许将其他规则组合在一起形成更复杂的行为模式。
它可以用于描述许多规则之间的关系和顺序。
以下是一个超级规则的示例：rule["规则1","规则2"]-->["规则3"];这个规则表示在规则1和规则2被应用后，规则3将被应用。
一种改进的Woo-Lam密码协议模型
一种改进的Woo-Lam密码协议模型
赵宇;袁霖;王亚弟;韩继红
【期刊名称】《计算机应用》
【年(卷),期】2006(26)9
【摘要】提出了一种改进的Woo-Lam密码协议模型,即eWoo-Lam模型.与Woo-Lam模型相比,新模型具有以下特点:增强了模型中关于密码学原语操作的描述语法,使得对密码协议主体行为的描述更加精确,提高了模型在检测协议攻击方面的能力;引入了匹配运算机制,保障了模型安全性证明的有效性;提出了七条形式化准则,规范了模型的抽象过程;扩充了模型基于状态迁移的形式语义,使其更加精确合理;重新给出了模型安全性的形式定义,使其更具一般性.
【总页数】5页(P2116-2120)
【作者】赵宇;袁霖;王亚弟;韩继红
【作者单位】信息工程大学,电子技术学院,河南,郑州,450004;信息工程大学,电子技术学院,河南,郑州,450004;信息工程大学,电子技术学院,河南,郑州,450004;信息工程大学,电子技术学院,河南,郑州,450004
【正文语种】中文
【中图分类】TP309.07
【相关文献】
1.一种双方不可否认密码协议的分析与改进 [J], 李艳平
2.一种基于规划理论的密码协议形式模型 [J], 赵宇;王亚弟;韩继红;范钰丹;张超
3.一种改进的密码协议形式化模型 [J], 张畅;王亚弟;韩继红;郭渊博
4.对一种基于动态密码体制的Kerberos协议的改进 [J], 卢小良;袁丁
5.一种利用动态密码体制改进Kerberos协议的方法 [J], 胡汉平;朱海燕;张宝良;王祖喜
因版权原因，仅展示原文概要，查看原文内容请购买。
一种新的安全协议形式化分析方法——证据逻辑
维普资讯
第３ ４卷 第 ２期
Ｖ １ ４ ０ ３ ＿．
・
计
算
机
工
程
２０ ０８年 １月
Ｊ ｎ ａ ｙ２ ０ ａ ｕ ｒ ０ ８
Ｎｏ ２ ．
Ｃｏ ｐ ｔ ｒＥｎ ｉ ｅ ｒ ｎ ｍ ｕ ｅ ｇｎ ｅ ｉ ｇ
安 全技 术 ・
一
文章 编号：１ ｏ＿４８０８ ２ ０２ ３ 文献标识码：Ａ ０ ＿３２（０） —０９—ｏ ０确设计至 关重 要 ，近 十几年来 国内外学者对这一技 术进 行了较为深入的研究 ，提 出 了多种 形式化 分析方法 ，其 中最 具影响力 的是 Ｂ Ｎ 逻 Ａ 辑…。Ｂ Ｎ逻辑通过对协议主体 的信仰进行推理 ，成功发现 Ａ 了 Ｎｅｄ ａ Ｓｈｏ ｄｒ协议、Ｋ ｒｅｏ ｅｈ ｍ—ｃｒｅ ｅ ｅ ｒｓ协议等几个著名协议 ｂ 中存在 的漏 洞。 之后在 Ｂ Ｎ类逻辑的基础之上 ， Ａ 一些增 强和
［ ｓｒ ｃｌＴ ｅ￣ｒ ｌ ａｙｉ ｍｅ ｄ ｒ ｖｒ ｍｐ ｒ ｔｔ ｈ ｃｕａ ｅｉｎｏ ｅ ｓｃ ｒｙ ｐｏｏｏｓ ｈｓｐｐ ｒｉｔ ｄ ｃｓａｎ ｗ Ａｂｔａｔ ｈ ｍａ ａ ｌｓ ￣ｏ ｓａｅ ｅｙ ｉ ｏｔ Ｏ ｔｅ ａｃ ｒｔ ｄ ｓ ｆｔ ｅｕ ｔ ｒｔｃ ｌ ｎ ｓ ｎ ａ ｅ ｇ ｈ ｉ 、Ｔ ｉ ａｅ ｎｒ ｕｅ ｅ ｏ
ｈ ｘｓ ｎ ｏ ｋ ｐ ｏ ｆｌ ｉ，ｗ ｉｈ Ｃ ｂ ｓｄ ｔ ｌ ｚ ｕ ｎｉ ｔ ｒ ｔｃ ｌ ｈ ｅ ｘ ｈ ｅ ｐｏ ｏ ｏ ｓｎ ｏ — ｕ ｉｔ ｔｅ ｅ ｉ ｉｇ ｗ ｒ ， ｒ ｏ ｇ ｃ ｈ ｃ ａ ｅ ｕ ｅ Ｏ ａ ａｙ ｅ ｔｅ ａ ｔｅ ｔ ａｉｎ ｐ ｏｏ ｏ ｓ ｔｅ ｋ ｙ ｅ ｃ ａ ｇ ｒｔ ｃ ｌ ａ ｄ ｔｅ ｎ ｎｒ ｐ ｄａｉｎ ｔ ｏ ｎ ｎ ｈ ｈ ｃ ｏ ， ｎ ｈ ｅ ｏ
第３ ４卷 第 ２期
Ｖ １ ４ ０ ３ ＿．
・
计
算
机
工
程
２０ ０８年 １月
Ｊ ｎ ａ ｙ２ ０ ａ ｕ ｒ ０ ８
Ｎｏ ２ ．
Ｃｏ ｐ ｔ ｒＥｎ ｉ ｅ ｒ ｎ ｍ ｕ ｅ ｇｎ ｅ ｉ ｇ
安 全技 术 ・
一
文章 编号：１ ｏ＿４８０８ ２ ０２ ３ 文献标识码：Ａ ０ ＿３２（０） —０９—ｏ ０确设计至 关重 要 ，近 十几年来 国内外学者对这一技 术进 行了较为深入的研究 ，提 出 了多种 形式化 分析方法 ，其 中最 具影响力 的是 Ｂ Ｎ 逻 Ａ 辑…。Ｂ Ｎ逻辑通过对协议主体 的信仰进行推理 ，成功发现 Ａ 了 Ｎｅｄ ａ Ｓｈｏ ｄｒ协议、Ｋ ｒｅｏ ｅｈ ｍ—ｃｒｅ ｅ ｅ ｒｓ协议等几个著名协议 ｂ 中存在 的漏 洞。 之后在 Ｂ Ｎ类逻辑的基础之上 ， Ａ 一些增 强和
［ ｓｒ ｃｌＴ ｅ￣ｒ ｌ ａｙｉ ｍｅ ｄ ｒ ｖｒ ｍｐ ｒ ｔｔ ｈ ｃｕａ ｅｉｎｏ ｅ ｓｃ ｒｙ ｐｏｏｏｓ ｈｓｐｐ ｒｉｔ ｄ ｃｓａｎ ｗ Ａｂｔａｔ ｈ ｍａ ａ ｌｓ ￣ｏ ｓａｅ ｅｙ ｉ ｏｔ Ｏ ｔｅ ａｃ ｒｔ ｄ ｓ ｆｔ ｅｕ ｔ ｒｔｃ ｌ ｎ ｓ ｎ ａ ｅ ｇ ｈ ｉ 、Ｔ ｉ ａｅ ｎｒ ｕｅ ｅ ｏ
ｈ ｘｓ ｎ ｏ ｋ ｐ ｏ ｆｌ ｉ，ｗ ｉｈ Ｃ ｂ ｓｄ ｔ ｌ ｚ ｕ ｎｉ ｔ ｒ ｔｃ ｌ ｈ ｅ ｘ ｈ ｅ ｐｏ ｏ ｏ ｓｎ ｏ — ｕ ｉｔ ｔｅ ｅ ｉ ｉｇ ｗ ｒ ， ｒ ｏ ｇ ｃ ｈ ｃ ａ ｅ ｕ ｅ Ｏ ａ ａｙ ｅ ｔｅ ａ ｔｅ ｔ ａｉｎ ｐ ｏｏ ｏ ｓ ｔｅ ｋ ｙ ｅ ｃ ａ ｇ ｒｔ ｃ ｌ ａ ｄ ｔｅ ｎ ｎｒ ｐ ｄａｉｎ ｔ ｏ ｎ ｎ ｈ ｈ ｃ ｏ ， ｎ ｈ ｅ ｏ
一种混合的安全协议形式化分析技术
现有 的 两种 重 要 的形式 化 分析 工 具 为 。： 种是 基 于模 型 检 测技 术 的形 式 化证 伪 工 具 ； 种 是基 于 一 一
逻 辑 推证 技 术 的形式 化 证 明工 具 ． 种工 具 具有 一 定 的互 补性 ， 两 因此 综 合其 各 自的优 点 是 十分 必要 的 ．
１ 引 言
安 全 协议 为 网上用 户 的安 全需 求 提 供解 决 方 案 ， 可保 护 计 算 机 系 统 和 网 上通 信 免 遭 恶 意攻 击 Ⅲ ． 但 由于 安全 协议 所 处 的恶 意 的 网络通 信 环 境 ， 以及 安 全协 议 自身设 计 的 困难性 ， 使得 安 全 协 议是 易 错 的 ， 并 且 错误 很 难通 过 人 的直 观加 以识 别 ． 因此 ， 在对 协议 进 行分 析 时 ， 需借 助 形 式化 的分析 工 具 ．
干诚 实 主体 和 一个 入 侵者 （ 诚 实 主体 ） 成 的 系统 ． 一个 主 体 在协 议运 行 中的状 态 由其 自身 的局 部 变 不 组 每
量来说明， 而整 个协 议 运 行 的状 态则 由全局 变 量来 说 明 ， 局 变 量 中包 括 每 一 个 诚 实 主 体 的局 部 变 量 和 全 入 侵 者 的局 部变 量 ． 次 描述 入 侵者 的攻击 能 力 ． 其 在模 型检测 技 术 中 ， 入侵 者 能够 任 ，９ ９年 ７月 生 ， 师 ， 士 生 女 １６ 讲 博
维普资讯
第 ３期
范 红 冯 登 国 ： 种 混 合 的 安 全 协 ｛ ； 一 Ｈ 式化 分 析 技 术
２１ ４
以下两 方 面 ： 一是 对 于 消息 ． 括 对 获取 的 消息 的 级联 与 分离 ， 包 以及 如获 取 可对 消息 进 行 加 密 和解 密 运 算
逻 辑 推证 技 术 的形式 化 证 明工 具 ． 种工 具 具有 一 定 的互 补性 ， 两 因此 综 合其 各 自的优 点 是 十分 必要 的 ．
１ 引 言
安 全 协议 为 网上用 户 的安 全需 求 提 供解 决 方 案 ， 可保 护 计 算 机 系 统 和 网 上通 信 免 遭 恶 意攻 击 Ⅲ ． 但 由于 安全 协议 所 处 的恶 意 的 网络通 信 环 境 ， 以及 安 全协 议 自身设 计 的 困难性 ， 使得 安 全 协 议是 易 错 的 ， 并 且 错误 很 难通 过 人 的直 观加 以识 别 ． 因此 ， 在对 协议 进 行分 析 时 ， 需借 助 形 式化 的分析 工 具 ．
干诚 实 主体 和 一个 入 侵者 （ 诚 实 主体 ） 成 的 系统 ． 一个 主 体 在协 议运 行 中的状 态 由其 自身 的局 部 变 不 组 每
量来说明， 而整 个协 议 运 行 的状 态则 由全局 变 量来 说 明 ， 局 变 量 中包 括 每 一 个 诚 实 主 体 的局 部 变 量 和 全 入 侵 者 的局 部变 量 ． 次 描述 入 侵者 的攻击 能 力 ． 其 在模 型检测 技 术 中 ， 入侵 者 能够 任 ，９ ９年 ７月 生 ， 师 ， 士 生 女 １６ 讲 博
维普资讯
第 ３期
范 红 冯 登 国 ： 种 混 合 的 安 全 协 ｛ ； 一 Ｈ 式化 分 析 技 术
２１ ４
以下两 方 面 ： 一是 对 于 消息 ． 括 对 获取 的 消息 的 级联 与 分离 ， 包 以及 如获 取 可对 消息 进 行 加 密 和解 密 运 算
基于串空间和状态转换的认证协议分析方法
摘 要 串空间是一种新兴的安全协议 形式化分析模 型。串空间模型 中的理论证 明方法 虽然 严谨 ， 但难 度很 大。本
文 基 于 串空 间模 型 ， 先 定 义 系统 状 态 ， 以 Ｎ ｅ ｈ ｍ Ｓｈｏ ｄｒＬ ｗｅ 钥 认 证 协 议 为 例 说 明 系统 状 态 转换 的 分 析 首 并 ｅｄ ａ －ｃ ｒｅｅ－ ｏ 公
化的分析方法被公认为分析认证 协议 的最有效 手段 。 １９ ９ ８年 ， ａｒｇ 、 ｒｏ Ｆ ｂｅａ Ｈｅｚｇ和 Ｇｕｔ ｎ提 出 了协议 的 串 ｔ ｍａ （ ｔａｄ 空间模型［ ， Ｓｒｎ ） ２ 并应 用该 理论证 明了 Ｎｅｄ ａ Ｓ ｈｏ— ］ ｅｈ ｍ－ｃ ｒｅ
ｄ ｒＬ ｗｅｐ ｂ ｉ ｋ ｙ ａ ｔ ｅ ｔ ａｉｎｐ ｏｏ ｏ． Ｉ ｖ ｓｉａｉｇｎ ｎ ｅ ｎ ｔａ ｓｔ ｎ ｅｗｅ ｎ ｓ ｓｅ ｓａｅ ，ｗｅｄ ａ ｓ ｍｅ ｅ－ ｏ ｕ ｌ ｅ ｕｈ ｎ ｉ ｔ ｒ ｔｃ １ ｎ ｅ ｔ ｔ ｏ ｃ ｓｉ ｒｎ ｉｉ ｓｂ ｔ ｅ ｙ ｔｍ ｔｔｓ ｃ ｃ ｏ ｇ ｎ ｏ ｒｗ ｏ ｓ ｎ ｆｃ ｎ ｏ ｃ ｕ ｉ ｎ ． Ｆ ｎ ｌ ｉ ｉ ａ ｔｃ ｎ ｌ ｓｏ ｓ ｉ ａ ｌ ｇ ｉ ｙ。ｔ ｅ ｓ ｃ ｒｔ ｆＮｅ ｄ ａ ｈ ｅ ｕ ｉｙ ｏ ｅ ｈ ｍ－Ｓ ｈ ｏ ｄ ｒ Ｌ ｗｅ ｐ ｏ ｏ ｏ Ｓ ｖ ｌ ａ ｅ ． Ｔｈ ｓ ｎ ｗ ｔ ｏ ｏ ｃ ｒ ｅ ｅ － ｏ ｒ ｔ ｃ Ｉｉ ａ ｉ ｔ ｄ ｄ ｉ ｅ ｍｅ ｈ ｄ ｆ ｒ ａ ａ ｙ ｉｇ ａ ｔ ｅ ｔｃ ｔ ｎ ｐ ｏ ｏ ｏ ｓ ｉ ｉ ｌ ｎ ｆｉｉ ｎ ，ａ ｄ ｉ ｉ ｐ ｏ ｅ ｔ ｅａ ｔ ｍａ ｅ ． ｎ ｌ ｚｎ ｕ ｈ ｎ ｉａ ｉ ｒ ｔ ｃ ｌ ｓ ｓｍｐ ｅ ａ ｄ ｅ ｆｃｅ ｔ ｎ ｔ ｓ ｒ ｎ Ｏ ｂ ｕ ｏ ｔ ｄ ｏ
文 基 于 串空 间模 型 ， 先 定 义 系统 状 态 ， 以 Ｎ ｅ ｈ ｍ Ｓｈｏ ｄｒＬ ｗｅ 钥 认 证 协 议 为 例 说 明 系统 状 态 转换 的 分 析 首 并 ｅｄ ａ －ｃ ｒｅｅ－ ｏ 公
化的分析方法被公认为分析认证 协议 的最有效 手段 。 １９ ９ ８年 ， ａｒｇ 、 ｒｏ Ｆ ｂｅａ Ｈｅｚｇ和 Ｇｕｔ ｎ提 出 了协议 的 串 ｔ ｍａ （ ｔａｄ 空间模型［ ， Ｓｒｎ ） ２ 并应 用该 理论证 明了 Ｎｅｄ ａ Ｓ ｈｏ— ］ ｅｈ ｍ－ｃ ｒｅ
ｄ ｒＬ ｗｅｐ ｂ ｉ ｋ ｙ ａ ｔ ｅ ｔ ａｉｎｐ ｏｏ ｏ． Ｉ ｖ ｓｉａｉｇｎ ｎ ｅ ｎ ｔａ ｓｔ ｎ ｅｗｅ ｎ ｓ ｓｅ ｓａｅ ，ｗｅｄ ａ ｓ ｍｅ ｅ－ ｏ ｕ ｌ ｅ ｕｈ ｎ ｉ ｔ ｒ ｔｃ １ ｎ ｅ ｔ ｔ ｏ ｃ ｓｉ ｒｎ ｉｉ ｓｂ ｔ ｅ ｙ ｔｍ ｔｔｓ ｃ ｃ ｏ ｇ ｎ ｏ ｒｗ ｏ ｓ ｎ ｆｃ ｎ ｏ ｃ ｕ ｉ ｎ ． Ｆ ｎ ｌ ｉ ｉ ａ ｔｃ ｎ ｌ ｓｏ ｓ ｉ ａ ｌ ｇ ｉ ｙ。ｔ ｅ ｓ ｃ ｒｔ ｆＮｅ ｄ ａ ｈ ｅ ｕ ｉｙ ｏ ｅ ｈ ｍ－Ｓ ｈ ｏ ｄ ｒ Ｌ ｗｅ ｐ ｏ ｏ ｏ Ｓ ｖ ｌ ａ ｅ ． Ｔｈ ｓ ｎ ｗ ｔ ｏ ｏ ｃ ｒ ｅ ｅ － ｏ ｒ ｔ ｃ Ｉｉ ａ ｉ ｔ ｄ ｄ ｉ ｅ ｍｅ ｈ ｄ ｆ ｒ ａ ａ ｙ ｉｇ ａ ｔ ｅ ｔｃ ｔ ｎ ｐ ｏ ｏ ｏ ｓ ｉ ｉ ｌ ｎ ｆｉｉ ｎ ，ａ ｄ ｉ ｉ ｐ ｏ ｅ ｔ ｅａ ｔ ｍａ ｅ ． ｎ ｌ ｚｎ ｕ ｈ ｎ ｉａ ｉ ｒ ｔ ｃ ｌ ｓ ｓｍｐ ｅ ａ ｄ ｅ ｆｃｅ ｔ ｎ ｔ ｓ ｒ ｎ Ｏ ｂ ｕ ｏ ｔ ｄ ｏ
物联网中安全通信协议的形式化分析
物联网中安全通信协议的形式化分析
吴名欢;程小辉
【期刊名称】《桂林理工大学学报》
【年(卷),期】2013(033)002
【摘要】针对物联网通信协议安全性不足和使用非形式化方法进行分析时容易出现错误的问题,提出了一种物联网安全通信协议,建立了协议主体模型和攻击者模型,采用通信顺序进程CSP的形式化方法对协议模型进行了分析.该通信协议对传送的信息进行加密,采用的加密方式是散列函数结合异或运算.协议主体进行了相互认证,认证服务器为协议主体通信分配了会话密钥,解决了读写器非法扫描和信息安全传送的问题.利用故障发散改进检测器(FDR)对该协议模型CSP进程进行了检测,结果表明:该协议主体进行了相互认证,会话密钥是安全的,所提出的物联网通信协议是安全可靠的,CSP方法用于分析协议的安全性是可行的.
【总页数】6页(P333-338)
【作者】吴名欢;程小辉
【作者单位】桂林理工大学广西矿冶与环境科学实验中心,广西桂林541004;桂林理工大学信息科学与工程学院,广西桂林541004;桂林理工大学广西矿冶与环境科学实验中心,广西桂林541004;桂林理工大学信息科学与工程学院,广西桂林541004
【正文语种】中文
【中图分类】TP309.2
【相关文献】
1.Casper／FDR和串空间在物联网通信协议中的形式化分析 [J], 吴名欢;程小辉
2.列车运行控制系统中安全通信协议的形式化分析 [J], 陈黎洁;单振宇;唐涛
3.物联网中安全通信协议的形式化分析 [J], 高爱玲
4.CBTC系统通信协议的设计和形式化分析 [J], 杨森
5.无人机无线通信协议的形式化认证分析与验证 [J], 刘栋;连晓峰;王宇龙;谭励;赵宇琦;李林
因版权原因，仅展示原文概要，查看原文内容请购买。
IEEE802.16安全认证协议的形式化分析
２２ＩＥ ８ ２１ ｅＰ Ｍ ２ ． Ｅ Ｅ ０ ．６ Ｋ ｖ 认证协议简介
在 Ｉ Ｅ ８ ２１ｄ的基 础 上，Ｉ Ｅ ０ ． Ｅ Ｅ ０． ６ ＥＥ ８ ２１ ６工作 组于 ２ ０ ０５
２ＩＥ ８ ２１ Ｅ ０ ．６认证协议介绍 Ｅ
２１ＩＥ ８ ２１ ｄＰ Ｍｖ 认 证 协 议简 介 【 ． Ｅ Ｅ ０ ．６ Ｋ １ 】
【 关键词 】 Ａ 逻辑 安全密钥管理 认证协议 ＢＮ
１引言
Ｉ Ｅ ８ ２１ Ｅ Ｅ０． ６工作组相继推出了 ８ ２１ｄ和 ８ ２１ｅ ０． ６ ０ ． 两个版 ６
认 证信 息消息 ：ｓ ｓ在初 始测距完成 ，取得 与 Ｂ Ｓ的物理 同步后，向 ＢＳ 送 一条认证信息消息 ，该消息包含了 ｓ 发 ｓ生
Ｉ Ｅ ０． ＥＥ ８ ２１ ６工 作 组 对 ８ ２１ａ Ｓ ０． 、 Ｓ ６
年发布 了新 的版本 ８ ２１ｅ ０ ． ，与 ８ ２１ｄ相 比，其主要特点是 ６ ０． ６ Ｂ 支持移动性 ，它是一种固定和移动宽带无线接入系 Ｓ
Ａ ｕｈ ｎ ｉａｉ ｎ Ｉ ｆ ｒ ａ ｏ ｔ ｅ ｔ ｔ ｎ ｏ ｍ ｔ ｎ ｃ ｏ
｛ Ｋｅｃａ ｇ） Ａ ｘ ｈ ｎ ｅ
Ｋｅ ｑ ｅ ｔ ｙ Ｒｅ ｕ ｓ
考图１ ，主要区别 在于 每条消息所包 含的内容 。这
２ ｏ ．９ ０ ８Ｏ
３ ７
里对认证流程进行分析时，我们将 ８ ２１ ｄ中的 ｓ ０． ６ ｓ改为 ＭＳ ， 体现终端的移动性。 认证信息消息 ： ＭＳ在初始测距完成 ，取得 与 Ｂ Ｓ的物理 同步后 ，向 ＢＳ发送一条认证信息消息 ，该 消息包含了 ＭＳ生
本 ，作为 目前宽带无线接入技 术的排头 兵。其中 ８ ２１ ｄ以固 ０． ６ 定模 式 为主，而 ８ ２１ｅ在这基 础上，提 升了终 端的移动性 ， ０． ６ 支持客户终端 以车载速 度移动通信。随着 网络应用的迅速 发
一种基于SPIN的安全协议形式化验证方法
息通 道 等描述 的 待验证 系统 ，以及 以 Ｌ Ｔ Ｌ或
断言 描 述 的待验 证属 性 ，作 为 输人 ，然后 把 种系统描述语言。它是用来对有 限状态 系统进 Ｐ ｒ ｏ ｍ ｅ ｌ ａ 描述 的待验证 系统 中每个 进程转 化为 行建模 的形 式描述 语言 ．由于 Ｐ ｒ ｏ ｍｅ ｌ ａ 提供对
此 为 了确保 信 息安 全 ，人 们设 计 出 了安全 协
议来保证 通信过程的安全可靠 。安全 协议 是一
个分布 式算法 ，它规定 了两个或两个 以上 的协
议主体在一 次通 信过程 中必须要执行 的一 系列
步骤 。利用安全 协议 人们来实现在开发 网络 中 ห้องสมุดไป่ตู้
的安全通信 。可 以说 安全协议是信息安全 的基 础 ，其 自身的安全 问题 已成 为安全研究的重要
一
内容。 目前 ，在安全协议验 证领域存在多种验
证 方法如模拟 、形式化 等，模 拟的方法存在不
个有 限自动机并对这些有 限 自动 机进 行异步
数据结构与 ｃ代码嵌 入方面的支持 ，可 以很好
积运 算得 到 优先 自动机 Ａ， 同时把 Ｌ Ｔ Ｌ表 达 地 形式化描述 协议 ．一个 Ｐ ｒ ｏ ｍｅ ｌ ａ （ ｐ ｒ ｏ ｃ ｅ ｓ ｓ ｍｅ ｔ ａ 式取反并转换为一个 自动机 Ｂ ，最后对 自动机 ｌ ａ ｎ ｇ ｕ ａ ｇ ｅ ） Ａ 和 自动机 Ｂ进行 同步积运算得到 自动机 Ｃ 。
１引言
期望的性质描述。如果不满足则返 回错误 并提 只在乎事件发生的先后顺序 ，不在乎事件发生 供导 致错误 的状态迁移路径 ，我们将通过错误 的时 间间 隔。每一 个 Ｌ Ｔ Ｌ公 式都可 以表 达为
随着 计 算机 技术 的 发展 ，人类 进人 了信 路径来 定位错 误。本文详细介绍 了模型检测工 的方方面面 ，然而信息在开 放的网络环境 中传
基于HCPN模型检测方法的DNP3-SA协议形式化安全评估与改进
基于HCPN模型检测方法的DNP3-SA协议形式化安全评估与改进基于HCPN模型检测方法的DNP3-SA协议形式化安全评估与改进摘要：DNP3-SA（Distributed Network Protocol 3 - Secure Authentication）协议是一种广泛应用于远程监控与控制系统的通讯协议，该协议的安全性一直备受关注。
本文基于HCPN模型（High Coloured Petri Nets）检测方法，对DNP3-SA协议进行了形式化的安全评估与改进。
通过建立HCPN 模型，分析了DNP3-SA协议的安全性问题，并通过模型检测技术发现了协议的一些潜在安全漏洞。
针对这些安全漏洞，提出了相应的改进策略，以提升DNP3-SA协议的安全性。
实验结果表明，所提出的改进策略能够有效地解决已发现的安全漏洞，并在一定程度上提高了协议的安全性。
1. 引言DNP3-SA协议作为一种常用的通讯协议，主要应用于电力系统、水利系统等远程监控与控制系统中。
然而，随着网络攻击威胁的不断增加，DNP3-SA协议的安全性问题日益突出。
因此，对DNP3-SA协议进行形式化的安全评估与改进具有重要的实际意义。
2. HCPN模型与DNP3-SA协议的建模为了对DNP3-SA协议进行形式化安全评估，我们选择了HCPN模型来描述该协议的行为。
HCPN模型具备对系统并发性和非确定性行为进行描述的能力，适用于建模复杂的协议系统。
我们通过将DNP3-SA协议的行为抽象为一组变迁、库所和弧，建立了HCPN模型。
该模型包括了协议的数据交换过程、身份认证阶段和密钥协商等重要环节，并考虑了协议中的并发与时序行为。
3. 安全性分析与模型检测在完成HCPN模型的建模之后，我们对DNP3-SA协议进行了安全性分析。
通过模型检测技术，我们发现了协议中的一些潜在安全漏洞，如信息泄漏、重放攻击等。
这些安全漏洞可能导致协议的机密性、完整性和可用性受到威胁。
一种安全协议自动化分析方法
安全协议是 以密码学为基础的协议 ， 它在 网络 和分 布式 系 统 中提供各种各样的安全 服务 ， 有着广泛 的应用 ， 信息 系统 在 安全 中占据重要 的位置 。 自动化 ’ 析方法 是协 议形 式化 分 分 析 领 域 中一 个 重 要 的 研 究 方 向 ， 目前 安 全 协 议 的 自动 化 分 析
ｍａ ｅ ｓｃ ｉ ｏｔｃ ｌａ ａｙ ｉ ｒ ｉ ｐｅ ａ ｄ ｉ ｔ ｉｉｅ． ｈｅｍｏｄ ｌｉ ｅ ｎｔｄ ｉｓｆ ｃｉ ｎ ｂ ｏ ｎｇｉ Ｅｃｉ ｓ ｎ ｉｏ ｄ ｅ ｕｒｔ ｐｒ ｏ ｏ ｎ ｌｓｓｍｏ ｅ ｓｍ ｌ ｎ ｎ ｕｔｖ Ｔ ｙ ｅ ｍｐｌｍｅ ｅ ｔ ｕｎ ｔｏ ｙ ｃ ｄｉ ｎ Ｍｙ ｌｐ ｅ ｅ ｖｒ ｎ—
．
Ｋｉ ｄ ｏ ｕ ｏ ｔ ｄ ａ ａ ｙ ｉ ｔ ｏ ｆｓ ｃ ｒｔ ｒ ｔ ｃ ｌ ｎ ｆａ ｔ ｍａ ｅ ｎ ｌ ｓｓ ｍｅ ｈ ｄ ｏ ｅ ｕ ｉ ｐ ｏｏ ｏ ｙ
ｗｕ Ｘａ—ｉｇ Ｚ Ｕ Ｑｎ— ｉ ｉ ｙｎ ． ＨＯ ｉｇｌ ｏ ｅ
（ ｏｅｅｏ ｎｏｍ ｔ ｎＥ ｇｎｅ ｎ Ｚ ｅｇｈｕＵ ｉ ｒｔ， ｈｎｚｏ ５０ １ Ｃ ｉａ Ｃ ｌｇ ｆｒ ａｉ ｎ ｉｅｒ ｇ， ｈｎ ｚｏ ｎｖ ｓｙ Ｚ ｅｇｈｕ４ ０ ０ ， ｈｎ ） ｌ ｆＩ ｏ ｉ ｅｉ
第２ ７卷 第 ６期
２１ ０ ０年 ６月
计 算 机 应 用 研 究
Ａｐ ｌ ａ ｉｎ Ｒｅ ｅ ｒ ｈ ｏ ｏ ｕ ｅ ｓ ｐ ｉ ｔ ｓ ａ ｃ ｆＣ ｍｐ ｔ ｒ ｃ ｏ
Ｖｏ ． ７ Ｎｏ ６ １２ ．
Ｊｎ ２ ０ ｕ ． ０１
一
种 安 Ａｂｓｒ ｔ： Ｔｈｉ ｐｅ ｒ ｓ ｎ ｅ ｎ ａ ｏ ｔｄ ａ ａｙ ｉ ｏ ｌｂａ ｅ ｎ ｓｒ ｎ ｐ ｃ ｆｓ ｃ ｉｔ ｏｏ ｏ． Ｔｈｅ ｍｏ ｅ ｃ ｅ ｅ ｔ ａｃ ｓｐａ ｒｐ ｅ ｅ ｔ ｄ ａ ｕｔｍａ ｅ ｎ ｌｓｓｍ ｄｅ ｓ ｄ ｏ ｔａ ｄ ｓ ａ ｅ ｏ ｅ ｕｒ ｙ ｐｒ ｔｃ １ ｄ ｌａ ｈｉｖ ｄ
安全协议UML模型的SPIN分析
安全协议UML模型的SPIN分析在信息系统中，安全协议起着至关重要的作用，用于确保系统在通信过程中的安全性和保密性。
为了评估安全协议的正确性和可靠性，我们可以使用SPIN（The Simple Promela Interpreter）工具进行形式化验证。
本文将探讨安全协议UML模型的SPIN分析方法。
一、安全协议UML模型概述安全协议UML模型是一种使用UML（Unified Modeling Language）建模的安全协议表示方法。
通过使用UML建模，我们可以清晰地描述安全协议中的各种实体、消息和交互方式。
这种模型旨在提供一种可视化的方式来展示安全协议的运行过程和通信流程。
二、SPIN分析介绍SPIN是一种用于模型检查和形式验证的工具，它基于Promela （Process Meta Language）语言。
Promela是一种基于通信序列进程的描述语言，用于描述并发系统行为。
SPIN可以使用Promela模型对系统进行形式化的验证，并自动地检查系统中是否存在安全性问题。
三、安全协议UML模型的形式化描述在进行SPIN分析之前，我们需要将安全协议UML模型进行形式化描述。
这可以通过将UML模型转换为Promela代码来实现。
在转换过程中，我们需要定义系统中的进程、通信方式和协议规则等。
首先，我们需要为系统中的各个实体定义对应的进程。
每个进程可以表示一个参与协议的角色，例如发送方、接收方和中间人等。
进程之间通过消息进行通信，我们需要定义消息的格式和传输方式。
然后，我们需要定义系统中的安全协议规则。
协议规则描述了各个参与方之间的交互方式和消息处理过程。
我们需要确保协议规则的正确性和安全性，例如防止信息泄露和身份伪造等。
最后，我们将所有的定义转换为Promela代码，并使用SPIN工具进行形式化验证。
四、SPIN分析的步骤进行SPIN分析的步骤如下：1. 将安全协议UML模型转换为Promela代码。
一个可抵抗临时指数泄露的密钥协商协议形式化安全模型
ｃ ｕ ｒ ｉ ｔ ｙ ｏ ｆ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ｔ ｏ ＤＤＨ ａ ｓ ｓ ｍ ｐ ｕ ｔ ｉ ｏ ｎ ｔ ｉ ｇ ｈ ｔ ｌ ｙ ． Ａｃ ｔ ｕ ａ ｌ ｌ ｙ。 ｄ ｅ ｓ ｉ ｇ ｎ ｉ ｎ ｇ ａ ｓ ｅ ｃ ｕ ｒ ｅ ｋ ｅ ｙ ａ ｇ ｒ ｅ ｅ ｍｅ ｎ ｔ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ｉ ｎ ｗｈ ｉ ｃ ｈ ｅ ｐ ｈ ｅ ｍｅ ｒ ａ ｌ
ｈ ｉ ｄ ｄ ｅ ｎ ｔ ｒ ｏ ｕ ｂ ｌ ｅ ａ ｎ ｄ ｂ ｕ ｉ ｌ ｔ ａ ｎ ｅ ｗ ｆ ｏ ｒ ｍａ ｌ ｓ ｅ ｃ ｕ ｒ ｉ ｔ ｙ ｍｏ ｄ ｅ ｌ ｉ ｎ ｗｈ ｉ ｃ ｈ ａ ｍｕ ｃ ｈ ｓ ｔ ｒ ｏ ｎ ｇ ｅ ｒ ａ ｄ ｖ ｅ ｒ ｓ ａ ｒ ｙ ｃ ａ ｎ ｂ ｅ ｒ ｅ ｓ ｉ ｓ ｔ ｅ ｄ ａ ｎ ｄ ａ ｌ Ｓ Ｏ ａ ｎ ｅ ｗ
ｎ ｅ ｗ ｍｏ ｄ ｅ １ ． Ｔｈ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ １ ｍｏ ｄ ｉ ｆ ｉ ｅ ｓ ｔ ｈ ｅ ｇ ｅ ｎ ｅ ｒ ａ ｔ ｉ ｏ ｎ ｆ ｕ ｎ ｃ ｔ ｉ ｏ ｎ ｏ ｆ ｅ ｉ ｎ ａ ｎ ａ ｔ ｕ ｒ ａ ｌ ｗａ ｙ ａ ｎ ｄ ｍａ ｋ ｅ ｓ ｉ ｔ ｉ ｒ ｅ —
ｄ ｕ ｃ ｅ ｓ ｔ ｈ ｅ ｔ ｉ ｍｅ ｓ ｏ ｆ ＨＡＳ Ｈ ａ ｎ ｄ ａ ｌ ｓ ｏ ｔ ｈ ｅ ｒ ｅ ｆ ｌ ｅ ｃ ｔ ａ ｔ ｔ ａ ｃ ｋ ｃ ａ ｎ ｂ ｅ ａ ｖ ｏ ｉ ｄ ｅ ｄ ． Ｉ ｎ ｏ ｒ ｄ ｅ ｒ ｔ ｏ ｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅ ｓ ｅ ｃ ｕ ｒ ｉ ｔ ｙ ｏ ｆ ＨＣＭＱＶ， ｗｅ ｄ ｉ ｄ ｎ ｏ ｔ ｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅ ｕ ｎ ｆ ｏ ｒ ｇ ｅ ａ ｂ ｉ ｌ ｉ ｔ ｙ ｆ ｏ ｒ ｔ ｈ ｅ ｓ ｉ ｇ ｎ ａ ｔ ｕ ｒ ｅ ｓ ｃ ｈ ｅ ｍｅ ｌ ｉ ｋ ｅ ＨＭＱＶ， ｂ ｕ ｔ ａ ｄ ｉ ｓ ｔ ｉ ｎ ｇ ｕ ｉ ｓ ｈ ｅ ｒ ｗａ ｓ ｃ ｏ ｎ ｓ ｔ ｒ ｕ ｃ ｔ ｅ ｄ ｔ ｏ ｒ ｅ ｄ ｕ ｃ ｅ ｔ ｈ ｅ ｓ ｅ —
ｈ ｉ ｄ ｄ ｅ ｎ ｔ ｒ ｏ ｕ ｂ ｌ ｅ ａ ｎ ｄ ｂ ｕ ｉ ｌ ｔ ａ ｎ ｅ ｗ ｆ ｏ ｒ ｍａ ｌ ｓ ｅ ｃ ｕ ｒ ｉ ｔ ｙ ｍｏ ｄ ｅ ｌ ｉ ｎ ｗｈ ｉ ｃ ｈ ａ ｍｕ ｃ ｈ ｓ ｔ ｒ ｏ ｎ ｇ ｅ ｒ ａ ｄ ｖ ｅ ｒ ｓ ａ ｒ ｙ ｃ ａ ｎ ｂ ｅ ｒ ｅ ｓ ｉ ｓ ｔ ｅ ｄ ａ ｎ ｄ ａ ｌ Ｓ Ｏ ａ ｎ ｅ ｗ
ｎ ｅ ｗ ｍｏ ｄ ｅ １ ． Ｔｈ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ １ ｍｏ ｄ ｉ ｆ ｉ ｅ ｓ ｔ ｈ ｅ ｇ ｅ ｎ ｅ ｒ ａ ｔ ｉ ｏ ｎ ｆ ｕ ｎ ｃ ｔ ｉ ｏ ｎ ｏ ｆ ｅ ｉ ｎ ａ ｎ ａ ｔ ｕ ｒ ａ ｌ ｗａ ｙ ａ ｎ ｄ ｍａ ｋ ｅ ｓ ｉ ｔ ｉ ｒ ｅ —
ｄ ｕ ｃ ｅ ｓ ｔ ｈ ｅ ｔ ｉ ｍｅ ｓ ｏ ｆ ＨＡＳ Ｈ ａ ｎ ｄ ａ ｌ ｓ ｏ ｔ ｈ ｅ ｒ ｅ ｆ ｌ ｅ ｃ ｔ ａ ｔ ｔ ａ ｃ ｋ ｃ ａ ｎ ｂ ｅ ａ ｖ ｏ ｉ ｄ ｅ ｄ ． Ｉ ｎ ｏ ｒ ｄ ｅ ｒ ｔ ｏ ｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅ ｓ ｅ ｃ ｕ ｒ ｉ ｔ ｙ ｏ ｆ ＨＣＭＱＶ， ｗｅ ｄ ｉ ｄ ｎ ｏ ｔ ｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅ ｕ ｎ ｆ ｏ ｒ ｇ ｅ ａ ｂ ｉ ｌ ｉ ｔ ｙ ｆ ｏ ｒ ｔ ｈ ｅ ｓ ｉ ｇ ｎ ａ ｔ ｕ ｒ ｅ ｓ ｃ ｈ ｅ ｍｅ ｌ ｉ ｋ ｅ ＨＭＱＶ， ｂ ｕ ｔ ａ ｄ ｉ ｓ ｔ ｉ ｎ ｇ ｕ ｉ ｓ ｈ ｅ ｒ ｗａ ｓ ｃ ｏ ｎ ｓ ｔ ｒ ｕ ｃ ｔ ｅ ｄ ｔ ｏ ｒ ｅ ｄ ｕ ｃ ｅ ｔ ｈ ｅ ｓ ｅ —
《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》
• 现有的安全协议形式化分析技术主要有四种： – 逻辑方法：采用基于信仰和知识逻辑的形式分析方法，比如以 BAN逻辑为代表的类BAN逻辑 – 通用形式化分析方法：采用一些通用的形式分析方法来分析安全 协议，例如应用Petri网等 – 模型检测方法：基于代数方法构造一个运行协议的有限状态系统 模型，再利用状态检测工具来分析安全协议 – 定理证明方法：将密码协议的安全行作为定理来证明，这是一个 新的研究热点
P believe k P, P saw{X}k P 定义了主体在协议运行中对消息的获取 • 规则5
R5 : P | kQ, P{X}kQ1 PX
为各种协议形式化分析方法形成统一的形式语言表述以描述可利用的必要信息并使之能够应用于一些新的应用协议的分析中将形式化方法应用于协议说明和协议涉及阶段使之不仅仅用于分析具体的某个安全协议的安全性从而可以极小的代价尽可能早地发现错误类ban逻辑形式化分析ban逻辑形式化首先需要进行理想化即将协议的消息转换为ban逻辑中的公式再由逻辑的推理规则根据理想化协议和假设进行推理推断协议能否完成预期的目标类ban逻辑形式化分析ban逻辑形式化加密系统是完善的只有知道密钥的主体才能解读密文消息任何不知道密钥的主体都不能解读密文消息也没有办法根据密文推导密钥密文含有足够的冗余消息解密者可以根据解密的结果来判断他是否已经正确解密消息中有足够的冗余消息使得主体可以判断该消息是否来源于自身ban逻辑还假设协议的参与主体是诚实的类ban逻辑形式化分析ban逻辑形式化依照ban逻辑的惯例pqr等表示主体变量k表示密钥变量xy表示公式变量
内容提要
1. 安全协议存在安全缺陷 2. 安全协议形式化分析 3. 类BAN逻辑形式化分析 4. 例子：对NSSK认证协议的BAN逻辑分析
类BAN逻辑形式化分析——BAN逻辑形式化
P believe k P, P saw{X}k P 定义了主体在协议运行中对消息的获取 • 规则5
R5 : P | kQ, P{X}kQ1 PX
为各种协议形式化分析方法形成统一的形式语言表述以描述可利用的必要信息并使之能够应用于一些新的应用协议的分析中将形式化方法应用于协议说明和协议涉及阶段使之不仅仅用于分析具体的某个安全协议的安全性从而可以极小的代价尽可能早地发现错误类ban逻辑形式化分析ban逻辑形式化首先需要进行理想化即将协议的消息转换为ban逻辑中的公式再由逻辑的推理规则根据理想化协议和假设进行推理推断协议能否完成预期的目标类ban逻辑形式化分析ban逻辑形式化加密系统是完善的只有知道密钥的主体才能解读密文消息任何不知道密钥的主体都不能解读密文消息也没有办法根据密文推导密钥密文含有足够的冗余消息解密者可以根据解密的结果来判断他是否已经正确解密消息中有足够的冗余消息使得主体可以判断该消息是否来源于自身ban逻辑还假设协议的参与主体是诚实的类ban逻辑形式化分析ban逻辑形式化依照ban逻辑的惯例pqr等表示主体变量k表示密钥变量xy表示公式变量
内容提要
1. 安全协议存在安全缺陷 2. 安全协议形式化分析 3. 类BAN逻辑形式化分析 4. 例子：对NSSK认证协议的BAN逻辑分析
类BAN逻辑形式化分析——BAN逻辑形式化
一种安全协议的形式化设计方法
Ｋｅ ｗｏ ｄ ：ｓ ｃ ｒ ｙ ｐ ｏｏ ｏ ， ｅ ｒ ｍ ｐ ｏ ｅ ｒ ｄ ｎ ａ ｃ ｒ ｔｃ ｌ ｒ ｄ ｃｉ ｎ ｙ ｒ ｓ ｅ ｕ ｔ ｒ ｔｃ ｌ ｔ ｏ ｅ ｒｖ ｎ，ｅ ｕ ｄ ｎ ｙ ｐ ｏｏ ｏ ，ｅ ｕ ｔ ｉ ｈ ｏ
１ 概 述
网络 的飞 速 发 展使 得 安 全协 议 得 到 大 规 模 应用 ， 别 是 在 特 电 子 商 务 、 子 政 务 的 应 用 中 ， 全 协 议 为 数 据 的 安全 提 供 了 电 安
的 发 展 增加 设 计 规 则和 约 简规 则 。
关 键 词 安 全 协 议 定 理 证 明 冗 余 协议 约 简
文 章 编号 １０ — ３ １ （ｏ６ １－ ０ １ ０ 文 献 标 识 码 Ａ 中图 分 类 号 Ｔ ３９ ０ ２ ８ ３ 一 ２ ｏ ） １０ ２ － ３ Ｐ ０
Ｔ ｅ ｍｅｈ ｄ ｃ ｎ ｒａｉｅ ａ ｔ－ ｅ ｉｎ ｏ ｅ ｕｉ ｒｔｃ ｌａ ｄ ｈ ｓｇ ｏ ｘｅ ｓｏ ｏ ｅｉｎ ｒｌｓａ ｄ ｒｄ ｃｉｎ ｒｌｓ ｈ ｔｏ ａ ｅ ｌ ｕｏ ｄ ｓｇ ｆｓｃ ｒ ｙ ｐ ｏｏ ｏ ｎ ａ ｏ ｄ ｅｔｎ ｉｎ ｆｒｄ ｓｇ ｕｅ ｎ ｅ ｕ ｔ ｕｅ． ｚ ｔ ｏ
（ｃ ｏｌｏ ｏ ｐ ｔｒＷｕ ａ ｎｖｒｉ ， ｈ ｎ ４ ０ ７ ） Ｓ ｈ ｏ ｆＣ ｍ ｕｅ ， ｈ ｎ Ｕ ｉｅｓ ｙ Ｗｕ ａ ３ ０ ２ ｔ
Ａｂ ｔ ａ ｔ Ｔ ｉ ａ ｅ ｒ ｐ ｓ ｓ ｎ ｗ ｓｒ ｃ ： ｈ ｓ ｐ ｐ ｒ ｐ ｏ ｏ ｅ ａ ｅ ｍｅｈ ｄ ｏ ｓ ｃ ｒｔ ｐ ｏｏ ｏ ｄ ｓｇ ｕ ｉｇ ｈ ｏｅ ｐ ｏ ｅ ａ ｄ ｅ ｕ ｔ ｒ ｔｃ ｌ ｔ ｏ ｆ ｅ ｕ ｙ ｒ ｔｃ ｌ ｅ ｉｎ ｓｎ ｔ ｅ ｒ ｍ ｒ ｖ ｎ ｎ ｓ ｃ ｒ ｙ ｐ ｏｏ ｏ ｉ ｉ
１ 概 述
网络 的飞 速 发 展使 得 安 全协 议 得 到 大 规 模 应用 ， 别 是 在 特 电 子 商 务 、 子 政 务 的 应 用 中 ， 全 协 议 为 数 据 的 安全 提 供 了 电 安
的 发 展 增加 设 计 规 则和 约 简规 则 。
关 键 词 安 全 协 议 定 理 证 明 冗 余 协议 约 简
文 章 编号 １０ — ３ １ （ｏ６ １－ ０ １ ０ 文 献 标 识 码 Ａ 中图 分 类 号 Ｔ ３９ ０ ２ ８ ３ 一 ２ ｏ ） １０ ２ － ３ Ｐ ０
Ｔ ｅ ｍｅｈ ｄ ｃ ｎ ｒａｉｅ ａ ｔ－ ｅ ｉｎ ｏ ｅ ｕｉ ｒｔｃ ｌａ ｄ ｈ ｓｇ ｏ ｘｅ ｓｏ ｏ ｅｉｎ ｒｌｓａ ｄ ｒｄ ｃｉｎ ｒｌｓ ｈ ｔｏ ａ ｅ ｌ ｕｏ ｄ ｓｇ ｆｓｃ ｒ ｙ ｐ ｏｏ ｏ ｎ ａ ｏ ｄ ｅｔｎ ｉｎ ｆｒｄ ｓｇ ｕｅ ｎ ｅ ｕ ｔ ｕｅ． ｚ ｔ ｏ
（ｃ ｏｌｏ ｏ ｐ ｔｒＷｕ ａ ｎｖｒｉ ， ｈ ｎ ４ ０ ７ ） Ｓ ｈ ｏ ｆＣ ｍ ｕｅ ， ｈ ｎ Ｕ ｉｅｓ ｙ Ｗｕ ａ ３ ０ ２ ｔ
Ａｂ ｔ ａ ｔ Ｔ ｉ ａ ｅ ｒ ｐ ｓ ｓ ｎ ｗ ｓｒ ｃ ： ｈ ｓ ｐ ｐ ｒ ｐ ｏ ｏ ｅ ａ ｅ ｍｅｈ ｄ ｏ ｓ ｃ ｒｔ ｐ ｏｏ ｏ ｄ ｓｇ ｕ ｉｇ ｈ ｏｅ ｐ ｏ ｅ ａ ｄ ｅ ｕ ｔ ｒ ｔｃ ｌ ｔ ｏ ｆ ｅ ｕ ｙ ｒ ｔｃ ｌ ｅ ｉｎ ｓｎ ｔ ｅ ｒ ｍ ｒ ｖ ｎ ｎ ｓ ｃ ｒ ｙ ｐ ｏｏ ｏ ｉ ｉ
一种混合的安全协议分析方法
化 ， 立统 一 的调 和 方 法框 架 对 安 全 协 议进 行 分 析 是 研 究的 热 点和 难 点 。通 过 对 两种 观 点 的研 究 ， 照 优 势 互 补 的 原 则 将 两 者 相 调 建 按
和 ， 出 了一种 新 的 形 式 化分 析 方 法 ， 方法 可提 供 更 为 完全 的 安全 协 议 形 式 化 分 析 。 提 该 关 键 词 可证安全 逻 辑 分 析 安 全 协 议 混 合 分 析
ａｔ ｃｉｅａ ｄ ｄｆ ｃ ｌ ｆｒｒｓａｃ ｅｓｔ ｕｌ ｎｆｒ ｈ ｒ ｎｏ ｓｍｅｈ ｄｆａ ｗ ｒ ｏａ ａｙｅｓ ｃ ｒｙ ｐｏｏｏｓ ｅ ｏｍａ ｎ ｌｓｓ ｔａ ｔ ｎ ｉ ｕｔ ｏ ｅｅ ｒｈ ｒ ｏｂ ｉ ａｕ ｉ ｍ ａｍｏ ｉｕ ｔｏ ｒｍｅ ｏｋ ｔ ｎ ｌｓ ｅ ｕｉ ｒｔｃ ｌ．Ａ ｎ ｗ ｆｒ ｌａ ａｙ ｉ ｒ ｖ ｉ ｆ ｄ ｏ ｔ
Ａ Ｉ Ｍ ＸＥＤ ＳＥＣＵＲＩ ＴＹ ＰＲｏＴｏ ＣｏＬ ＡＮＡＬＹＳ Ｓ Ｍ ＥＴＨ ｏＤ Ｉ
Ｈｕ ｎ ｆ ｉ ｏ Ｔｇ Ｆａ ｎ ｎ
（ ｒｄａｅＰｏｅ ｉｎｌＴａｎｎ ｅｔ ，ｏ ｅｅｏ ｎｏｍ ｔ ｎＥ ｇｎｅｉ Ｂｉｎ ０ ０ ４ Ｃ ｉ Ｇａ ｕｔ ｒ ｓｏａ ｒｉｉｇＣ ｎｒ Ｃ ｌｇ ｆ ｒａｉ ｎｉｅｒ ｇ，ｅｉｇ１０ ９ ， ｈｎ ｆｓ ｅ ｌ ｆＩ ｏ ｎ ｊ ａ） （ ｏｅｅｏ ｎｏｍ ｔ ｎＥ ｇｎｅｉ Ｉ ｏｍａｉｎＥ ｇｎｅｉｇＵ ｉ ｒｔ，ｈｎｚｏ ５０ ２， ｅａ Ｃ ｉａ Ｃ ｌｇ ｆｒ ａｉ ｎ ｉ ｒ ｇ，ｆ ｒ ｔ ｎ ｉ ｒ ｎｖ ｓｙＺ ｅｇｈ ｕ４ ００ Ｈ ｎｎ，ｈｎ ） ｌ ｆＩ ｏ ｅ ｎ ｎ ｏ ｅ ｎ ｅｉ
议中可能存在 的缺 陷却 是一项非 常困难的工作。现有的两种重 要 的分析方法 为： 一种是基于知识与信念推理 的模态逻辑方法 ；
一种安全协议的形式化分析方法
ｙ ：参 与 协议 的主 体 。
Ｘ ： 与 ｙ之问共享对称密钥 。 Ｙ
Ｍ ：Ｍ 是 新 鲜 的。
（ ：用 与 ｙ共享 的对称密钥加密 的消息 ） ［ ｒ ：主体 相信 。
Ｉ Ｉ ｘ：主 体 控 制 Ｍ。 （ ） ：主 体 曾发 送过 。 ４－ ４ ：被 使 用 过 的条 件 。
第３ ６卷 第 ７期
ＶＬ ｏ ３６
・
计
算
机
工
程
‘
２１ ００年 ４月
Ａｐｒｌ ０１ ｉ ２ ０
Ｎｏ７ ．
Ｃｏ ｐｕ ｅ ｍ ｔ ｒＥｎｇ ｎｅ ｒｎｇ ｉ ｅｉ
软 件技术 与数据 库 ・
一
文章编号：１０＿ ４８０ｏ ７＿８ ＿ 文献 ０ｍ－ ２（ １０—０ ２ ｏ ３ ２ ） ０— ２ 标识码： Ａ
［ ｓｒｃ］ Ｔ ｉ ｐｐｒｒｓａｃ ｅ ｎ ｑ ｉ ｎ ｆ ｃ ｎ ｏｍａ ａ ａ ｓｓｏ ｅｕｉ ｒｔｃ ｌ ｎ ｒｓｎｓｔｅ ｃｎ ｅｔｏ ｕ ｔｄ ｍａｎ Ａｂｔａ ｔ ｈｓ ａｅ ｅｅｒｈｓ ｏ ｕｃ ａ ｄ ｅｆ ｉ ｔｆｒ ｌ ｎｌ ｉ ｆｓｃｒｔ ｐｏｏｏ，ａ ｄ ｐｅｅｔ ｈ ｏ ｃｐ ｆｔ ｓ ｏ ｉ． ｋ ｉｅ ｙ ｙ ｒ
过程清晰、直观 。 方法直接分析协议参与主体的信任域，简化 分析过程和步骤。实验结果表 明， 该 与传统方法相比 ， 该方法更快速、直观 ，
并能为分析协议的冗余性提供具体方法和依据。
关健诃 ： 式化分析 ；安全协议 ；Ｂ Ｎ逻辑 ； Ｓ Ｋ协议 形 Ａ Ｎ Ｓ
Ｆｏ ｍ ａ ｒ ｌ Ａｎａ ｙ ｉ ｅ ｈ ｄ ０ ｃ ｉ Ｐｒ ｔ ｃ ｌ ｌ ｓｓＭ ｔ ｏ ｆＳｅ ｕｒｔ ｙ ｏ ｏ ｏ
的误判 ，与 事实不符 。文 献【］ Ｊ ６中在构造类别代数的基础上
Ｘ ： 与 ｙ之问共享对称密钥 。 Ｙ
Ｍ ：Ｍ 是 新 鲜 的。
（ ：用 与 ｙ共享 的对称密钥加密 的消息 ） ［ ｒ ：主体 相信 。
Ｉ Ｉ ｘ：主 体 控 制 Ｍ。 （ ） ：主 体 曾发 送过 。 ４－ ４ ：被 使 用 过 的条 件 。
第３ ６卷 第 ７期
ＶＬ ｏ ３６
・
计
算
机
工
程
‘
２１ ００年 ４月
Ａｐｒｌ ０１ ｉ ２ ０
Ｎｏ７ ．
Ｃｏ ｐｕ ｅ ｍ ｔ ｒＥｎｇ ｎｅ ｒｎｇ ｉ ｅｉ
软 件技术 与数据 库 ・
一
文章编号：１０＿ ４８０ｏ ７＿８ ＿ 文献 ０ｍ－ ２（ １０—０ ２ ｏ ３ ２ ） ０— ２ 标识码： Ａ
［ ｓｒｃ］ Ｔ ｉ ｐｐｒｒｓａｃ ｅ ｎ ｑ ｉ ｎ ｆ ｃ ｎ ｏｍａ ａ ａ ｓｓｏ ｅｕｉ ｒｔｃ ｌ ｎ ｒｓｎｓｔｅ ｃｎ ｅｔｏ ｕ ｔｄ ｍａｎ Ａｂｔａ ｔ ｈｓ ａｅ ｅｅｒｈｓ ｏ ｕｃ ａ ｄ ｅｆ ｉ ｔｆｒ ｌ ｎｌ ｉ ｆｓｃｒｔ ｐｏｏｏ，ａ ｄ ｐｅｅｔ ｈ ｏ ｃｐ ｆｔ ｓ ｏ ｉ． ｋ ｉｅ ｙ ｙ ｒ
过程清晰、直观 。 方法直接分析协议参与主体的信任域，简化 分析过程和步骤。实验结果表 明， 该 与传统方法相比 ， 该方法更快速、直观 ，
并能为分析协议的冗余性提供具体方法和依据。
关健诃 ： 式化分析 ；安全协议 ；Ｂ Ｎ逻辑 ； Ｓ Ｋ协议 形 Ａ Ｎ Ｓ
Ｆｏ ｍ ａ ｒ ｌ Ａｎａ ｙ ｉ ｅ ｈ ｄ ０ ｃ ｉ Ｐｒ ｔ ｃ ｌ ｌ ｓｓＭ ｔ ｏ ｆＳｅ ｕｒｔ ｙ ｏ ｏ ｏ
的误判 ，与 事实不符 。文 献【］ Ｊ ６中在构造类别代数的基础上
一种形式化分析安全协议的新模型
者 串 空 间模 型 ． 时利 用 此 入 侵 者 串空 间 模 型 分 析 了该 协议 存 在 的缺 陷 ． 明 了 改进 后 的 Ｗｏ＊ ａ 协 同 说 ｏＬ ｍ 议 可克 服 此 缺 陷． 现 有 安 全 协 议 形 式 化 分 析 方 法 相 比 较 ． 空 间模 型 不 仅 具 有 简 洁 直 观 的优 点 ， 与 串 而且 还 可避 免状 态 空 闯爆 炸 的 问题 ． 关 键 词 ：安 全 协 议 ； 式 化 分 析 Ｉ 空 间模 型 Ｉ 形 串 入侵 者 串
ｅ ｐｌ ｉ ｎ ｐ ｏｂ ｅ ｘ ｏｓｏ ｒ ｌ ｍ．
Ｋｅ ｏ ｄ ： ｓ ｃ ｒｔ ｒ ｔｃ ｌｆ ｒ １ ｎ ｌｓｓ ｓｒ ｎ ｐ ｃ ｏ ｅ ； ｅ ｅ ｒｔ ｒｓｒ ｎ ｙ Ｗ ｒ ｓ ｅ ｕ ｉｙｐ ｏ ｏ ｏ ；ｏ ｍａ ａｙ ｉ ；ｔａ ｄ ｓ ａ ｅｍ ｄ ｌ ｐ ｎ ｔａ ｏ ｔａ ｄ ａ
中图 分 类 号 ： Ｐ ０ ３９ Ｆ
文献 标 识 码 ： Ａ
文 章编 号 ：０ １２ ０ （０ ６ ０ ３ １ ５ １０ —４ ０ ２０ ３０ ８ — Ｊ ０
Ａ ｗ ｄ ｌｆ ｒ ａ ａ ｙ ｉ ｇ ｓ ｃ ｒ ｔ ｏ ｏ ｏ ｓ ｆ ｒ ａ ｌ ｎｅ ｍｏ ｅ ｏ ｎ ｌ ｚ ｎ ｌ ｉ ｎｊ Ｔ
（ ｃ ｏ ｌ ｆＣｏ ｐ ｔ ｒＳｃｅ ｃ ｎ ｃ ｎ ｌ ｇ Ｓ ｈ ｏ ｍ ｕ ｅ ｉ ｎ ｅ ａ ｄ Ｔｅ ｈ ｏ ｏ ｙ，Ｘｉ ｉ ｎ Ｕ ｎ ｖ ｏ ｄ ａ ｉ ．，Ｘｉ ｎ ７ ０ ７ ，Ｃｈ ｎ ） １０ １ ａ ｉａ
ｏ ｅ ｃ ｍｅ ｉ ｈ ｍｐ ｏ ｅ ｏ — ｍ ｒ ｔ ｃ １ Ｔｈ ｔ ａ ｄ ｓ ａ ｅ ｍｏ ｅ ｉ ｃ ｓ ｅ ｂ ｖ ｖ ｒ ｏ ｎ ｔ ｅ ｉ ｒ ｖ ｄ Ｗ ｏ Ｌａ ｐ ｏ ｏ ｏ ． ｅ ｓ ｒ ｎ ｐ ｃ ｄ ｌｄ ｓ ｕ ｓ ｄ ａ ｏ ｅ ｉ ｄ ｓ ｉ ｇ ｉｈ ｄ ｒ ｍ ｏ ｈ ｒ ｍ ｏ ｅ ｓ ｙ ｉｓ ｉ ｐ ｉｉｙ ａ ｄ ａ ｖ ｉ ｔ ｅ ｔ ｔ ｓ ａ ｅ ｓ ｉｔｎ ｕ ｓ ｅ ｆｏ ｔ ｅ ｄｌ ｂ ｔ ｓｍ ｌ ｔ ｎ ｃ ｎ ａ ｏ ｄ ｈ ｓ ａ ｅ ｐ ｃ ｃ
ｅ ｐｌ ｉ ｎ ｐ ｏｂ ｅ ｘ ｏｓｏ ｒ ｌ ｍ．
Ｋｅ ｏ ｄ ： ｓ ｃ ｒｔ ｒ ｔｃ ｌｆ ｒ １ ｎ ｌｓｓ ｓｒ ｎ ｐ ｃ ｏ ｅ ； ｅ ｅ ｒｔ ｒｓｒ ｎ ｙ Ｗ ｒ ｓ ｅ ｕ ｉｙｐ ｏ ｏ ｏ ；ｏ ｍａ ａｙ ｉ ；ｔａ ｄ ｓ ａ ｅｍ ｄ ｌ ｐ ｎ ｔａ ｏ ｔａ ｄ ａ
中图 分 类 号 ： Ｐ ０ ３９ Ｆ
文献 标 识 码 ： Ａ
文 章编 号 ：０ １２ ０ （０ ６ ０ ３ １ ５ １０ —４ ０ ２０ ３０ ８ — Ｊ ０
Ａ ｗ ｄ ｌｆ ｒ ａ ａ ｙ ｉ ｇ ｓ ｃ ｒ ｔ ｏ ｏ ｏ ｓ ｆ ｒ ａ ｌ ｎｅ ｍｏ ｅ ｏ ｎ ｌ ｚ ｎ ｌ ｉ ｎｊ Ｔ
（ ｃ ｏ ｌ ｆＣｏ ｐ ｔ ｒＳｃｅ ｃ ｎ ｃ ｎ ｌ ｇ Ｓ ｈ ｏ ｍ ｕ ｅ ｉ ｎ ｅ ａ ｄ Ｔｅ ｈ ｏ ｏ ｙ，Ｘｉ ｉ ｎ Ｕ ｎ ｖ ｏ ｄ ａ ｉ ．，Ｘｉ ｎ ７ ０ ７ ，Ｃｈ ｎ ） １０ １ ａ ｉａ
ｏ ｅ ｃ ｍｅ ｉ ｈ ｍｐ ｏ ｅ ｏ — ｍ ｒ ｔ ｃ １ Ｔｈ ｔ ａ ｄ ｓ ａ ｅ ｍｏ ｅ ｉ ｃ ｓ ｅ ｂ ｖ ｖ ｒ ｏ ｎ ｔ ｅ ｉ ｒ ｖ ｄ Ｗ ｏ Ｌａ ｐ ｏ ｏ ｏ ． ｅ ｓ ｒ ｎ ｐ ｃ ｄ ｌｄ ｓ ｕ ｓ ｄ ａ ｏ ｅ ｉ ｄ ｓ ｉ ｇ ｉｈ ｄ ｒ ｍ ｏ ｈ ｒ ｍ ｏ ｅ ｓ ｙ ｉｓ ｉ ｐ ｉｉｙ ａ ｄ ａ ｖ ｉ ｔ ｅ ｔ ｔ ｓ ａ ｅ ｓ ｉｔｎ ｕ ｓ ｅ ｆｏ ｔ ｅ ｄｌ ｂ ｔ ｓｍ ｌ ｔ ｎ ｃ ｎ ａ ｏ ｄ ｈ ｓ ａ ｅ ｐ ｃ ｃ
- 1、下载文档前请自行甄别文档内容的完整性，平台不提供额外的编辑、内容补充、找答案等附加服务。
- 2、"仅部分预览"的文档,不可在线预览部分如存在完整性等问题,可反馈申请退款(可完整预览的文档不适用该条件!)。
- 3、如文档侵犯您的权益，请联系客服反馈,我们会尽快为您处理(人工客服工作时间：9:00-18:30)。
)’ 可能存在一些不易发现的安全缺陷 # 有些甚至数年后 才被 发现 & 长期 以 来 # 形式化方法被公认为分析安全 +
协议的有力武器 + 目前分 析 安 全 协 议 的 形 式 化 方 法 主 要 有 $ 该 方 法 基 于 知 识 和 信 念 推 理 的 模 态 逻 辑# 如 ! 推 理 构 造 法#
! " " &年&月 第’ ’卷!第’期
!
西安电子科技大学学报 （自然科学版） ! "#$%& ’!" (!) * + * &%!#% * , -$ . * /0
!
U < A+ ! " " & V 8 + ’ ’!P + ’
一种形式化分析安全协议的新模型
慕建君
! 西安电子科技大学 计算机学院 " 陕西 西安 !% # ) " " % ) 摘要 ! 串空间是安全协议形式化分析的一种新模型 + 利用次序关系的理论证明了借助串空间模型进行 安全协议形式化分析的一个重要结论 + 通过构造 入 侵 者 串 的 方 法 ! 针对 , $ . / 0 协议提出了一个入侵 者串空间模型 ! 同时利用此入侵者串空间模型分 析 了 该 协 议 存 在 的 缺 陷 ! 说明了改进后的 , $ . / 0协 议可克服此缺陷 + 与现有安全协议形式化分析方法 相 比 较 ! 串空间模型不仅具有简洁直观的优点! 而且 还可避免状态空间爆炸的问题 + 关键词 ! 安全协议 " 形式化分析 " 串空间模型 " 入侵者串 中图分类号 ! " # 1 2 ’ " *!! 文献标识码 ! 3!! 文章编号 ! ) " " ) $ ! ( " " ! " " & " ’ $ " ’ 4 ) $ " #
+ 串8 中& & ) 是& ! 的直接前驱 . )* & ! 表示在同一串上 & ) 是& ! 的前驱但不一定是直接前驱 + 0= &) . % 一个无符号项- 出现在结点& $ : 当且仅当- # > ? 0(
源于 ) 结点& $ : 如果0= 的符号为正且-# ! 但对于同一串上 &) 0= &) & 一个无符号项-产生于 ( > ? 0( > ? 0( , 结点 & 的任何前驱& <有 -# 0= & <) . > ? 0( ’ 一个无符号项- 惟一产生的如果- 产生于惟一的结点& $ : . 容易看出 ! 结点集 : 与边& ! ( & ) ’& ! 和& )* ! 的集合一起构成了一个有向图 " & ’+ * )# . ! " $! 束和次序关系 一 个束表示在某一具体情形下一个协议的执行过程 ! 它是有向图 "&! ( 此子图 ’+ * ) # 的有限子图 ! 中的边表示结点之间的因果依赖关系 + 定义 %! 假设 ’= ,’ ! 令 > 2 " :> ! ( ( 其中 :> 表 *= , * . ’= + *=) # 是 " :! ’+ * ) # 的子图 !
&’ ’’ 但K 而不能分析协议的保密性质 & % 该方 K 3P 逻辑 ! 等 # 3P 逻辑只能分析协议的认证性质 # " 攻击构造法 # 法从协议的初始状态开始 # 对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索 # 以期找到协议可能 &’ & #’ 存在的错误 + 这种方法主要有基于模型检测技术的模型检测器 Q 验证语言 M 代数 简化 理论模 R S( ( < ? ! ( & &# %’ 型以及特定专家系统 ! 如特殊目的 PS " # 但这种方法无法解决状态空间爆炸问 . 分 析 器 和T A = > ? ? / = ? C
$ ! 5 0 3 * + 1 3 = ? / A BI / 6 > @ I /A > J0 B > 8 9 ? = 7 > 9 ? 0 / 8 / A / 8 I @ I9 I > 6 < ? @ = ? = 6 8 I + K !5 ; D D; D < I @ A 7 > = 7 > ? 9? B > ? ? > 8 / = @ A# /G > ? 0 ? = / A =6 A 6 8 < I @ A< I > B= -/ A / 8 L >I > 6 < ? @ = C= DD@ ; D D ? = 6 8 I 9 ? 0 / 8 8 @ = 7= 7 >7 > 8 9= 7 >I = ? / A BI / 6 >0 B > 8 @ II 7 J A+K A I = ? < 6 = @ A ; DJ ;; D6 C > A > = ? / = ?I = ? / A B I 9 ? = 7 >, $ . / 0; ? = 6 8J >; ? > I > A = /I = ? / A BI / 6 >0 B > 8 @ A 9 @ 8 = ? / = > B ; ; #J 9 ? = 7 @ I; ? = 6 8 +M ? > G > ? @ = 7= 7 >7 > 8 9= 7 @ II = ? / A BI / 6 > 0 B > 8@ A 9 @ 8 = ? / = > B J > ; ; / A / 8 L > = 7 >9 8 / J@ A= 7 @ I; ? = 6 8/ A B@ 8 8 < I = ? / = >= 7 / == 7 @ I9 8 / J@ A= 7 @ I; ? = 6 86 / AN > D G > ? 6 0 > @ A= 7 > @ 0 ? G > B, $ . / 0; ? = 6 8 +1 7 >I = ? / A BI / 6 >0 B > 8B @ I 6 < I I > B/ N G > ; ; @ IB @ I = @ A < @ I 7 > B9 ? 0= 7 > ?0 B > 8 IN = II @ 0 8 @ 6 @ = A B6 / A/ G @ B= 7 >I = / = >I / 6 > C D@ ; D/ ; > O 8 I @ A; ? N 8 > 0+ ; $ % % % 6 # & * ’ 0 > 6 < ? @ = ? = 6 8 9 ? 0 / 8 / A / 8 I @ I I = ? / A BI / 6 >0 B > 8 > A > = ? / = ?I = ? / A B !I D; D ; ; ,7 安全协议是采用密码技术来保障通信各方之间安全交 换信息 的一个 规则 序 列 # 其目的是在通信各方之 间提供认证或为新的会话分配会话密钥 + 尽管现有的安全协议是安全专家精心设计和详细审核过的 # 但仍然
收稿日期 ! ! " " # $ " # $ ! % 基金项目 ! 国家自然科学基金资助项目 ! " & " # % ’ " ’ ( 作者简介 ! 慕建君 ! " # 男# 副教授 # 博士 + ) * & # $
自然科学版 " ’卷 !!!!!!!!!!! !!!!! 西安电子科技大学学报 ! !!!!!!!!!!! !!!!! 第 ’ ’ 4 !
8! 串空间模型
! " !! 项和子项 * 中的元素称为项 + !! 设 * 表示一个协议中参与者之间可能交换的所有消息的集合 ! 定义 !! 符号项是一个有序对 ""! 其中 % $ *! ! 记一个符号项为 +-或 ,! % #! +! ,& +-表示 "$ % % 发出项’ ( ,- 表示接收到项-. /*) 表示符号项的有限序列的集合 + 设 0 表示原子信息集合 ! 且 0 & 1 23! 通常假设集合 * 是由集合 1 和0 在求逆密钥 1 表示密钥集合 ! 加密 % 4 * 5& 5! 下生成的自由信息空间代数 + 4 和级联运算 5) 定义 #! 设 * 自由信息空间代数 ! 可递归定义为 + 有% # * 上的子项关系 # %’ ! 对所有的% 2- $0!
) ,
有% # ! 则% # % 或 %’ 4 $1) " 对所有 的% 2 4 $1 ! # 若% # $ 若% # 6 或% 2 % 6& 6 $*! 6& 6! 4 ( 4’ ! 则% # 7( 7. %# 7 或% 26 7 $*) 6 $*! 6 ! " #! 串和串空间 串是一个参与者可能参与的事件序列 + 对于合法参与 者 ! 每个 串是接收 和 发 送 的 消 息 序 列 ! 表示该参与 者在一次特定协议执行中的行为以及所有数据项 ( 如 密 钥和临 时值 ) 的特 定值 + 攻击 者 串 是 攻 击 者 可 能 发 送 和接收的消息序列 + 定义 $! 设 * 为自由信息空间代数 ! * 上的一个串空间是包含各种合法主体串和攻击者串的集合# 及
Байду номын сангаас
协议的有力武器 + 目前分 析 安 全 协 议 的 形 式 化 方 法 主 要 有 $ 该 方 法 基 于 知 识 和 信 念 推 理 的 模 态 逻 辑# 如 ! 推 理 构 造 法#
! " " &年&月 第’ ’卷!第’期
!
西安电子科技大学学报 （自然科学版） ! "#$%& ’!" (!) * + * &%!#% * , -$ . * /0
!
U < A+ ! " " & V 8 + ’ ’!P + ’
一种形式化分析安全协议的新模型
慕建君
! 西安电子科技大学 计算机学院 " 陕西 西安 !% # ) " " % ) 摘要 ! 串空间是安全协议形式化分析的一种新模型 + 利用次序关系的理论证明了借助串空间模型进行 安全协议形式化分析的一个重要结论 + 通过构造 入 侵 者 串 的 方 法 ! 针对 , $ . / 0 协议提出了一个入侵 者串空间模型 ! 同时利用此入侵者串空间模型分 析 了 该 协 议 存 在 的 缺 陷 ! 说明了改进后的 , $ . / 0协 议可克服此缺陷 + 与现有安全协议形式化分析方法 相 比 较 ! 串空间模型不仅具有简洁直观的优点! 而且 还可避免状态空间爆炸的问题 + 关键词 ! 安全协议 " 形式化分析 " 串空间模型 " 入侵者串 中图分类号 ! " # 1 2 ’ " *!! 文献标识码 ! 3!! 文章编号 ! ) " " ) $ ! ( " " ! " " & " ’ $ " ’ 4 ) $ " #
+ 串8 中& & ) 是& ! 的直接前驱 . )* & ! 表示在同一串上 & ) 是& ! 的前驱但不一定是直接前驱 + 0= &) . % 一个无符号项- 出现在结点& $ : 当且仅当- # > ? 0(
源于 ) 结点& $ : 如果0= 的符号为正且-# ! 但对于同一串上 &) 0= &) & 一个无符号项-产生于 ( > ? 0( > ? 0( , 结点 & 的任何前驱& <有 -# 0= & <) . > ? 0( ’ 一个无符号项- 惟一产生的如果- 产生于惟一的结点& $ : . 容易看出 ! 结点集 : 与边& ! ( & ) ’& ! 和& )* ! 的集合一起构成了一个有向图 " & ’+ * )# . ! " $! 束和次序关系 一 个束表示在某一具体情形下一个协议的执行过程 ! 它是有向图 "&! ( 此子图 ’+ * ) # 的有限子图 ! 中的边表示结点之间的因果依赖关系 + 定义 %! 假设 ’= ,’ ! 令 > 2 " :> ! ( ( 其中 :> 表 *= , * . ’= + *=) # 是 " :! ’+ * ) # 的子图 !
&’ ’’ 但K 而不能分析协议的保密性质 & % 该方 K 3P 逻辑 ! 等 # 3P 逻辑只能分析协议的认证性质 # " 攻击构造法 # 法从协议的初始状态开始 # 对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索 # 以期找到协议可能 &’ & #’ 存在的错误 + 这种方法主要有基于模型检测技术的模型检测器 Q 验证语言 M 代数 简化 理论模 R S( ( < ? ! ( & &# %’ 型以及特定专家系统 ! 如特殊目的 PS " # 但这种方法无法解决状态空间爆炸问 . 分 析 器 和T A = > ? ? / = ? C
$ ! 5 0 3 * + 1 3 = ? / A BI / 6 > @ I /A > J0 B > 8 9 ? = 7 > 9 ? 0 / 8 / A / 8 I @ I9 I > 6 < ? @ = ? = 6 8 I + K !5 ; D D; D < I @ A 7 > = 7 > ? 9? B > ? ? > 8 / = @ A# /G > ? 0 ? = / A =6 A 6 8 < I @ A< I > B= -/ A / 8 L >I > 6 < ? @ = C= DD@ ; D D ? = 6 8 I 9 ? 0 / 8 8 @ = 7= 7 >7 > 8 9= 7 >I = ? / A BI / 6 >0 B > 8 @ II 7 J A+K A I = ? < 6 = @ A ; DJ ;; D6 C > A > = ? / = ?I = ? / A B I 9 ? = 7 >, $ . / 0; ? = 6 8J >; ? > I > A = /I = ? / A BI / 6 >0 B > 8 @ A 9 @ 8 = ? / = > B ; ; #J 9 ? = 7 @ I; ? = 6 8 +M ? > G > ? @ = 7= 7 >7 > 8 9= 7 @ II = ? / A BI / 6 > 0 B > 8@ A 9 @ 8 = ? / = > B J > ; ; / A / 8 L > = 7 >9 8 / J@ A= 7 @ I; ? = 6 8/ A B@ 8 8 < I = ? / = >= 7 / == 7 @ I9 8 / J@ A= 7 @ I; ? = 6 86 / AN > D G > ? 6 0 > @ A= 7 > @ 0 ? G > B, $ . / 0; ? = 6 8 +1 7 >I = ? / A BI / 6 >0 B > 8B @ I 6 < I I > B/ N G > ; ; @ IB @ I = @ A < @ I 7 > B9 ? 0= 7 > ?0 B > 8 IN = II @ 0 8 @ 6 @ = A B6 / A/ G @ B= 7 >I = / = >I / 6 > C D@ ; D/ ; > O 8 I @ A; ? N 8 > 0+ ; $ % % % 6 # & * ’ 0 > 6 < ? @ = ? = 6 8 9 ? 0 / 8 / A / 8 I @ I I = ? / A BI / 6 >0 B > 8 > A > = ? / = ?I = ? / A B !I D; D ; ; ,7 安全协议是采用密码技术来保障通信各方之间安全交 换信息 的一个 规则 序 列 # 其目的是在通信各方之 间提供认证或为新的会话分配会话密钥 + 尽管现有的安全协议是安全专家精心设计和详细审核过的 # 但仍然
收稿日期 ! ! " " # $ " # $ ! % 基金项目 ! 国家自然科学基金资助项目 ! " & " # % ’ " ’ ( 作者简介 ! 慕建君 ! " # 男# 副教授 # 博士 + ) * & # $
自然科学版 " ’卷 !!!!!!!!!!! !!!!! 西安电子科技大学学报 ! !!!!!!!!!!! !!!!! 第 ’ ’ 4 !
8! 串空间模型
! " !! 项和子项 * 中的元素称为项 + !! 设 * 表示一个协议中参与者之间可能交换的所有消息的集合 ! 定义 !! 符号项是一个有序对 ""! 其中 % $ *! ! 记一个符号项为 +-或 ,! % #! +! ,& +-表示 "$ % % 发出项’ ( ,- 表示接收到项-. /*) 表示符号项的有限序列的集合 + 设 0 表示原子信息集合 ! 且 0 & 1 23! 通常假设集合 * 是由集合 1 和0 在求逆密钥 1 表示密钥集合 ! 加密 % 4 * 5& 5! 下生成的自由信息空间代数 + 4 和级联运算 5) 定义 #! 设 * 自由信息空间代数 ! 可递归定义为 + 有% # * 上的子项关系 # %’ ! 对所有的% 2- $0!
) ,
有% # ! 则% # % 或 %’ 4 $1) " 对所有 的% 2 4 $1 ! # 若% # $ 若% # 6 或% 2 % 6& 6 $*! 6& 6! 4 ( 4’ ! 则% # 7( 7. %# 7 或% 26 7 $*) 6 $*! 6 ! " #! 串和串空间 串是一个参与者可能参与的事件序列 + 对于合法参与 者 ! 每个 串是接收 和 发 送 的 消 息 序 列 ! 表示该参与 者在一次特定协议执行中的行为以及所有数据项 ( 如 密 钥和临 时值 ) 的特 定值 + 攻击 者 串 是 攻 击 者 可 能 发 送 和接收的消息序列 + 定义 $! 设 * 为自由信息空间代数 ! * 上的一个串空间是包含各种合法主体串和攻击者串的集合# 及
Байду номын сангаас