Computational Logical Verification Method for Cryptographic Protocols
| Project/Area Number |
21700023
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
HASEBE Koji 筑波大学, システム情報系, 助教 (80470045)
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2011: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2010: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2009: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
|
|---|
| Keywords | 仕様記述 / 仕様検証 / 形式手法 / 暗号プロトコル / 安全性検証 / 論理推論 / 計算論的安全性 / 数理的技法 / 計算論的安全性証明 |
|---|
| Research Abstract |
We developed an extended inference system based on Based Protocol Logic (BPL), a variant of first order logic for proving correctness of cryptographic protocols. This extended system was obtained from BPL by adding some computational aspects of cryptography and sound with respect to a computational semantics. We also demonstrated the usefulness of this system by proving secrecy property of some protocols, such as Needham-Schroeder protocol.
|
Report
(4 results)
Research Products
(8 results)
