| Project/Area Number |
12133204
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Review Section |
Science and Engineering
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
YONEZAKI Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Professor, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
YOSHIURA Noriaki Gunma University, Computer Center, Associate Professor, 総合情報処理センター, 助教授 (00302969)
NISHIZAKI Shin-ya Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Associate Professor, 大学院・情報理工学研究科, 助教授 (90263615)
YONEDA Tomohiro National Institute of Informatics, Infrastructure Systems Research Division, Professor, 情報基盤研究系, 教授 (30182851)
TOMOISHI Masahiko Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Assistant Professor, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥40,500,000 (Direct Cost: ¥40,500,000)
Fiscal Year 2003: ¥8,400,000 (Direct Cost: ¥8,400,000)
Fiscal Year 2002: ¥16,400,000 (Direct Cost: ¥16,400,000)
Fiscal Year 2001: ¥15,700,000 (Direct Cost: ¥15,700,000)
|
|---|
| Keywords | Safety critical system / specification analysis / safe program synthesis / network security analysis / security protocol / secure system architecture / security of cryptographic primitives / verification and synthesis of hardware / 安全性検証 / 暗号方式 / ネットワークセキュリティ / Dos攻撃 / 非同期回路 / コード生成 / 検証 / DoS攻撃 / インテグリティ解析 / JAVA / 実現可能性 / セキュリティープロトコル / 耐攻撃性 / インテグリティー解析 |
|---|
| Research Abstract |
Our research results fall into fourfold.
1)Verification and synthesis method for keeping safety of reactive systems. We developed verification methods for specifications of reactive systems. These verification systems examine whether a specification satisfy the condition that for any infinite behavior of environment, the reactive system can properly react against it forever. We found various techniques for the implementation of an efficient verification system.
2) Network security. We defined an axiomatic system that can verify security properties of security protocols. Based on this inference rules, we also design construction rules for security protocols. By introducing several criteria of costs of protocols, optimized protocols are generated for each purpose. We also developed an analysis method for fairness of auction protocols. A new computational model is introduced, with which we can analyze the resistivity of the system for this kind of attack.
3) Construction of secure system arc
… More
hitecture. Once an intruder succeeds to get privilege of the super-user, he can easily intrude connecting other systems by abusing user switching mechanism. For this security problem, we gave a solution in which the user interfaces of other system components are unchanged but we introduced user authentication mechanism to the user switching mechanism. The intruder trying to avoid this mechanism is also detected in our system.
4) Fundamental theories. We analyzed various encryption schemes and hash functions in axiomatic way and strictly formalized various security properties e.g. partial information of contents in cipher text cannot leak out. We also proved their sufficient conditions. Analysis of such security properties in axiomatic way is new and is not found anywhere. For verification of reactive systems, we gave a proof method for temporal logic of finite frames and prove its completeness. It is not trivial to give the complete proof method because finiteness is not first order definable. Less
|
