安全协议理论与方法.ppt

Denning Sacco密钥分配协议攻击 ■如果B不诚实，它在获得A的证书后,可以冒充A给C发信息，使得C以为A与其共享密钥Kab,将会导致危险发生。 B?S: B,C S?B: Certb,Certc B(A)?C: Certa, Certc, E(Kc: E(Ka-1:Kab,T)) 其他协议 ■SPLICE / AS 认证协议 ■Denning Sacco密钥分配协议 ■SRA three-pass协议 ■Gong双方认证协议 ■加密的密钥交换协议 安全协议的形式化分析 ■目前的技术主要用于对密钥正确的认证 ■安全协议的形式化分析有助于减轻协议设计者的部分工作量： ①. 界定安全协议的边界,即协议系统与其运行环境的界面。 ②更准确地描述安全协议的行为。 ③更准确地定义安全协议的特性。 ④证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。 安全协议形式化分析的历史与现状 ■最早提出对安全协议形式化分析思想的是Needham和Schroeder[NESC78] 。 [NESC78] R.M.Needham and M.D.Schroeder，Using encryption for authentications of large networks of computers. Communications of the ACM,21(12),993-999,1978 ■真正在此领域做出工作的为Dolev和Yao[DOYA83]。 [DOYA83] D.Dolev. And A.Yao. On the security of public key protocols.IEEE Transactions on Information Theory.29(2):198-208,Mar 1983 ■1989年,Burrows,Abadi和Needham提出了BAN逻辑。 安全协议形式化分析的历史与现状 ■以BAN逻辑代表的基于推理结构性方法。 推广应用如GNY逻辑， ■基于攻击结构性方法。研究热点，大量一般目的的形式化方法被用于这一领域。 ■基于证明结构性方法。 有关问题 ■open-ended协议:协议使用的数据结构固定。只有协议并行执行的数目和攻击者为创建一个消息而执行的操作数不受限制。 ■拒绝服务:指攻击者开始一个协议之后就放弃，造成合法的协议请求不能接受。 ■匿名通信:防止“旁观者”了解信息来源和去向。 ■高逼真度: ■可合成性:同意环境下,多个协议同时执行。一个协议的消息是否会破坏其他协议的安全目标。 活跃研究团体 ■美国空军研究实验室:Meadows代表。 ■英国London学院:Schneider代表。 ■英国Oxford学院:Roscoe代表。 ■美国Carnegie Mellon学院:Milen代表。 ■ATT实验室: Stubblebine代表。 相关问题---局限性 ■对安全协议的分析或推证往往是基于环境某些假设之上的，只有当假设成立时，证明才成立。 一旦某种假设不成立，一切的证明无效。 ■一些关键性的假设，只要攻击者违反了他们，仍可成功入侵系统。 ■安全特性对不同的要求侧重点不一样，甚至矛盾。例如匿名性和可追究性是冲突的。 形式化法进一步解决的问题 ■扩展现有的形式化分析工具的能力,不仅能证明是不安全的,还能证明是安全的。 ■为现有形式化语言构造完善的数学描述,并进行严谨的理论证明,形成统一的形式语言描述,以描述可利用的必要信息,并使之能应用于一些新的应用协议的分析中。 ■将形式化方法应用于协议说明与设计阶段，从而可以极小的代价尽可能早地发现错误。 * * 安全协议及其受到攻击的实例 ■A,B,…: 表示参与协议的主体。 ■ Kij: 主体i，j共享的会话密钥。 ■ Ki：主体i的公钥，Ki-1：主体i的私钥。 ■ Ri：主体i生成的随机数，Ni：主体i生成的序列号。 ■ Ti：主体i生成的时戳。 ■[m1| m2]: 表示消息 的级联 ■ E(k:m): 表示用密钥K对消息m加密。 ■ Text1,Text2, …: 为消息常量。 ■ fKab(X): 表示用Kab加密的Hash函数。 ■ Z:表示攻击者。 无可信第三方参与的对称密钥协议 ■ISO one-pass 单方对称密钥认证协议 1) A?B: Text2, E(Kab: [Ta | Na], B, Text1) ■ISO two-pass 单方对称密钥认证协议 1) B?A: Rb, Text1 2) A?B: Text3, E(Kab:Rb, B, Text2) 无可信第三方参与的对称密钥协议 ■ISO two-pass 双方对称密钥认证协议