STUDY ON THE VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS BASED ON LOGIC

点击翻译按钮获取中文摘要

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 ifP believes P sees X (]SY.reverse left half-bracket.[)P believes Q says Xis 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 ifP believes P sees X (]SY.reverse left half-bracket.[)P believes Q says X for the first timeis derived, whereP 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 timeThis 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.