STUDY ON THE VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS BASED ON LOGIC

1997 Fiscal Year Final Research Report Summary

• 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
• Keywords: BAN LOGIC / CRYPTOGRAPHIC PROTOCOL / LOGIC FORMULA / KEY DISTRIBUTION / VERIFICATION

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.