基于Pi-演算的安全协议的形式化描述和验证论文

2017-03-18

基于Pi-演算的安全协议的形式化描述和验证全文如下：

摘要：形式化论文范文方法对于建模和验证软件系统是一种有效的方法，所以对安全协议的形式化描述和验证是一个重要的研究方向。Pi-演算是一种移动进程代数，可用于对并发和动态变化的系统进行建模;移动工作台MWB(Mobility Workbench)是为Pi-演算开发的一个自动验证工具，可对用Pi-演算等描述的移动并发系统进行分析与验证。本文基于Pi-演算对Aziz-Diffie无线通信安全协议进行形式化分析并使用MWB工具验证此协议存在的攻击。

关键词：移动进程代数;Pi-演算;移动工作台MWB;Aziz-Diffie;无线通信安全协议

本文首先扼要叙述了Pi-演算的基本概念，然后介绍了MWB工具在Windows下的使用并提出了基于Pi-演算协议分析的形式化方法，最后以Aziz-Diffie无线通信安全协议为例说明了如何使用Pi-演算与MWB工具分析安全协议，找出协议攻击。

1 Pi-演算

1.1 名字与进程

设Χ = {x, y, z,a,b,c,…} 是名字(names)的可数集(可将名字看作是通信中的通道channels of communication)，，X，

定义 Pi演算的进程(processes)如下(其中//…为帮助理解的直观说明)：

P:: = 0 //空进程

P|Q //并发(并行)

P+Q //选择

[x=y]P //匹配

.P //沉默(Silent)前缀、内部(Internal)前缀

x.P //输出(Output)前缀

x(y).P //输入(Input)前缀

νx.P //限制(Restriction)

A(x1, x2,…, xn) //代理(Agent)

A(x1, x2,…, xn)是被某P唯一定义的进程(写为A(x1, x2,…, xn) =P，或A(x1, x2,…, xn) = P)，其中x1, x2,…, xn是彼此不同的名字且fn(P){x1, x2,…, xn}。

为减少刮号，约定下列作用顺序：限制与前缀、并发、选择;例如：νx.P|.Q+R应读为((νx.P)|(.Q))+R。

1.2 自由与约束的名字

设P、Q为进程，归纳定义名字集合fn(P)如下：

称为进程P的自由名字集，若，称名字x在进程P中是自由的;如果进程P中的名字x不是自由名字，则称为约束名字，用表示P的约束名字集，记称nP为P的名字集;对，将在P中自由出现的x称为被约束的名字;注意，有P，使，即某个名字x可能同时在P中自由出现与约束出现.

自由名字的代入：对任何进程P，进程P[z/x]是将P里每个自由出现的x改为z而得的进程，称为在进程P里对自由名字x进行代入。

约束名字的改名：(1)对进程的约束名字x可用z改名并将改名结果记为，如果 ;(2)对进程的约束名字x可用z改名并将改名结果记为，如果 ;

注意：对改名的结果并不导致或里的任何名字的自由出现变为约束出现;为防止改名失败，可简单地使用新鲜名字来改名，

2 移动工作台MWB(Mobility Workbench)

2.1 移动工作台MWB(Mobility Workbench)

移动工作台MWB(Mobility Workbench)是针对Pi-演算开发的第一个自动验证工具[5]，可对用多子Pi-演算[2]描述的移动并发系统进行分析与验证;MWB首先在瑞典的Uppsala大学开发;可在Windows、Linux等系统下使用，MWB是开放源代码的。

2.2 PI-演算公式的MWB编码

为将PI-演算公式输入MWB，需将通常的PI-演算公式做一些转换：

对于限制，用代;对于输入前缀，可将写为，称为P的x的抽出(Abstraction)并用代 ; 可写为，称[x]为P的x的凝固(Concretion)。

可用来表示P为：agent = P

A称为P的名，注意P的名可用任意的符号串(例如MyID)，但第一个字母需大写，且(…)里一定要将P的非受限名字完全列举;可将几个MWB公式放到一块以ag为扩展名用ASCII文件存盘。

3 安全协议分析

3.1 进程的性质

一个进程的行为就是这个进程的执行树，一个进程的性质就是对这个进程行为的断言。对于顺序程序来说，它的性质基本上分为两种：程序中止或者程序执行完成并得到结果;但对于并发进程来说，它除了有顺序程序的性质外，还有一些其他性质，比如：程序是否死锁，是否公平等等。

死锁：进程之间由于互相占用对方所需要的资源而都不能继续执行下去的现象，我们称之为死锁

4总结

形式化方法对于建模和验证软件系统是一种有效的方法，对安全协议的形式化描述和验证是一个重要的研究方向。本文使用Pi-演算对Aziz-Diffie无线通信安全协议分析并进行建模，最后使用MWB工具证明出该协议存在攻击，并给出了该协议存在的攻击。

5 参考文献：

[1] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, partI/II. Journal of Information and Computation, 100:1-77, Sept. 1992.

[2] Robin Milner. The polyadic -calculus: A tutorial. Technical Report ECS-LFCS-91-180.

[3]Jens Chr.Godskesen. The Needham-Schroeder Public-Key Protocol—How to Break It:Version 1.0.IT University of Copenhagen March 10,2005.

[4] Bjorn Victor. The Mobility Workbench User's Guide: Polyadic version 3.122. Department of Information Technology, Uppsala University, 1995.

[5] Bjorn Victor. A Verification Tool for the Polyadic -Calculus. Licentiate thesis, Department of Computer Systems, Uppsala University, 1994. Available as report DoCS 94/50.

[6]张玉清，王春玲，冯登国，运行模式法分析ISO/IEC密钥建立协议，通信学报，2005年2月第26卷第2期，P15-18

[7]卿斯汉，认证协议两种形式化分析方法的比较，软件学报，2003年，第14卷第12期，P2028-2036

[8] Horng G, Hsu CK. Weakness in the Helsinki protocol. Electronic Letters, 1998,34:354~355.

[9] Mitchell CJ, Yeun CY. Fixing a problem in the Helsinki protocol. Operating Systems Review, 1998,32:21~24.

[10]卿斯汉，安全协议，北京：清华大学出版社，2005年3月

[11]范红，冯登国，安全协议理论与方法，北京：科学出版社，2003年

[12]A.Aziz，W.Diffie.www.51lunwen.com/jsjaq/ A secure communications protocol to prevent unanthorized access:Privacy and authentication for wireless local area networks[J].IEEE Personal Communications,1994:25-31.

[13]D.Dolev and A.Yao. On the security of public key protocols. IEEE Trans.on Information and Theory,29(2):198-208,1983

[14]Fredrick B.Beste. The Model Prover-a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents, 1998,1,9,29-33

[15] 刘道斌，郭莉，白硕，基于petri 网的安全协议形式化分析,电子学报，2004年11月，P1926-1929