Elementary Studies on Formal Description and Verification of Security Protocols

近年来，计算机网络系统遍布世界各地，我们在日常生活中对它们的依赖也越来越多。网络应用，特别是电子商务、远程医疗等高级应用，对网络系统提出了足够的安全要求。然而，由于计算机网络系统等并发系统的不确定性，很难保证它们的功能和性质。在本研究中，我们试图用形式化方法来保证包括计算机网络系统在内的大规模和/或复杂系统的功能和性质。我们将安全套接字层(Secure Socket Layer，安全套接字层)协议版本2视为安全协议的真实示例。我们用RSL(RAISE规范语言)描述了它的形式化规范。提出了一种新的网络安全和认证方法，并在一个实验网络系统上对其功能和可行性进行了评估。我们设计了一个在计算机网络上的应用程序，它需要用户身份验证和安全。它通过互联网提供多媒体内容。我们在另一个实验网络系统上实现了一个原型系统，并用进程代数扩展了一种形式化描述语言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.