第2章安全协议-中山大学信息科学与技术学院本科教育网站

第2章安全协议-中山大学信息科学与技术学院本科教育网站内容摘要：

为 AVISPA 工具集提供一个集成的 GUI界面，使其简单易用。 AVISPA（ Automated Validation of Inter Security Protocols and Applications）是由欧洲委员会（ European Commission）资助并由欧共体的意大利、法国、瑞士和德国等国的大学或研究机构联合进行的一个项目。 项目启动于 2020 年1 月 1 日并在进行中。 项目的宗旨是为 Inter 上安全敏感的大型协议和应用开发一种自动化的和工业级的分析技术。 [10] 下面是 AVISPA 的模块结构图： 9 图 1 .AVISPA 的工具模块结构图 顶层的是 Translator HLPSL2IF（即 hlpsl 编译器）， 它将用 HLPSL（ High Level Protocol Specification Language）语言描述的协议编译成用 IF（ Intermediate Format）描述的协议。 HLPSL 语言易于理解，方便用户读和写 HLPSL 规范。 编译后得到的 IF描述的协议就可以输入到底层的工具以进行验证。 目前，底层的工具集包括 四个 ： OFMC（ OntheFly Model Checker） 基于 CL（ Constraint Logic）逻辑的定理证明器 AtSe 基于 SAT 的模型检测器 SATMC（实际上 SATMC 又包括三个 sat Solver： Chaff、SIM 和 SATO） 树自动化分析器 TA4SP 事实上每个工具内部又有相应的编译器将 IF 编译成本地描述语言。 OFMC 较 Casper 的优点是：不会产生消息空间和状态空间的爆炸问题，协议验证过程所需时间非常短。 这一点使其非常适于分析大型的工业级密码协议。 各工具集各有优点，但在时间效率上， AtSe 要较 OFMC 要高。 另外 经试验， SPAN 的 windows 版本中的底层工具子集 SATMC 是使用不了的，因为其要调用 的 bash shell 脚本，这脚本只能在 UNIX/LINUX 运行。 但一般情况下，对协议的分析验证只需要用到 SPAN 中的 OFMC 和 AtSe 两个工具子集就足够了。 10 本文采用的是 windows 版本的 SPAN 程序。 当 协议经过底层工具集检验后，程序将 会 给出安全 或不安全两种结果，对于不安全的情况将给出详细的攻击序列。 这样我们就能够根据理论分析和攻击实例来改进协议。 注意 ：因为 SPAN 是 AVISPA 的图形界面，为了提醒读者这一事实： AVISPA 才是真正的自动化分析工具，所以下文中提及 SPAN 程序统一使用 AVISPA 来代替， 11 第四章 使用自动化验证工具分析经典安全协议 这里我们选取了两个经典的协议，采用自动化验证工具 AVISPA 来进行分析，看是否有攻击的存在，如果有是，则根据攻击实例序列来修改协议，直至通过形式化验证后结果 为 Safe。 同时把得出的结果与安全协议学者已得出的结果进行比较，从而发现 AVISPA 工具集 目前存在的一些局限性。 NSPK 协议 协议描述 NSPK 协议 [11]描述如下：  协议初始假设： A , B ：协议主体，相互间平等 Na， Nb ：新鲜随机数 Ka， Kb ：分别是 A, B 的公开密钥 A 的初始知识： A ,B ,Ka, Kb B 的初始知识： A, B, Ka, Kb  协议步骤如下： 1) A B: { }_Kb 2) B A: { }_Ka 3) A B: { Nb }_Kb 即 ： Step1。 用户 Alice 生成新鲜随机数 Na,并把 Na 和代表他的用户标识符 A 级连后，用 Bob 的公开密钥加密后 ,发送给用户 Bob。 Step2。 用户 Bob 接收到 消息 { }_Kb 并解密后，把得到的 Na 和他自己新产生的新鲜随机数 Nb 级连， 根据解密得到的用户标识符 A 来选择 用 Alice的公开密钥 把级连后的消息 加密后发送给 Alice。 Step3。 用户 Alice 接收到 消 息 { }_Ka 并解密后 ， 首先把解密得到的 Na 与之前他自己产生并保存的 Na 进行比较，如果一致的话，则证明通信对方 12 能解读用 bob 公开密钥加密的信息，从而 认为 通信对方确实是用户 Bob，并 把 解密 得到的 Nb 用 Bob 的公开密钥加密后发送回 Bob；如果不一致的话， 则认为通信对方不是用户 Bob， 中止通信。 Step4。 用户 Bob 收到消息 { Nb }_Kb 后 ， 把解密后得到的 Nb 与 之前他自己产生且保存的 Nb 进行 对比，如果一致的话，就认为通信的对方就是用户 Alice，从而完成 对 Alice 认证 ，可以跟 Alice 进行安全通信 ；不一致的话，则 认为 认证失败，中断通信。  协议目标： 1) A 和 B 相互认证，即 A 想确认协议运行中的另一方确实就是其所声称的 B； B想 确认协议运行中的另一方确实就是其所声称的 A。 2) Na 和 Nb 的机密性，以后可以使用二者来产生共享的会话密钥。 如上，协议假定双方都知道对方的公开密钥。 A 首先生成新鲜临时值 Na 与其标识符级连，用 B 的公开密钥加密后发送给 B。 B 接收到后，生成新鲜临时值 Nb，与Na 级连后用 A 的公开密钥加密后发送给 A。 因此 ,B 通过能读第 1 条消息来向发起者证明自己的身份，从而响应了发起者的请求，最后 A 通过返回用 B 的公开密钥加密的 Nb，让 B 检验 Nb 的值以确认 A 的身份。 NSPK 协议的自动化分析 把 节中描述的 NSPK 协议 ，用 hlpsl 语言描述出来，具体编程注意事项请参考文献 [12][13]。 这里就不给出完整的编码（见论文附件 ），只给出 入侵者的初始知识和 要达到的安全目标的 hlpsl 描述： Intruder_knowledge = { a, b, ka, kb, ki, inv(ki)} goal secrecy_of na , nb %确保 na， nb 的机密性 authentication_on bob_alice_nb %bob 凭 nb 认证 alice end goal 注意 ： 根据协议的详细 描述， alice 是通过某用户能读用 bob 的公钥加密的信息的事实来认证该用户就是 bob，这一点已经隐含在通信过程中。 实质上，协议设计者这 13 一想法导致了该协议会遭到了中间人攻击。 在下面的分析中，我们将看到这一点。 用 AVISPA 中的 OFCM 验证结果如下： % OFMC % Version of 2020/02/13 SUMMARY UNSAFE DETAILS ATTACK_FOUND PROTOCOL C:\SPAN\testsuite\results\ GOAL secrecy_of_nb BACKEND OFMC COMMENTS STATISTICS parseTime: searchTime: visitedNodes: 8 nodes depth: 2 plies ATTACK TRACE i (a,6): start (a,6) i: {Na(1).a}_ki i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki i (i,17): Nb(2) i (i,17): Nb(2) 14 从输出结果中 ，我们可以看到协议是 UNSAFE 的，同时知道安全目标 goal 中的secrecy_of_nb 无法满足 ，即无法保证 nb 的机密性。 然后我们详细分析下 AVISPA 给出 ATTACK TRACE（攻击序列）： i (a,6): start (a,6) i: {Na(1).a}_ki 这里入侵者 i 作为一个合法用户 ，与用户 a 开始一次合法的通信 ， a 产生一个新鲜临时值 Na(1)，并用 i 的公开密钥 ki 加密 Na(1).a 后把加密结果发给 i i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka 入侵者 i 用自己的私 有密 钥 inv(ki)解密从 a 接收到消息 ，并解密结果用用户 b 的公开密钥 kb 加密后发送给用户 b。 b 接收 此消息后，将产生新鲜临时值 Nb(2)， 并将其与 Na(1)级连后用 a 的公开密钥 ka 加密后，发送该消息。 入侵者 i 截获到该消息。 i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki 入侵者 i 把截获到的信息转发 a， a 解密消息后 ， 把 Nb(2)用 i 的公开密钥加密后发给 i， 从而使得 i 也可以 获知 Nb(2)。 仔细分析以上 AVISPA 给出的攻击序列，除了获知入侵者 i 能通过中间人攻击来获得 Nb 的值外 ，我们还发现在此协议中用户 a 无法确认接收 到的 消息{Na(1).Nb(2)}_ka 是否真正由正在与其通信的对方产生，并发送给他的，只是简单的认为谁把这一消息发给他，谁便是这一消息的产生者，而且用户 a 回 发的信息将采用该用户的公钥进行加密。 我们认为用户 a 的这一行为正是导致协议遭到中间人攻击的原因，从而使 NSPK 协议不能满足 secrecy_of_nb，同时也 将 使另一目标authentication_on bob_alice_nb 失败。 为了验证一点，我们把安全目标改成：（具体编码见附件 ） goal authentication_on bob_alice_nb %bob 凭 nb 认证 alice end goal 用 AVISPA 验证后的输出结果如下： 15 % OFMC % Version of 2020/02/13 SUMMARY UNSAFE DETAILS ATTACK_FOUND PROTOCOL C:\SPAN\testsuite\results\ GOAL authentication_on_bob_alice_nb BACKEND OFMC COMMENTS STATISTICS parseTime: searchTime: visitedNodes: 15 nodes depth: 3 plies ATTACK TRACE i (a,6): start (a,6) i: {Na(1).a}_ki i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki i (b,3): {Nb(2)}_kb 整个攻击过程与 NSPK_1 相似 ， 这 就 证明我们的想法正确，即“用户 a 无法确认接收到的消息 {Na(1).Nb(2)}_ka 是否真正由正在与其通信的对方产生，并发送给他的，只是简单的认为谁把这一消息发给他，谁便是这一消息的产生者”这一事实是导 16 致了 NSPK 协议遭遇中间人攻击。 下面我们就这发现进行对 NSPK 协议的修改 NSPK 协议的改进 根据 节中的分析，我们对 NSPK 协议进行修改，修改后的协议 描 如下：  协议初始假设： A , B ：协议主体，相互间平等 Na， Nb ：新鲜随机数 Ka， Kb ：分别是 A, B 的公开密钥 A 的初始知识： A ,B ,Ka, Kb B 的初始知识： A, B, Ka, Kb  协议步骤如下： 1) A B: { }_Kb 2) B A: {B. }_Ka 3) A B: { Nb }_Kb 即 ： Step1。 用户 Alice 生成新鲜随机数 Na,并把 Na 和代表他的用户标识符 A 级连后，用 Bob 的公开密钥加密后 ,发送给用户 Bob。 Step2。 用户 Bob 接收到消息 { }_Kb 并解密后，把代表 Bob 的用户标识符 B，解密后得到的 Na 和他自己新产生的新鲜随机数 Nb 级连，根据解密得到的用户标识符 A 来选择用 Alice 的公开密钥把级连后的消息加密后发送给Alice。 Step3。 用户 Alice 接收到消息 { }_Ka 并解密后 ，首先把解密得到的 Na与之前他自己产生并保存的 Na 进行比较，如果一致的话，则证明通信对方能解读用 Bob 公开密钥加密的信息， 并且若解密后的用户标识符是 Bob的标识 B，则可 认为通信对方确实是用户 Bob，并把解密得到的 Nb 用 Bob的公开密钥加密后发送回 Bob；如果不一致的话，则认。