【作者】 王巧丽；

【导师】 李祥；

【作者基本信息】 贵州大学 ， 计算机软件与理论， 2006， 硕士

【摘要】 软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一，尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety—critical)领域更是如此。这类系统要求绝对安全可靠，不容半点疏漏，否则将导致灾难性后果。如1861年8月英国克莱顿隧道事故，就是由于协议的不完整性造成的，还有1996年6月4日，欧洲航天局阿丽亚娜(Ari—ane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜，如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。 据统计，在美国每年要花去3000亿美金用来雇佣程序员专门来解决程序的BUG，而这个工作就占据了整个产品开发周期40％～60％的时间。尽管花费了这么大量的人力和物力来排除BUG，他们还是不能保证软件没有错误。 为了从根本上保证软件系统的可靠安全，包括图灵奖得主A．PnDeli在内的许多计算机科学家都认为，采用形式化方法(formalmethds)对系统进行形式化验证和分析，是构造可靠安全软件的一个重要途径。模型检测技术是形式验证方法中的一种。而获得ACM(Association for Computing Machinery)软件系统奖(Software Systems Award)的SPIN就是著名的模型检测工具之一。 典型的SPIN工作模式是首先对并发式系统或分布式算法的规范建立高标准的模型，在确认没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为，然后SPIN产生一个用C语言描述的验证程序，经检验机编译后被执行，执行中如果发现了违背正确性说明的任何反例，则反馈给交互模拟机，通过重现细节剔除引起错误的原因。 本文首先详细介绍了著名的模型检测工具SPIN的历史、发展与特点，讨论了使用SPIN对网络通信协议分析的方法。本文所做的主要工作、技术难点与创新处如下： ● SPIN(Simple Promela Interpreter)是适合于并行系统，尤其是协议一致性的辅助分析验证工具，本文讨论了在Win32下和Cygwin／Linux／Unix下对SPIN的安装和使用。 ● 使用SPIN的最简单的方式是使用图形界面XSPIN，图形界面独立于SPIN运行，辅助产生和选择相应的SPIN命令，XSPIN在后台运行SPIN得到期望的输出值，XSPIN知道什么时候怎么样去编译模型检测的代码，也知道什么时候如何去执行它，所以可以不用记住所有的参数。本文介绍了在Cygwin下安装和使用SPIN的图形界面工具XSPIN。 ● Promela(Protocol／Process Meta Language)是用来对有限状态系统进行建模的形式描述语言，本文阐述了如何使用Promela语言对协议进行描述。 ● AB协议是最早的端到端的通信协议之一，用SPIN对AB协议进行分析从而得到协议中不容易发现的错误。 ● 使用SPIN的图形界面XSPIN对上述协议进行分析得到直观的进程之间信息的交互图。 ● SPIN不仅可以用来验证协议的正确性，也可以对身份验证协议进行有效的攻击检测。本文讨论了在网络保密通信中使用密钥分配中心KDC系统时的攻击问题，用Promela语言建立了KDC的模型，使用LTL描述其性质，用SPIN进行模型检测验证，使用XSPIN得到协议受攻击的轨迹图形。 ● 对NSSK协议进行建模和分析，得到协议受攻击的轨迹。对Woo_Lam协议进行建模和分析，得到协议中潜在的两个受攻击轨迹。更多还原

【Abstract】 Whether the software is credible has become one of the crucial factors for the national economy and national defence etc., especially in some safety-critical fields such as the control of nuclear reactor, aerial navigation and railway attempter. These systems require absolute safety and no error is permitted, or else terrible result may occur. For example, Clayton Tunnel Accident in August 1861 just resulted from half-baked protocol. And on June 1996, Europe spaceflight department, rocket Ari-ane 501 exploded 37 seconds after being fired, due to the bugs in its specification and design of the control. Similar reports are common occurrences. How to ensure the dependability of these systems has become a focus problem in computer science and cybernetics field.According to statistics, in America, $3000 hundred million will be spent in employing programmer to deal with the bug, which took up 40%~60% of the whole development period. Although so much time and energy has been consumed in demolishing bugs, they can’t ensure bugs are removed from the software.With the aim to ensure the credibility and safety of the software system radically, many computer scientists, including A. PnDeli, a gainer of Turing Award, believe that it is an important way to construct safe software through validating and analyzing the system by formal methods. Model checking technology is one of the validating ways. And SPIN, which is a gainer of Association for Computing Machinery Software Systems Award, is one of the most famous model checking tools.SPIN’S typical mode of working is to start with the specification of a high level model of a concurrent system, or distributed algorithm, typically using SPIN’S graphical front-end XSPIN. After fixing syntax errors, interactive simulation is performed until basic confidence is gained that the design behaves as intended. Then, SPIN is used to generate an optimized on-the-fly verification program from the high level specification. This verifier is compiled, with possible compile-time choices for the types of reduction algorithms to be used, and executed. If any counterexamples to the correctness claims are detected, these can be fed back into the interactive simulator and inspected in detail to establish, and remove, their cause.In the front of this paper, the history, development and characteristics of SPIN, a famous model detection tool, are introduced. Promela, the SPIN modeling language, is followed. The installation of UNIX edition SPIN PIN in Windows 2000 through Cygwin is discussed in this paper. As follows, AB-protocol is described and we found the false and the leak. Finally, the course of analyzing crypto protocol by Promela designing is pointed out, and the potential attack was found. This paper includes the main doing work, the deep technique, and the creative work as follows: SPIN is a model checker for the verification of concurrent algorithms systems, especially is that auxiliary tools for analyzing agreement consistency. In this paper we discuss that how to setup and use SPIN in the Win32 environment and in the Cygwin/Linux/Unix environment. The simplest way to use SPIN is to use XSPIN, which has graphical interfaces. Graphical interfaces run without using SPIN and choose corresponding orders of SPIN. XSPIN gets anticipant output-answers through running SPIN in the background. XSPIN knows when and how to compile the code and it also knows that how to run the code, so you needn’t to remember all the parameters. The paper introduces how to install and use XSPIN, the GUI of SPIN, on Cygwin platform. Promela (Protocol/Process Meta Language) is a formal descriptive language, which is written to make model of the finite states system. The paper introduces how to describe a更多还原