2016 Fiscal Year Final Research Report
Formal verification of anonymity for timed security protocols
| Project/Area Number |
26330166
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Information security
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 匿名性 / 実時間システム / 形式手法 / 検証 / 定理証明 / セキュリティプロトコル |
|---|
| Outline of Final Research Achievements |
Recently, many real-time systems such as smartphones, intelligent robots, and vehicular software are connected to the Internet, and they are running security protocols that deal with privacy-related information. Hence, it is getting more important to establish the anonymity of real-time systems. In this study, we are interested in a formal verification for the anonymity of timed security protocols. Compared with the anonymity of untimed systems, the timed anonymity property was not investigated well, since there are some difficulties in modeling of timed anonymity. In this study, we provided a formalization of timed anonymity, and we developed a proof technique for the timed anonymity of security protocols. Our technique is based on I/O-automaton theory, and the theory provides computer-assisted theorem proving tools. With such tools, we can theorem-prove the timed anonymity of security protocols.
|
| Free Research Field |
形式手法，セキュリティ検証
|
