Elementary Studies on Formal Description and Verification of Security Protocols

近年来，计算机网络系统遍布世界各地，我们在日常生活中越来越依赖它们。网络应用，特别是电子商务、远程医疗等高级网络应用，对网络系统的安全性提出了更高的要求。然而，由于并发系统（如计算机网络系统）的非确定性行为，其功能和性质难以保证，本研究试图应用形式化方法来保证包括计算机网络系统在内的大型复杂系统的功能和性质。我们把SSL（安全套接字层）协议版本2作为一个真实的安全协议的例子。我们用RAISE规范语言RSL（RAISE Specification Language）对其进行了形式化描述。在此基础上，提出了一种新的网络安全认证方法，并在一个实验系统上对该方法的功能和可行性进行了评估。我们在计算机网络上设计了一个应用程序，它需要用户身份验证和安全性。它通过互联网提供多媒体内容。我们在另一个实验网络系统上实现了一个原型系统，用进程代数扩展了形式化规范语言Z，提出了一种描述和分析并发系统行为的统一方法。并将其应用于分布式系统中内存一致性模型的描述与验证。

Recently, computer network systems spread all over the world and we depend on them more and more in every day life. Network applications, especially advanced ones such as electric commerce and remote medical care, require sufficient security on the network systems. It is, however, difficult to assure the functions and properties of concurrent systems such as computer net work systems because of their non-deterministic behaviors.In this research, we intended to apply formal methods to assure the functions and properties of large-scale and/or complicated systems including computer network systems. We treat SSL (Secure Socket Layer) Protocol Version 2 as a real example of security protocol. We described its formal specification with RSL (RAISE Specification Language). We also verified some of its correctness and security properties.More generally and practically, we proposed a new approach to network security and authentication, and evaluate its functions and feasibility on an experimental network system. We designed an application program on computer networks which would require user authentication and security. It delivers multi-media contents through the Internet. We implemented a prototype system on another experimental network system.We extended a formal specification language Z with process algebras, and proposed a unified approach to describing and analyzing behaviors of a concurrent system. We applied it to description and verification of a memory consistency model in distributed systems.