基于 spi 演算的安全协议验证

《基于 spi 演算的安全协议验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第２８卷第３期计算机应用与软件Ｖｏｌ２８Ｎｏ．３２０１１年３月ＣｏｍｐｕｔｅｒＡｐｐｌｉｃａｔｉｏｎｓａｎｄＳｏｆｔｗａｒｅＭａｒ．２０１１基于Ｓｐｉ演算的安全协议验证郑清雄（上海交通大学计算机科学与工程系上海２００２４０）摘要在安全协议的各种验证方法中，进程代数方法依托完善的进程演算理论得到了很好的应用。Ｓｐｉ演算在ＰＩ演算的基础上扩充了密码操作原语来刻画安全协议，并使用测试等价验证安全属性。讨论了利用Ｓｐｉ演算进行验证的过程，并对经典ＮＳＳＫ协议进行分析。关键词安全协议　Ｓｐｉ演算测试等价　ＮＳＳＫ协议ＶＥＲＩＦＹＩＮＧＳＥＣＵＲＩ

2、ＴＹＰＲＯＴＯＣＯＬＳＢＡＳＥＤＯＮＳＰＩＣＡＬＣＵＬＵＳＺｈｅｎｇＱｉｎｇｘｉｏｎｇ（ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＥｎｇｉｎｅｅｒｉｎｇ，ＳｈａｎｇｈａｉＪｉａｏｔｏｎｇＵｎｉｖｅｒｓｉｔｙ，Ｓｈａｎｇｈａｉ２００２４０，Ｃｈｉｎａ）Ａｂｓｔｒａｃｔ　　Ａｍｏｎｇｓｅｖｅｒａｌａｕｔｈｅｎｔｉｃａｔｉｏｎｍｅｔｈｏｄｓｆｏｒｓｅｃｕｒｉｔｙｐｒｏｔｏｃｏｌｓ，ｐｒｏｃｅｓｓａｌｇｅｂｒａａｐｐｒｏａｃｈｗｈｉｃｈｒｅｌｉｅｓｏｎａｓｏｕｎｄｔｈｅｏｒｙｏｆｃｏｎｃｕｒｒｅｎｔｐｒｏｃｅｓｓｃａｌｃｕｌｕ

3、ｓｈａｓｂｅｅｎｗｅｌｌａｐｐｌｉｅｄ．ＴｈｅＳｐｉｃａｌｃｕｌｕｓｄｅｐｉｃｔｓｓｅｃｕｒｉｔｙｐｒｏｔｏｃｏｌｓａｓａｎｅｘｔｅｎｓｉｏｎｏｆｔｈｅｐｉｃａｌｃｕｌｕｓｂｙｅｎｒｉｃｈｉｎｇｉｔｓｃｒｙｐｔｏｇｒａｐｈｉｃｐｒｉｍｉｔｉｖｅｓ，ａｎｄｕｓｅｓｔｅｓｔｉｎｇｅｑｕｉｖａｌｅｎｃｅｔｏｖｅｒｉｆｙｓｅｃｕｒｉｔｙｐｒｏｐｅｒｔｉｅｓ．ＴｈｅｐｒｏｃｅｓｓｏｆａｕｔｈｅｎｔｉｃａｔｉｏｎｗｉｔｈＳｐｉｃａｌｃｕｌｕｓｉｓｄｉｓｃｕｓｓｅｄｉｎｔｈｅｐａｐｅｒ，ｔｈｅａｎａｌｙｓｉｓｏｎｃｌａｓｓｉｃａｌＮＳＳＫｐｒｏｔｏｃ

4、ｏｌｉｓｃａｒｒｉｅｄｏｕｔｕｓｉｎｇｔｈｉｓａｐｐｒｏａｃｈａｓｗｅｌｌ．Ｋｅｙｗｏｒｄｓ　　Ｓｅｃｕｒｉｔｙｐｒｏｔｏｃｏｌｓ　Ｓｐｉｃａｌｃｕｌｕｓ　Ｔｅｓｔｉｎｇｅｑｕｉｖａｌｅｎｃｅ　ＮＳＳＫｐｒｏｔｏｃｏｌＬ，Ｍ，Ｎ　　　　　　　　　ｔｅｒｍｓ０　引言ｎｎａｍｅ（Ｍ，Ｎ）ｐａｉｒ安全协议是信息安全的基础，然而设计一个符合安全目标　０ｚｅｒｏ的协议十分困难。因此，必须借助形式化方法，对安全协议进行ｓｕｃ（Ｍ）ｓｕｃｃｅｓｓｏｒ分析和验证［１］。基于进程代数的安全协议验证能够精确地描ｘｖａｒｉａｂｌｅ述协议中不同主体之间的交互过程

5、，得到了广泛的应用。Ａｂａｄｉ｛Ｍ｝ｎｓｈａｒｅｄｋｅｙｅｎｃｒｙｐｔｉｏｎ和Ｇｏｒｄｏｎ在ｐｉ演算［２，３］的基础上，增加密码学描述原语，建立在ｐｉ演算中，名是唯一的项。Ｓｐｉ演算增加了描述对（ｐａｉｒ）和数字（ｚｅｒｏ，ｓｕｃｃｅｓｓｏｒ）的项结构是为了便于在安全协议中描了用来描述和验证安全协议的Ｓｐｉ演算。Ｓｐｉ演算保持了ｐｉ演述它们。而将变量从名中区分开来则是为了简化一些等式的描算简单的语法和强大的描述能力，采用互模拟等价理论对安全述。另外，Ｓｐｉ演算增加了基于共享密钥加密的项结构，项｛Ｍ｝Ｎ协议进行验证。表示在共享密钥系统（如

6、ＤＥＳ）中用密钥Ｎ对项Ｍ加密所得到本文以Ｓｐｉ演算为工具对安全协议验证的过程进行描述，的密文。并且在Ｓｐｉ演算框架内验证对经典ＮＳＳＫ协议的一种攻击方法。１．２　Ｓｐｉ演算的进程进一步，定义Ｓｐｉ演算中的进程（ｐｒｏｃｅｓｓ）集合：１　Ｓｐｉ演算的语法Ｐ，Ｑ，Ｒｐｒｏｃｅｓｓｅｓｍ〈Ｎ〉．Ｐ　ｏｕｔｐｕｔ［４，５］ｐｉ演算是ＲｏｂｉｎＭｉｌｎｅｒ在ＣＳＳ等进程演算的基础上提Ｍ（ｘ）．Ｐ　ｉｎｐｕｔ出的，已经成为并发计算的基础模型。ｐｉ演算能够表示通信拓Ｐ｜Ｑ　ｃｏｍｐｏｓｉｔｉｏｎ［６］扑结构可以动态变化的系统（既移动进程）。Ｓｐｉ演算是

7、对ｐｉ（ｖｎ）Ｐ　ｒｅｓｔｒｉｃｔｉｏｎ演算的增强和扩充，增加了支持密码系统的原语。利用Ｓｐｉ演！Ｐ　ｒｅｐｌｉｃａｔｉｏｎ算，我们能够对协议进行详细的抽象和分析。［ＭｉｓＮ］Ｐ　ｍａｔｃｈ１．１　Ｓｐｉ演算的项　０　ｎｉｌｌｅｔ（ｘ，ｙ）＝ＭｉｎＰ　ｐａｉｒｓｐｌｉｔｔｉｎｇ假设有名（ｎａｍｅ）所组成的无限集合，这是安全协议中用来通讯的通道集合；以及有变量（ｖａｒｉａｂｌｅ）所组成的无限变量收稿日期：２００９－１２－２８。郑清雄，硕士生，主研领域：远程演算，安集合。定义Ｓｐｉ演算的项（ｔｅｒｍ）集合如下：全协议。第３期郑清雄：基于Ｓｐｉ

8、演算的安全协议验证２６３ｃａｓｅＭｏｆ０：Ｐｓｕｃ（ｘ）：ＱｉｎｔｅｇｅｒｃａｓｅｃａｓｅＬｏｆ｛ｘ｝ＮｉｎＰｓｈａｒｅｄｋｅｙｄｅｃｒｙｐｔｉｏｎ３　Ｓｐｉ演算的语义进程的基本语义可以做如