权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

STUDY ON THE VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS BASED ON LOGIC

基于逻辑的密码协议验证研究

基本信息

批准号：
07650413
负责人：
KUROSAWA Kaoru
金额：
$ 1.6万
依托单位：
TOKYO INSTITUTE OF TECHNOLOGY
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至 1997
项目状态：
已结题

项目摘要

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.

本文展示了BAN逻辑在不安全协议中的一个新方面。也就是说，我们给出了一些不安全协议将满足的公式。这使我们能够系统地识别不安全协议中的缺陷。考虑一个协议，其中P将X发送给Q，其中X可以是一个秘密或一个秘密密钥。我们首先表明，如果P认为P看到X (]SY)，协议就会遭受模拟攻击。倒左半括号。[)P相信Q说x是推导出来的。直观地说，这个公式意味着P有可能收到Q没有发送的X。这是一种模仿攻击，敌人通过模仿q将X发送给P。不幸的是，我们没有一个推理规则可以推导出这个公式。因此，我们给出了另一个公式，它可以有一个推理规则。也就是说，如果P认为P看到了X (]SY，则表明协议遭受了模拟攻击或重放攻击。倒左半括号。[)P认为Q第一次说X是推导出来的，而P第一次说X * fresh (X) P说X。接下来，由于BAN逻辑没有可以推导出这个公式的推理规则，我们提出如下的新推理规则。P相信Q说过X。倒左半括号。[] P相信新鲜的(X)(]SY。倒左半括号。[)P相信Q第一次说了X，这是一个合理的推理规则，因为我们证明了它的合理性。也就是说，我们在Abadi和Tuttle的语义下证明了该规则为真。最后，我们将新的推理规则应用于Andrew Square RPC握手协议，并展示了我们的（第二个）公式是如何推导出来的。然后我们的定理告诉我们，该协议存在模拟攻击或重放攻击。实际上，众所周知，它遭受了重放攻击。我们还证明了第二个公式比第一个公式更有效。未来的工作将是推广我们的Spi演算方法。