1、 1 摘 要 网络协议是互联网通信的基本构架， 不完备或错误的协议往往给攻击者提供 了攻击的机会。因为协议本身的高并发性以及所处环境的复杂性，网络协议的设 计是非常困难的。我们可以通过对协议设计完毕后进行安全建模，并进行自动化 验证，来找到协议设计存在的安全隐患。 在本文中， 我们用两种方法分别对 BGP 协议进行建模。 方法一基于规则推理， 对协议进行完全分析，得到协议资源和具有某种推导关系的行为，基本资源可以 作为协议行为的参数，通过用 AND 和 OR 来表示协议行为的推导关系。将此方法 应用到 BGP 协议，最终在 BGP 协议的攻击规则图上得到了 29 条攻击路径。方法 二用 CSP
2、 对协议建模，用 CSP 来表示协议之间各个进程的并发作用，模型包括协 议本身、攻击者，以及所要满足的安全约束。并用 FDR 检验所建立的模型是否满 足约束。用该方法来对 BGP 进行建模验证，检验结果为，该模型满足其中一个约 束，而另一个没有被满足的约束得到了一个反例序列。 本文提出了两种对协议进行分析以及建模的方法，一种是基于规则的，一种 是用形式化的方法来进行建模。通过这两种方法，我们可以用建立的模型来准确 的描述网络协议，使得更好的理解网络协议，并通过对协议的有效分析与验证， 得到协议的攻击方法与协议的缺陷。 关键词：CSP；网络协议；规则；安全建模；BGP 协议 2 ABSTRACT
3、 Network protocol is the basic framework of Internet communications, however, the incomplete or incorrect protocol often provides attackers some opportunities. Because of the high concurrency of a network protocol and the complexity of the environment where it works, it is difficult to design a netw
4、ork protocol with a reliable safety. We can find out a network potentials safety hazard through security modeling and automated verification. In this paper, well use two methods to model on the BGP protocol. The first method bases on the rule-based reasoning approach to analyze the protocol and get
5、protocol resources as well as behaviors which have some kinds of derived relations. The basic resources serve as the parameters of the protocols behaviors and indicates the derived relations by “AND” and “OR”. Applying this method to BGP protocol, we successfully get 29 attack paths on the attacking
6、 rules diagram. The second method is to model with CSP. Well use CSP to indicate the concurrency effect of every process among the protocols. This model contains not only the protocols but also the attackers and the security constraints which need to be satisfied. At the same time, we use FDR to test this model to exam whether it meets the constraints. In this way, we testify the BGP and the result is that one of the two constraints is satisfied while the other is unsatisfied from which we
