《安全协议分析与设计 普通高等教育“十一五”国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第4章-上》由会员分享，可在线阅读，更多相关《安全协议分析与设计 普通高等教育“十一五”国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第4章-上（36页珍藏版）》请在金锄头文库上搜索。
1、安全协议分析与设计 第四章（上）,卫剑钒,2,模型检测分析方法,BAN逻辑可以被看做“证明”工具，而模型检测方法则是“证伪”工具。 模型检测方法是一种十分有效的协议形式化分析工具，主要是通过构造攻击来证明协议是不安全的。它可以抽象地描述为：给定模型M和性质P，检查M中P是否成立。 基于攻击的结构性方法对协议进行分析时，一般要借助于自动化工具，从协议的初始状态开始，对合法主体和攻击者所有可能的执行路径进行穷尽搜索，以期找到协议可能存在的错误。,3,CSP方法,通信顺序进程（CSP）是C. A. R. Hoare 为解决并发问题而提出的代数理论Hoar85，它是一个专为描述并发系统消息交互而设计的
2、抽象语言。 Lowe将其用于安全协议的描述与分析，将协议的安全问题描述为CSP 进程是否满足其CSP 规约的问题，并使用FDR对协议的性质进行分析与验证。,4,CSP基本术语,1进程 从通信的角度而言，进程是能执行通信事件的主体，如进程P1在先后执行事件x、y以后，变为进程Stop。 P1=xyStop 其中，Stop是CSP定义的终止进程。CSP定义的终止进程共有两个，另一个是Skip。Stop与Skip表示的终止进程的区别在于Stop表示死锁，而Skip表示成功地终止。,5,CSP基本术语,2信道 CSP把不同事件类型看成不同的信道，并规定它所传递的数据的类型，如通道channel out
3、:T，表示out通道能够输出类型为T的数据。 P2=in?x:Tout.xStop 在上面进程P2的描述中，in?x:T表示只要输入的x为通道in所认可的数据类型T，P2便可执行该in.x事件。而且，一旦in.x事件已经执行，则它的后一事件out.x便可以执行。 “?”表示输入，“!”和“.”都可表示输出，“.”还可表示连接。,6,CSP基本术语,P3为一个循环进程，其描述为 P3=in?x:Tout.xP3 和P2执行完两个事件后终止不同，P3可以执行无限多个in和out事件组成的序列。 进程也可以进一步以参数方式表示，例如 P4(X)=in?x:Tout.xP4(Xx) P4在执行完in和
4、out事件后，参数X集合中多了一个成员x。,7,CSP基本术语,3选择 表示在两个进程事件间的外部选择，如 P5=aP5 P6=bP6 P7=P5P6 P7给外部环境提供了两种选择，如果外部环境选择事件a，则P7如同P5行为；如果外部环境选择事件b，则P7如同P6行为。,8,CSP基本术语,4.并行 一个进程也可能由多个进程（如P和Q）通过共同的事件同步通信而组成，当它们可以互相等待以同时执行事件e时，进程P和Q在事件e上同步。 P|X|Q 表示并行操作，即进程P和Q将在事件集合X的所有事件上同步； P|Q 表示穿插操作，即进程P和Q不在任何事件上同步，它们之间完全相互独立。,9,CSP基本术
5、语,5隐藏 对于一个确定进程P，通常把P的事件分成外部环境可见的事件和外部环境不可见的内部事件。事件的不可见可以通过隐藏操作符“”来实现： PE 表示隐藏操作，E是在进程P的外部环境中被隐藏的事件集，也即E是内部事件。,10,CSP基本术语,6重命名 操作符 表示重命名，Pcc表示P被重命名后的进程，除了被重新命名的事件c外，该进程和P表现一样。例如： P5=P4ac,bd 表示P5除了将P4中的事件a和b分别被替换为c和d外，其他和P4表现一样。 P6=P4ac,ad 表示P4中的事件a在P6中呈现为事件c或者事件d。 重命名机制实现了系统在更高层次的抽象，从而为更简洁地描述系统提供了有效的
6、方法。,11,CSP基本术语,7条件结构（if-then-else） 像很多其他语言一样，有时需要根据进程的中间状态参数做出下一步动作的决定。不同的CSP表达，可能会用不同的符号和形式来处理if-then-else结构，下面的示例是一种直接的表达方式： FW(s) = in?x if valid(x,s) then (out.xFW(newstate(s,x) Else FW(newstate(s,x),12,CSP基本术语,8迹 进程P的迹（trace）是一个事件序列，定义trace(P)为进程P能够执行的外部环境可见的所有迹的集合。例如： 进程Stop的迹为空，因为Stop不能执行任何事件
7、。 trace(P3)为 trace(P3)=，, 进程 P8=aP8，它的迹集合为 trace(P8)=,13,CSP基本术语,9.精炼 当进程Q的迹为进程P的迹的子集时，称进程Q的迹“精练”进程P的迹，记为： P T Q P T Q也即 trace(Q) trace(P)。 通过检验Spec T P，可以检验一个进程P是否能执行该进程规范Spec未定义的事件。,14,FDR工具,FDR（Failures Divergences Refinement）是一个商业工具，可用来分析CSP描述的并行交互系统，FDR接受两个CSP描述作为输入，一个叫做规范，另一个叫做实现。 规范往往表示一个抽象的系
8、统，通常具有一定的性质；而实现则表示一个比较具体的系统，通常希望其具备某种性质。FDR工具的目的就是检查实现是否精练了规范。 FDR工具用于检测进程P的每一个迹也在规范进程Spec的迹集合中，为了验证一个规范进程Spec是否被实现进程Impl进一步精练，FDR采用广度优先方法搜索两个进程的状态空间，如规范要求满足某性质，穷举实现的所有可能看是否有不满足的；或者规范声称一定不具有某性质，穷举实现的所有可能看是否有满足的。如果精练检验失败，FDR将给出反例的迹。,15,CSP描述-示例1,Stop 所有进程中最简单的进程是Stop，这个进程不进行任何动作，没有中间动作，也没有可见动作。它可以作为那
9、些不接受任何外部通信的进程的等价进程，如死锁现象，在这种情况下，并行进程对下一个动作不能达成共识，就与Stop等价。,16,CSP描述-示例2,下面几个进程都很简单，并且彼此等价，都描述了依次执行动作to和fro的过程，只要环境允许，将一直运行下去。 Alt=to-fro-Alt Malt1=to-Malt2 Malt2=fro-Malt1 Dalt=to-fro-to-fro-Nalt Nalt=to-fro-Dalt,17,CSP描述-示例3,一个可以编码的机器CM1。 此机器有两个参数，一个参数是内部状态s，另一个是关键值，关键值的取值范围在Loff内，L是字母表，所谓字母表即可选的值的
10、集合。 CM1(s) = ?x:LoffCM1(s,x) CM1(s,off) = Stop CM1(s,x) = crypt(s,x) CM1(newstate(s,x) xL M从外部接收属于集合L或off的一个事件，然后进入进程CM1(s,x)。如果接收的是off，就进入停机状态;如果不是off，则输出crypt(s,x)，然后进入新状态newstate(s,x) 。,18,CSP描述-示例4,定义数据类型为L的输入和输出信道in和out，不考虑事件off的情况，编码机器可改写为 CM2 (s) = in.x:Lout.crypt(s,x) CM2(newstate(s,x) 这个进程和
11、CM1唯一的不同是没有停机状态。,19,如果A=BC，则以下两个进程等价： ?x:AP(x) = (?x:BP(x) (?x:CP(x) 如果上式中B为空集，则?x:BP(x)和Stop等价，因为环境所给的任何值都不会被接受。 由于A=A空集，则 ?x:AP(x) = (?x:AP(x) Stop 事实上，PStop和P是等价的，因为Stop不接受任何输入，所以等式右边的行为就和左边完全一样。,CSP描述-示例5,20,CSP描述-示例6,将off添加回CM2，可得CM3如下： CM3(s) = (in?x:Lout!crypt(s,x) CM3(newstate(s,x) (in.offSt
12、op) CM3(s)的功能和CM1(s)一样。,21,CSP描述-示例7,考虑一对缓冲进程： BA=left?xmid!xBA BB=mid?xright!xBB BA和BB之间的接口是信道mid，因此两者的联合可写为 B2 = BA|mid|BB mid表示mid信道上所有可能出现的值的集合。 BA从信道left接收信息，然后经过mid信道转发到BB。对于BA和BB来说，mid是它们的和外部通信的信道，但是一旦两个进程组合成B2，对于B2来说mid可以被看做内部信道，mid上的事件也可被看作内部事件。应用隐藏符号，B2mid就使得mid上的事件变为内部事件。,22,CSP描述-示例8,在示例
13、7的缓冲区进程中： BA=left?xmid!xBA BB=mid?xright!xBB 两个进程的行为实质是一样的，只不过是所用的信道不同。故可以这样定义： BB=BAleftmid, midright 表示把BA中的left变为mid，mid变为right。这样就间接定义了BB。更进一步，可以定一个一般的进程： B=in?xout!xB 然后用重定向的B描述BA、BB： BA=Binleft, outmid BB=Binmid, outright,23,协议保密性的描述,如果要求m具有保密性，则m不能被正常通信者以外的用户得到。具体方法是插入一个声明Claim_secret到协议描述的结尾
14、，并进行检测，如果可以确认没有攻击者可以在协议的运行中获得m，则说明该协议对m有保密性。,24,协议认证性的描述,CSP模型检测方法对认证性的检测类似于Woo和LamWL93提出的一致性（correspondence）要求，即要求协议主体双方按照一定的锁定步骤（locked-step）运行协议，协议的身份认证目标被表述为下列断言的成立： ( i, EndInit( r ) ) = ( r, BeginRespond( i ) ) ( r, EndRespond( i ) ) = ( i, BeginInit( r ) ) 符号“=”表示“之前有”， ( i, EndInit( r ) )表示发
15、起者i完成了对响应者r的协议运行; ( r, BeginRespond( i ) )表示响应者r开始了对发起者i的协议运行; ( r, EndRespond( i ) )表示响应者r完成了对发起者i的协议运行; ( i, BeginInit( r ) )表示发起者i开始了对响应者r的协议运行。,25,Yahalom协议,26,发起者的进程,Initiator(a,na)= env?b: Agentsend.a.b.a.na (kabKey, nbNonce, mT)( receive.s.a.b.kab.na.nbkas.m send.a.b.m.nbkab session(a,b,kab,n
16、a,nb) ),27,env?b: Agent表示a的运行环境（env）要求发起一个对b的协议运行，b是一个类型为Agent的响应者。 send.a.b.a.na表示a发送给b消息a.na。send表示发送信道，send后紧跟的是发送者，然后是接收者，最后是发送的消息。 (kabKey, nbNonce, mT)()表示外部选择满足kabKey, nbNonce, mT的变量，然后a使用这些变量，按照()里的规定执行协议。 session(a,b,kab,na,nb)表示在Yahalom协议执行完毕后，获得了会话密钥和其他信息，并用此进行实际应用的会话运行。,28,响应方的进程,Responder( b, nb )= ( kab
