串空间

串空间（strandspace）学生：倪远1401120354电子与通信工程内容1.引言2.串空间理论框架3.攻击者能力描述4.串空间理论应用举例1.引言1998年，Thayer,Herzog和Guttman提出了一种新型有效的协议形式化分析方法————串空间（strandspace）这个形式化分析方法集NRL协议器，Schneider秩函数以及Paulson的归纳思想于一体。提供了避免状态爆炸问题、提高协议形式化分析效率的有效方法1.串（strand）是协议中的某个合法主体或攻击者行为事件的一个序列，由发送和接收消息组成。◆对于一个诚实的主体，串表示其在某轮协议中的行为。如果其在一段时间内参与了多轮协议，则用不同的串表示。不同主体用不同的串表示。◆攻击者的串中的行为由其已获知的消息的发送和接收行为组成2.串空间（strandspace）是一个串的集合，包括不同协议合法主体的串以及攻击者的串3.簇（bundle），是串空间的一部分，包括合法和不合法的串，这些串通过发送和接收同一消息相连。串与簇具有不同的结构。具体而言，串是线性结构，表示一个主体发送与接收消息的序列；而簇是图结构，表示诸多串之间的通信。串与簇的区别术语：在协议中主体间交换的可能信息组成的集合，记作A。t0⊂t1表示t0是t1的一个子术语。在一个协议中，主体既可发送也可接收术语。定义2.1一个符号术语是一个二元对σ,α,其中α∈A，σ符号为+或-。记为+t或-t。（±A）*是有限序列符号术语s集合，其元素记为〈〈σ1,α1〉,⋯,〈σn,αn〉〉,定义2.2A上的串空间是集合Σ和一个路径映射：tr：Σ→（±A）*，其中Σ是一个串的集合（串空间）基本概念定义2.3构造一个串空间∑（1）一个节点n表示成一个二元对s,i,s∈Σ,i是整数,1≤i≤length(tr(s)),结点集合为N.s,i属于s,每一个结点都属于唯一的一个串.(2)如果n=s,i∈N,那么index(n)=i且strand(n)=s,串s轨迹的第i个有符号项term(n)是(tr(s))i;无符号项un_term(n)是((tr(s))i)2.(3)如果n1,n2∈N,那么n1→n2意味着term(n1)=+a,term(n)=−a2,即n1发送消息,n2接受消息.(4)如果n1,n2∈N,那么n1⇒n2意味着n1,n2发生在同一个串上,n1是n2的直接前继,有index(n1)=index(n2)-1.(5)一个无符号项t发生在n∈N,当且仅当t⊂term(n).(6)一个无符号项t起源在n∈N,当且仅当term(n)是正号,t⊂term(n),而且对同一个串上n的任何前继n′没有t⊂term(n′).(7)一个无符号项t唯一起源在n∈N,当且仅当t起源在唯一的结点n∈N.(8)N加上两种边集合n1→n2和n1⇒n2就组成一个有向图,N,(→∪⇒).(9)n1⇒+n2表示在同一个串上n1经过一个或多个⇒边到达n2.(10)假设I⊆A是一个无符号项集,节点n∈N是I的一个入口点当且仅当term(n)=+t,(t∈I),且对于任意n之前的节点n1,term(n1)∉I.簇和因果次序设C是一个有向图,C中有两种边→和⇒,NC是C的结点集合.如果下面条件满足,则说C是一个簇(bundle).如果：1.C是有限的.2.如果n2∈NC,且term(n2)是负号,那么有唯一的结点n1满足n1→cn2.3.如果n2∈NC,且n1⇒n2,那么n1⇒cn2.4.C是无环的.上述定义形式化了一个通信进程，具有如下三个特性：1.一个串可以发送或接收消息，但不能同时做2.当一个串收到一个消息m时，唯一存在一个节点发送了消息m3.当一个串发送一个消息m时，许多串将立即收到此消息定义2.4一个节点n在簇C=〈Nc,(→c∪⇒c)〉中,记做n∈C.若一个串的所有节点都在C中则称这个串在C中.若C是一个簇,则一个串s的C-height是使得〈s,i〉∈C最大的i的值.定义2.5假设S是一个边的集合,S⊂→∪⇒,定义S上的一个二元关系s,n1,n2∈N,如果有n1→n2或者n1⇒n2,记做n1sn2.显然s是S上的一个闭的传递的二元关系,而≤s是S上的一个闭的传递的自反的二元关系.引理1假设C是一个簇,则≤c是一个偏序（非对称，可传递）.≤c表示因果次序，因为只有当n'的出现是n的出现造成的时候，n≤sn'才成立。每一个C的节点的非空子集都有≤s最小元.引理2假设C是一个簇,S⊆C是一个节点集.若n是S的一个≤c最小元,则n的符号为正.引理3假设C是一个簇,t∈A,且n∈C是集合{m∈C:t∈term(m)}的最小元,则t产生于节点n.术语和加密首先给出已知的假设：（1）原子消息集合T⊆A（2）与T不相交的密钥集合K⊆A（3）两个二元操作：encr:K×A→Ajoin:A×A→A自由假设：(1)若m1,m2∈A且K1,K2∈K,则{m1}K1={m2}K2⇒m1=m2,K1=K2.(2)若m1,m2,m3,m4∈A,K∈K,则m1m2=m3m4⇒m1=m3,m2=m4.m1m2≠{m3}K,m1m2∉K∪T,{m1}K∉K∪T.理想与诚实的定义[5]:如果k⊆K,那么A的一个k理想是A的一个子集,使得对于所有的h∈I,g∈A,K∈k满足:(1)hg,gh∈I;(2){h}k∈I.包含h的最小k理想记做Ik[h].如果S⊆A,Ik[S]=∪x∈SIk[x].命题1假设K∈K,S⊆A,且对任意的s∈S,s∈K∪T∪E且没有{h}k的形式,如果{h}K∈Ik[s],则h∈Ik[s].如果gh∈Ik[S],则g∈Ik[S]或h∈Ik[S].命题2假设C是A上的一个簇,如果m是集合{m∈C:term(m)∈I}的最小元,则m是I的一个入口点.称一个集合I⊆A对于簇C是诚实的,当且仅当如果I有攻击者节点p作为它的入口点,p是M节点或K节点.3攻击者能力描述攻击者能力主要由两方面因素描述:一是攻击者所掌握的密钥集,二是描述攻击者由他所获得的消息产生新消息的能力.其中攻击者所掌握的密钥集由Kp表示,攻击者的基本行为用下面的一个攻击者的迹的集合来描述:M.〈+t〉,这里t∈T,F.〈-t〉,T.〈-g,+g,+g〉,C.〈-g,-h,+gh〉,S.〈-gh,+g,+h〉,K.〈+K〉,这里K∈Kp,E.〈-K,-h,+{h}K〉,D.〈-K-1,-{h}K,+h〉以上描述了攻击者的一些基本能力.基本上可以说对于一个协议的攻击都可以看做是这些基本行为的组合.攻击者在攻击协议的过程中的行为序列也称为攻击者串.如果一个节点属于一个攻击者串称该节点为攻击者节点,否则称为一般节点.命题3令C是一个簇,且K∈K/Kp.如果K不产生于一个一般节点,则对于任意的n∈C,K⊂term(n).特别的对于任意的攻击者节点p∈C,K⊂term(p).考虑集合S={n∈C:K⊂term(n)}.假设S非空然后利用最小元的性质逐个分析攻击者串的迹即可导出矛盾,从而得出S是空集.所以对于任意的n∈C,K⊂term(n),且对于任意的攻击者节点p∈C,K⊂term(p).定理1假设C是A上的一个簇,S⊆T∪K,且K⊆S∪k-1,则Ik[S]对于C是诚实的.4.串空间理论举例NSL协议安全性的证明NSL协议的形式化描述如下:A→B:{NaA}KBB→A:{NaNbB}KAA→B:{Nb}KB定义NSL协议中3种类型的串如下:(1)攻击者串s∈P.(2)发起者串s∈Init[A,B,Na,Nb],迹为(+{NaA}KB,-{NaNbB}KA,+{Nb}KB)(3)响应者串s∈Resp[A,B,Na,Nb],迹为(-{NaA}KB,+{NaNbB}KA,-{Nb}KB)由以上定义,当给定一个串时,可以惟一确定它是攻击者串、发起者串、还是响应者串.安全性证明如下.响应者确认:假设s的第2节点为n0,n0的项为v0,则Nb⊂v0,并且n0的符号为正.又由于〈s,1〉不含有Nb,由前面结论Nb产生于n0.取S={n∈C,Nb⊂term(n)∧v0⊂term(n)}.很明显节点n3属于该集合,因此集合非空存在一个最小元n2.通过检查攻击者迹可知n2是一个一般节点且符号为正.再假设n2在一个一般串t上,Nb是惟一产生于n0的。因为n2≠n0,因此Nb不产生于n2.由此可知在串t上存在n1n2使得Nb∈term(n1).又由n2的最小元性质可知v0⊂term(n1).从串的形式上可以得出term(n1)={NaNbB}KA.并且t是一个发起者串,n1、n2分别为该串上的第2、3个节点,命题4假设Σ是一个NSL串空间,C是∑中的一个簇,s是一个响应者串Resp[A,B,Na,Nb]且高度为3.KA-1∉Kp.Na≠Nb,且Na,Nb惟一产生于2.则C一定包含发起者串t∈Init[A,B,Na,Nb]且高度为3.并且由Na是惟一产生的可知,发起者串是惟一的.同样可以得到发起者的确认:命题5假设Σ是一个NSL串空间,C是∑中的一个簇,s是一个发起者串Init[A,B,Na,Nb]且高度为3.KA-1∉Kp,KB-1∉Kp.Na≠Nb,且Na,Nb惟一产生于Σ.则C一定包含响应者串t∈Resp[A,B,Na,Nb]且高度为2.并且由Nb是惟一产生的可知,响应者串是惟一的.由此,通过串空间理论的分析可得出NSL协议达到了协议身份确认的目的.协议的保密性通过验证随机数Na、Nb的形式可以得到保证Thankyou!Content请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……Content231请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……ContentABCDEtexttexttexttexttextContent请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……请在此添加段落内容……Thankyou!