网络安全协议的形式化分析与验证 作者 李建华 第五章 安全协议的形式化设计方法.pptVIP

第5章 安全协议的形式化设计方法 最初人们在设计密码协议时主要是采用非形式化的方法。实践证明，几乎所有这样设计出的协议都存在安全漏洞。 Adnerson和Needham提出了一些协议健壮性原则 Abadi和Needham给出了理想的协议特性的设计规则 设计安全协议是一项十分复杂与困难的工作。协议的形式化分析方法在成功发现许多协议漏洞的同时，也不断为协议设计者总结了很多设计经验。 形式化的方法逐渐应用于协议设计方面。 第5章 安全协议的形式化设计方法 5.1 合成协议模型及其安全性 5.2 Fail-Stop协议 5.3 BSW简单逻辑 5.4 本章小结 5.1 合成协议模型及其安全性 协议的一致性问题是人们普遍关心的一个问题。 Heintze和Tygar提出了推证协议安全性的一个基础， 采用了一种基于模型的定义协议安全性质的方法 该方法最为突出的特点是对协议的合成。假设将两个协议A、B合成为一个新的协议C，如果A和B是安全的，那么在什么条件下C是安全的？ Heintze和Tygar给出了A和B的足够条件以保证合成协议C是安全的。 5.1 合成协议模型及其安全性 5.1.1 HT模型 1．消息、密钥和加密 2．路径 3．协议和非记时模型 5.1.2 协议的组合 5.1.1 HT模型 在HT模型定义中，通信主体处于分布式网络中，他们在公共信道上发送与接收消息。 主体的内部状态决定了它们的行为。一些主体将不依照协议执行，另一些主体可能会部分诚实。 协议被视为主体可能采取行为的一个约束。 每个主体与一个将其当前状态映射为可能的下一个行为的函数相关联。 5.1.1 HT模型 模型中，每个主体的内部状态包括3个部分： ①主体已知的消息和密钥； ②主体认为是安全的消息和密钥； ③主体新生成的随机数。 5.1 合成协议模型及其安全性 5.1.1 HT模型 1．消息、密钥和加密 2．路径 3．协议和非记时模型 5.1.2 协议的组合 5.1.1 HT模型 HT模型采用了完美加密假设，对协议分析包含以下 两个步骤： 1）集中分析协议固有的安全性质，并忽略关于所使用 的加密体制的细节; 2）分析加密体制与协议的交互。 5.1.1 HT模型 设B为基本消息集，包括密钥K，随机数N和不可分解的消息。 消息定义为基本消息的合成与加密的结果。因此，消息M可为 ①基本消息； ②{M}K，用密钥K加密消息M； ③(M1，…，Mn)，消息M1，…，Mn的合成。 对于一个已知的消息集S，一个主体具有有限的将消息解密和分解并构建新消息的能力。定义S*表示可从S中生成的消息集合。 5.1 合成协议模型及其安全性 5.1.1 HT模型 1．消息、密钥和加密 2．路径 3．协议和非记时模型 5.1.2 协议的组合 5.1.1 HT模型 设 ? 为所有主体的集合。可将每个主体看做一个包含“状态”及合法迁移集的自动机。 用路径来记录主体行为。 基本的交互行为用事件（Event）表示，具体有以下几种类型。 1）send(M)：主体发送消息M； 2）receive(M)：主体接收消息M； 3）generate(M)：一个基本消息M由一个主体生成； 4）expire(M)：消息M已经失效。 5.1.1 HT模型 定义5.1 路径T是一个以?为索引的所有事件集合的全体，其中每个事件集合都有一个完整顺序。 TA表示对应于主体A的集合，T表示所有TA的集合。 定义在TA上的顺序记为A；如果e Ae′，那么e precedes e′。e ≤ Ae′ 表示e Ae′或e = Ae′ 。 对于任一事件e ∈ TA ，如果它存在一个后继，则记为succ(e)，即succ(e)表示{ e ：e Ae′}中最早发生的事件。 路径并未指出主体间事件的顺序。 5.1.1 HT模型 定义5.2 路径T是有界的，对于所有主体A和所有TA中的事件对e1和e2，集合{e：e1 Ae Ae2 }是有限的。 定义5.3 路径T是可串行化的，如果T中存在顺序 ，使得： 1）顺序是对A的一个保守扩展，即对于A ∈ ?， 如果e Ae′，则 e e′； 2）T中的每一个接收事件receive(M)的前驱为发送事件send(M)； 3）对于所有的事件对e1和e2，集合{e：e1 e e2 }是有限的。 定义5.4 路径T表示消息生成，对于所有可区分的事件generate(M1)和generate(M2 )，消息Ml和M2是可区分的。 5.1 合成协议模型及其