网络安全协议的形式化分析与验证 作者 李建华 第三章 基于模型检测技术的安全协议分析方法.pptVIP

3.6.1 BRUTUS协议描述模型 2．实例 BRUTUS将协议描述为由诚实主体及入侵者的通信进程构成的异步组合，并认为通信媒介是不安全的，即通信主体的所有发送和接收消息都在入侵者的控制中。 在BRUTUS协议模型中，协议的一次运行称为“会话（Session）”，在一个会话中每个参与者都会按其在协议中的角色（如发起者或响应者）进行实例化（Instantiating），所以，一次会话是由所有参与者的实例（Instance）构成的。一个实体可以有多个实例，但一个实例只能运行一次。 协议模型就是由所有的实体实例及入侵者实例构成的。 3.6.1 BRUTUS协议描述模型 每个诚实主体的实例被描述为一个5元组N,S,I,B,P， N是主体的名称； S是唯一的实例号； B是对变量集的限制，设实体N的变量集合为vars(N)，则B:vars(N)→M； I ?M，表示实体在运行实例时所知道的消息的集合； P是实体执行操作的进程描述，所执行的操作既包括预定义的动作“send”和“receive”，也包括用户自定义的内部动作，如“commit”和“debit”等。 3.6.1 BRUTUS协议描述模型 入侵者Z的描述与之类似，但由于入侵者可以不按照协议运行，因此，它不包含动作序列PZ，也不包含限制集合BZ。另外，在任一时刻，入侵者可接收任意消息，也可以根据已知消息集IZ产生新的消息。综上，入侵者的实例可以表示为SZ=NZ, SZ, ?, IZ, ?。 所有实体实例及入侵者实例的异步组合就构成了协议的全局模型，该模型的每一次可能的执行称为“迹(Trace)”。迹可以表示为由全局状态和执行动作交替组成的一个有限序列，即 ， 。 3.6.1 BRUTUS协议描述模型 3．动作 在协议执行过程中包括send和receive两个预定义的动作，还包括一些用户自定义的动作。 协议模型中全局状态的迁移就是实例执行动作的结果。 状态迁移关系“→”可形式化地定义为?? ?×S×A×M×?，其中，?表示全局状态的集合，S是实例标识集，A是动作集，M是消息集。 为方便起见，一般将5元组元素表示为 。全局状态可表示为?=Z,H1, H2,…,Hn，其中，Z是入侵者的实例，Hi(1?i?n)是诚实主体的实例。 可将对变量集的限制B扩展为对消息模板的限制 ，即 (m)是将B(v)中的v用消息模板中含有v的m来代替。 3.6.1 BRUTUS协议描述模型 BRUTUS模型中所有合法的状态迁移有 1） ，在状态?时，实例s能够发送消息m，并达到新的状态??，当且仅当： ① ，即入侵者将m加入他所知道的消息集中。 ② 在?中有一个实例Hi=Ni,s,Bi,Ii,send(s?msg)?Pi? ，使得迁移之后的状态 为 ，Hi =Ni,s,Bi,Ii, Pi? ，并且m= (s?msg)，即一个实例准备发送消息m，在下一个状态中将把该发送动作从其动作序列中删除。 ③ Hj=Hj?，当j?i时，即所有其他的进程都将保持不变。 3.6.1 BRUTUS协议描述模型 2） ，在状态?时，实例s能够接收消息m，并达到新的状态 ，当且仅当： ① ，即入侵者能够产生消息m。 ② 在?中有一个实例Hi=Ni,s,Bi,Ii,receive(r?msg) ?Pi?，使得迁移之后 的状态为??，Hi =Ni,s,Bi?,Ii?,Pi?，Ii?=Ii∪m， ?(r?msg)=m，即一个实 例准备接收消息m，在下一个状态中，其限制也将被修改，同时把该接收动作也从其动作序列中删除。 ③ Hj=Hj? ，当j?i时，即所有其他的进程都将保持不变。 3.6.1 BRUTUS协议描述模型 3） ，在状态?时，实例s能够执行用户定义的内部动作A（其参数为m），并达到新的状态 ，当且仅当： ① 在?中有一个实例Hi=Ni,s,Bi,Ii,A(msg)?Pi? ，使得迁移之后的状态 为??，Hi =Ni,s,Bi,Ii,Pi?，m= (msg)，即一个实例准备执行动作A， 在下一个状态中，该动作将被从其动作序列中删除。 ② Hj=Hj? ，当j?i时，即所有其他的进程都将保持不变。 3.6.1 BRUTUS协议描述模型 BRUTUS采用一阶