| 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 |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
伊藤 暢浩 愛知工業大学, 情報科学部, 教授 (40314075)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2016: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2015: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| 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.
|
