1999 Fiscal Year Final Research Report Summary
Elementary Studies on Formal Description and Verification of Security Protocols
| Project/Area Number |
10680358
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYUSHU UNIVERSITY |
|---|
Principal Investigator |
ARAKI Keijiro Grand. School of Info. Sci. and Electr. Eng., Kyushu University, Professor, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAGUCHI Kenji Chikushi Women's University, Associate Professor, 文学部, 助教授 (30294903)
GOTO Yukinori Grand. School of Info. Sci. and Electr. Eng., Kyushu University, Research Associate, 大学院・システム情報科学研究科, 助手 (40315130)
OKAMURA Koji Education Center for Information Processing, Kyushu University, Associate Professor, 情報処理教育センター, 助教授 (70252830)
張 漢明 財団法人九州システム情報技術研究所, 第二研究室, 研究員
FUKUDA Akira Nara Institute of Science and Technology, Professor, 情報科学研究科, 教授 (80165282)
CHANG Hang-myung Inst. Of Systems and Information Technologies Researcher
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Keywords | Security Protocol / Formal Specification / Verification / Concurrent Systems / Behavior Description / Man in the Middle / Authentication / SSL (Secure Socket Layer) Protocol |
|---|
| Research Abstract |
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.
|
Research Products
(15 results)
