STUDY ON THE VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS BASED ON LOGIC
| Project/Area Number |
07650413
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
情報通信工学
|
|---|
| Research Institution | TOKYO INSTITUTE OF TECHNOLOGY |
|---|
Principal Investigator |
KUROSAWA Kaoru FACULTY OF ENGINEERING PROFESSOR, 工学部, 教授 (60153409)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TSUJII Shigeo CHUO UNIVERSITY FACULTY OF SCIENCE AND ENGINEERING, 理工学部, 教授 (50020350)
SATO Takashi TOKYO INSTITUTE OF TECHNOLOGY FACULTY OF ENGINEERING, 工学部, 助手 (30262281)
|
|---|
| Project Period (FY) |
1995 – 1997
|
| Project Status |
Completed (Fiscal Year 1997)
|
| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 1997: ¥300,000 (Direct Cost: ¥300,000)
Fiscal Year 1996: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 1995: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | BAN LOGIC / CRYPTOGRAPHIC PROTOCOL / LOGIC FORMULA / KEY DISTRIBUTION / VERIFICATION / 匿名通信路 / 秘密分散共有法 / secret sharing / 認証コード / グループ署名 |
|---|
| Research Abstract |
This paper shows a new aspect of BAN logic for insecure protocols. That is, we show formulas which some insecure protocols will satisfy. This enables us to identify flaws in insecure protocols systematically. Consider a protocol in which P sends X to Q,where X may be a secret or a secret key. We first show that a protocol suffers from an impersonation attack if
P believes P sees X (]SY.reverse left half-bracket.[)P believes Q says X
is derived. Intuitively, this formula means that there is a possibility that P receives X which Q did not send. This is an impersonation attack where an enemy sends X to P by impersonating Q.Unfortunately, we do not have an inference rule which can derive this formula. We therefore show another formula which can have an inference rule for it. That is, we show that a protocol suffers from an impersonation attack or a replay attack if
P believes P sees X (]SY.reverse left half-bracket.[)P believes Q says X for the first time
is derived, where
P says X for the first time * fresh (X) P says X.
Next, since the BAN logic does not have an inference rule which can derive this formula, we present a new inference rule such as follows.
P believes Q said X (]SY.reverse left half-bracket.[)P believes fresh (X)
(]SY.reverse left half-bracket.[)P believes Q says X for the first time
This is a reasonable inference rule because we prove its soundness.That is, we prove that this rule is true under the semantics of Abadi and Tuttle. Finally, we apply our new inference rule to the Andrew Square RPC Handshake protocol and show how our (second) formula is derived. Then our theorem tells us that the protocol has an impersonation attack or a replay attack. Actually, it is known that it suffers from a replay attack. We also show that our second formula is more powerful than our first formula.
Future work will be to generalize our approach to Spi calculus.
|
Report
(4 results)
Research Products
(8 results)
