3.2 BAN逻辑基本概念[2]

《3.2 BAN逻辑基本概念[2]》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第三章选取Kerberos协议的核心子集3.1选取需要实现的核心子集由于Kerberos协议非常庞大，经过了多年的修订发展，集中了许多人的智慧，受到了各大厂家的广泛支持，经过了时间的考验，其设计思想经受了千锤百炼。在有限的时间内全部实现是非常困难的，所以通过简化Kerberos的基本认证过程，产生了一个核心子集:l.Client->AS:c,怡s,Te2.AS->Client:(Kc,tgs,Tc,Tas}Kc,(Tc,tgs)Ktgs3.Client->TGS:(Ac,Nc)Kc,tgs,(Te,tgs)K

2、tgs,s,Tas4.TGS->Client:(Kc,s,Tc,Ttgs)Kc,tgs,(Tc,s}Ks5.Client->AP:(Ac,Ttgs}Nc)Kc,s,(Tc,s)Ks6.AP->Client:(timestamp+I,Nap)Kc,s(Optional)其中简化后的Ticket和Authenticator分别包含:Ticket;ClientName;RequestedServiceName;StartTimethattheticketcomesintoefect;ExpirationTime;S

3、essionKeyAuthenticator:ClientName;ClientIP;CurrentTime3.2BAN逻辑的基本概念1213.2.1基本符号实体:>'Q,R5共享密钥:Kab,Kas,Kpq公开密钥:Ka,Kb,Kp秘密密钥:Ka一，，Kb一，，Kp-'公式:X,Y任意密钥:K临时值:Na,Nb.Nc消息:m_M，X,Y3.2.2基本公式(1)PbelievesXP相信X是真的，而X本身既真既假，但P把X当做真的。(2)PseeXP已经接收到消息X.假如P有相应的解密密钥，那么他能够读出它的

4、内容，同时P亦把X发送给其它实体。(3)PsaidXP己经发送消息X,P相信他发送的X是真的。(4)PcontrolsXP对X有判定权，即P是对X的真的可信任的当局。(5)fresh(X)X是新鲜的。时间分为两个时段:过去与现在。而现在则以当前协议执行的起点为起点。当X不包含在过去发送的消息中，X是新鲜的。(6)Pc-x与QK是P和Q共享的密钥。K是P,Q之间通信的安全密钥，除P,Q之外，其它实体包括P,Q信任的实体都不能破译。(7)一二-iPK是P的公开密钥。(8)(X)‘X以K加密，{X);表示以K加密于

5、X后的消息。它是的{xXP)K简写，P表示消息发送源的实体。有时省略P是为了表明每个实体能够识别属于自己的消息。(9){X>Y(X,Y)nY是某种秘密。(14)(X,Y)X与Y链接。(11)H(X)X是单向杂凑函数3.2.3逻辑公设BAN逻辑主要有如下5条逻辑公设:1消息含义法则逻辑公设PbelievesQ+-}}-*P,Psees(X)k=:>PbelievesQsaidX这一逻辑公设说明:如果P相信K是P和Q之间的共享密钥，且P曾收到用K加密X后的结果，那么P相信Q曾发送过X.对于公开密钥，有类似的公设P

6、believesI=r>Q,Psees{X}k一‘=:>PbelievesQsaidX2.临时值校验法则逻辑公设Pbelievesfresh(X),PbelievesQsaidX=>PbelievesQbelievesX这一逻辑公设说明:如果P相消息X是新的，且P相信Q曾发送过X，则P相信Q相信X.3.管辖法则逻辑公设PbelievesQcontrolsX,PbelievesQbelievesX==>PbelievesX这一逻辑公设说明:如果P相消息X是新的，且P相信Q曾发送过X，则P相信Q相信X.4，逻辑公

7、设Psees(X,Y)=>PseesXPseesy=>PseesXPbelievesQ+-E-4P,Psees{X}K=:>PseesXPbelievesIK>P,Psees厦X)‘=:>PseesXPbelievesJ}Q,Psees(X}‘一，=*PseesX上述逻辑公设说明:如果一个主体曾经收到一个公式，且该主题知道相关的密钥，则该主题曾收到该公式的组成部分。5逻辑公设Pbelievesfresh(X)=:>Pbelievesfresh(X,钓上述逻辑公设说明:如果一个公式的一部分是新的，则该公式

8、全部是新的。3.3采用BAN逻辑证明核心子集的完备性3.3.1初始假设集合(1)ClientbelievesClienti-K'oAS(2)Clientbelievesfresh(Tc)(3)APbelievesfresh(Ttgs)