Ｄｉｇ ａ ａ ｒ ｍｍａ ｉ ｎ ｌ ｉ ｉ ｄ ｐ ｅ ， ｉ ｈ ｍａ ｅ ｅ ｕ ｔｏ ｆｐ ｏ ｏ ｏ ｒ ｌａ ｎ ｎ ｕ ｔｖ ． ｉ ｔ ｏ ｎ ｌ ｚ ｓｔ ｅ ｔｕ ｔ ｏ ａｎ ｏ ｒ ｔ ｃ ｌ ｔ ａ ａｙｓｓ ｓ ａ ｏ ｔ ｄ ｗｈ ｃ ｋ ｓ ｄ ｄ ｃ ｉ ｎ ｏ ｒ ｔ ｃ ｌ ｃ ｍｏ ｅ ｃ ｅ ｒａ ｄ ｉ ｔ ｉｉｅ Ｔｈ ｓｍｅ ｈ ｄ ａ ａ ｙ ｅ ｈ ｒ ｓ ｍ ｉ ｆ ｏ ｏ ｏ ｄ ｐ ｅ ｔ ｙ ｄ ｒ ｃ ｌ ，ｗｈ ｃ ｋ ｓ ａ ａ ｙ ｉ ａ ｉ ｒ ｎ ｉ ｉｅ ｔ ｔ ｙ ｉ ｈ ｍａ ｅ ｎ ｌ ｓ ｓ ｅ ｓｅ ．Ｅｘ ｅ ｉ ｎ ａ ｅ ｕ ｔ ｈ ｗ ｈ ｔｔ ｅ ｍ ｅｈ ｄ ｉ ａ ｔ ｒ ａ ｄ ｍｏ ｅ ｉ ｔ ｉｉ ｅ ｃ ｍｐ ｒ ｄ ｗｉ ｒ ｄ ｔ ｎ ｌ ｐ ｒｍｅ ｔ ｌｒ ｓ ｌｓ ｓ ｏ ｔ ａ ｈ ｔ ｏ ｓ ｆ ｓ ｅ ｎ ｒ ｎ ｕ ｔｖ ｏ ａ ｅ ｔ ｔａ ｉ ｏ ａ ｈ ｉ ｍｅｈ ｄ ． ｔ ｒ ｖｉ ｅ ｙ ｎ ａ ｉ ｆ ｒｆｎ ｉ ｇ ｒ ｄ ｎ ａ ｃ ｅ ｆ ｅ ｕ ｉ ｒ ｔ ｃ ｓ ｔ ｏ ｓ Ｉ ｏ ｄ ｓｗａ ｓａ ｄ ｂ ｓｓ ｏ ｄ ｎ ｅ ｕ ｄ ｎ ｉ ｓｏ ｃ ｒｔ ｐ ｏ ｏ ｏｌ． ｐ ｉ ｓ ｙ
中 圈分类号ｌ Ｐ０ ３９ Ｔ
种安 全协 议 的形 式化 分析 方 法
王 昕，袁超伟
（ 北京邮 电大学信 息与通信工程学院，北京 １０ ７ ） ０８６
摘
要： 对快速、高效 的形式化分析安全协议进行研究 ， 出 “ 提 信任域”的概念 。采用与图形化相结合的分析方法 ，使得协议 流程 的推导
［ ｓｒｃ］ Ｔ ｉ ｐｐｒｒｓａｃ ｅ ｎ ｑ ｉ ｎ ｆ ｃ ｎ ｏｍａ ａ ａ ｓｓｏ ｅｕｉ ｒｔｃ ｌ ｎ ｒｓｎｓｔｅ ｃｎ ｅｔｏ ｕ ｔｄ ｍａｎ Ａｂｔａ ｔ ｈｓ ａｅ ｅｅｒｈｓ ｏ ｕｃ ａ ｄ ｅｆ ｉ ｔｆｒ ｌ ｎｌ ｉ ｆｓｃｒｔ ｐｏｏｏ，ａ ｄ ｐｅｅｔ ｈ ｏ ｃｐ ｆｔ ｓ ｏ ｉ． ｋ ｉｅ ｙ ｙ ｒ
Ｗ Ａ ＮＧ ｎ， Ｘｉ ＹＵ ＡＮ Ｃｈａｏ ｗ ｅ － ｉ
（ｃｏ ｌ ｆｎｏｍａ ｏ ｎ ｏ Ｓ ｈ ｏ Ｉｆｒ ｔ ｎａ ｄＣ ｍｍｕｉａｉｎＥ ｇｎｅｉｇ Ｂ ｉｎ ｎｖｒｉ ｆ ｏｔ ａｄＴ ｌ ｏ ｏ ｉ ｎｃｔ ｎ ｉｅｒ ， ｅ ｉｇＵ ｉｅｓｙｏ Ｐ ｓ ｎ ｅｅ ｍｍｕ ｉａｉｎ， ｅ ｉｇ１０ ７ ） ｏ ｎ ｊ ｔ ｓ ｃ ｎｃｔ ｓＢ ｉｎ ０ ８ ６ ｏ ｊ
涉及。 文献【＿】 Ｂ Ｎ类逻辑为基础 ， 用逻辑分析与模型 ７８以 Ａ 采 检测相结合的方式完成分析 ，扩充 了分析范围，但形式化方 面仍较欠缺。实际上 ，协议设计和分析的 目标应是参与协议 主体的信任状态 ， 即分析过程 中应更关注主体所信任 的事物 ， 随协议的执行而发生变化 。 原有 Ｂ Ｎ类逻辑初始假设人为设 Ａ 定 ，是 否 合适 需 要 在 分析 完成 后 进 行 人工 检 验 。文 献 【］ ９同样
［ ｙｗｏ ｄ ］ ｆｒ ｌ ｎ ｌｓ ； ｅ ｕ ｉ ｒ ｔｃ ｌＢ ｇ ｃ ＮＳ Ｋ ｐ ｏｏ ｏ Ｋｅ ｒ ｓ ｏ ｍａ ａ ａｙ ｉ ｓ ｃ ｒ ｙｐ ｏｏ ｏ； ＡＮ ｌ ｉ； Ｓ ｒｔｃ ｌ ｓ ｔ ｏ
１ 概述
安全协议 的设计和分析十分复杂，采 用形式化分析 方法 可 以有效地降低分析过程 的复杂度 ，使得安全协议 的分析简 单、 规范和实用。 Ｎ ， Ｔ ＶＯ和 Ｓ Ｏ等 Ｂ Ｎ类逻辑方法ｌ Ｇ ＹＡ， Ｖ Ａ Ｊ 在安全 协议 的形式化分析 中被广 泛采用 ，新 的形式化分析 ｊ 方法也不断 出现Ｉ ｊ 是，Ｂ Ｎ 类逻辑分析 方法将论证的 ｊ 。但 Ａ 空问落在 了协议 的参与主体上，论证的焦 点是参与协议的主 体 ，这样容易造成分析过程 中对于主体的逻辑判断加入人为
第３ ６卷 第 ７期
ＶＬ ｏ ３６
・
计
算
பைடு நூலகம்
机
工
程
‘
２１ ００年 ４月
Ａｐｒｌ ０１ ｉ ２ ０
Ｎｏ７ ．
Ｃｏ ｐｕ ｅ ｍ ｔ ｒＥｎｇ ｎｅ ｒｎｇ ｉ ｅｉ
软 件技术 与数据 库 ・
一
文章编号：１０＿ ４８０ｏ ７＿８ ＿ 文献 ０ｍ－ ２（ １０—０ ２ ｏ ３ ２ ） ０— ２ 标识码： Ａ
的误判 ，与 事实不符 。文 献【］ Ｊ ６中在构造类别代数的基础上
引入了 “ 规则集合” 知识集合”的概念 ，对于 协议 的规范 、“
化 描述 起 到 重 要作 用 ，但 对 其在 协议 形 式 化 分析 的应 用 并 未
ｊ ：接收到新消息前，主体 的信任域为 ， 随着 Ｊ
Ｌ ＝
（） 法 和 语义 １语
ｙ ：参 与 协议 的主 体 。
Ｘ ： 与 ｙ之问共享对称密钥 。 Ｙ
Ｍ ：Ｍ 是 新 鲜 的。
（ ：用 与 ｙ共享 的对称密钥加密 的消息 ） ［ ｒ ：主体 相信 。
Ｉ Ｉ ｘ：主 体 控 制 Ｍ。 （ ） ：主 体 曾发 送过 。 ４－ ４ ：被 使 用 过 的条 件 。
过程清晰、直观 。 方法直接分析协议参与主体的信任域，简化 分析过程和步骤。实验结果表 明， 该 与传统方法相比 ， 该方法更快速、直观 ，
并能为分析协议的冗余性提供具体方法和依据。
关健诃 ： 式化分析 ；安全协议 ；Ｂ Ｎ逻辑 ； Ｓ Ｋ协议 形 Ａ Ｎ Ｓ
Ｆｏ ｍ ａ ｒ ｌ Ａｎａ ｙ ｉ ｅ ｈ ｄ ０ ｃ ｉ Ｐｒ ｔ ｃ ｌ ｌ ｓｓＭ ｔ ｏ ｆＳｅ ｕｒｔ ｙ ｏ ｏ ｏ