STUDY ON THE VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS BASED ON LOGIC
Project/Area Number  07650413 
Research Category 
GrantinAid for Scientific Research (C)

Allocation Type  Singleyear Grants 
Section  一般 
Research Field 
情報通信工学

Research Institution  TOKYO INSTITUTE OF TECHNOLOGY 
Principal Investigator 
KUROSAWA Kaoru FACULTY OF ENGINEERING PROFESSOR, 工学部, 教授 (60153409)

CoInvestigator(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 halfbracket.[)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 halfbracket.[)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 halfbracket.[)P believes fresh (X) (]SY.reverse left halfbracket.[)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
(4results)
Research Output
(8results)