网络安全认证协议形式化分析PPT演示文稿

信息网络的根本----信息服务质量
信息价值的体现：
信息的新鲜程度（及时性） 信息的准确程度 信息的全面性 掌握信息的权利（信息=资本/权益/责任）
信息的价值是信息网络不安全的根源----
通过一定手段非法得到或阻止及时地、合法 地得到正确的、完整的信息
安全信息网络
具有防范非法手段获得或破坏正常信 息获取能力的信息网络。
密码系统算法、生物信息（看成一种密码）
其它 其它
权限模型与权利保护
权限模型与权限服务器（强制访问控制服务 器、XrML）
数字版权保护与安全内容分发 安全服务器（S-Web Server、S-Email
Server、主机攻击报警等）
可信的WEB SERVICE技术
安全的服务的发布、查找和调用技术 基于XML的信息加密和签名
技术成果1：因特网技侦平台
Internet
实时获取因特网数据包
协求输入/信息获取
成 果
2
网 络 信 息 预 报 警
最终用户（End Users）（包括政府领导、司法/安全/军队部门人员、网管人员、 专业信息消费者等等）
服务
预警系统
报警系统
其它专业系统
控制系统
安全攻击的基本模式说明
信息源 信信息息源源
信息源
信地息信信信目息息息的目目目地的的的地地 信息目的地
正非常目信的息地 流
被中断的信息流------对可用性的攻击 被拦中伪截间造/篡侦的改听信的信息信息流息流---流---对----真对--对实机完性密整的性性攻的的击攻攻击击
二 信息网络安全核心技术
信息网络的安全核心技术
信息网络的可用性保证技术 应用的安全 身份认证和权限管理 内容安全 密码学和加密技术

Security of Authentication Protocols Involving T rusted Third Party
Z HUO Ji-liang , LIN Hui-li, LI Xian-xian (School of Computer S cience & Engi neer ing , Beihang Uni versi ty , Beiji ng 100083 , Chi na)
在有 T T P 存 在 的 情况 下 , 这 两 个设 计 目 标主 要 是 通过 T T P 及其所生成的安全会 话密钥来实现 的 。 因此协 议通常包 含两个基本 步 骤 :①在 对等 参 与者(或 其 中之 一)的 请求 下 , T T P 完成会话密 钥的生 成和 分发 ;②两 个对 等参与 者通 过握 手过程向对方证明自己的确拥有 T TP 刚刚颁发的会话密钥 。
早已成为国际上的一个研究热点 , 而且在近年来取 得了许多重 要的进展[ 6] :提出 了许 多用 于协 议分 析的 理论 模型 和分 析方 法 , 还开发出了许多自动分析工具 。 然而文献中专门针对具 有 可信第三方的这类认证协议特殊安全需求的分析较少 , 如何设 计安全高效的这类协议是一个实际应用中亟待解决的问题 。
我们把这类协议的基本安全需求归纳为以下四点 : (1)保密性 。 除去 A , B 和可信第 三方 S 外 , 没 有其他主体 可以得到该密钥 K ab 。 (2)真实性 。 K ab 的最初的来源是可信第三方 S 。 (3)新鲜性 。 K ab 是可信第三 方 S 为本次 协议会 话所生成
的一个新密钥 。 (4)一致性 。 A , B 最终所得到的会话密钥是同一个密钥 。 这四个基本安全需求是这类协议安全的四个必要条件 , 如

内江师范学院学报J OUR NAL OF N EIJ IAN G NORMAL UN IV ERSI TY第23卷第12期No.12Vol.23一种自动验证网络安全协议的互模拟方法杨　军,孟海涛3(盐城工学院江苏　盐城224051) 摘　要:为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为“符号化”的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi 演算设计了符号互模拟关系—符号Reded 互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现.关键词:密文通信协议;进程演算;符号互模拟中图分类号:TP393.08文献标识码:A文章编号:167121785(2008)12-0056-030　引言近十年来,进程演算,如Spi 演算[1]、CSP 和CCS 等,由于能很好地为网络安全协议建立模型、验证其安全属性,因而基于进程演算的安全协议形式化分析方法得到很大的发展.在这些模型中,Abadi 和G or 2don 的Spi 演算尤为引人注目.Spi 演算是在Pi 演算[5]中增加了加解密原语和一些关系扩展而来.协议的安全属性通常用偏序关系∠∠来表示[4].例如,为了说明协议P 具有保密性,可以构造一个与P 并发的攻击者O ,在环境ε里并发执行P 和O.如果所有的运行迹均未泄漏密文消息M ,则说明P 具备保密性,否则不具备.其缺点在于进程O 并不能描述所有的攻击者.1Spi 演算语言Spi 演算为由Pi 演算发展而来的进程代数语言.在增加了对称加解密、哈希原语之后,它能够用来表示复杂消息的传递,从而可以来为安全协议建立模型.在增加了配对(pairi ng )、配对分裂(pair 2split ti ng )、匹配(match )和非匹配(mismatch )等原语后,更进一步地描述安全协议性质.对安全协议的分析基于同样的完美加密假设[2],也即加密和哈希算法是足够强壮的,加密的密钥是原子的.本文所使用的Spi 演算的语法如下:n ∷=a ,c ,….,k ,n …名N ν∷=x ,y ,z …变元VM ∷=n │(M 1;M 2)│E (M;n )│H (M )　消息Mt ∷=x │M │(t 1,t 2)│E (t 1,t 2)│H (t)│πi (t 1,t 2)│D (t 1,t 2)项Tb ∷=tt │b 1　∧b 2│┐b │[t 1=t 2]│[t :N ]│[eν├t]布尔表达式BP ∷=0│c(x).P │c 〈t 〉.p │P │Q │b ∶P ,Q │(νa)P │let x =D (t ,t ′0)in P │case x of πi (t 1,t 2)in P进程项P为了表示非对称加密,假设有关系КΑN ×N ,满足(k ,k ′)ΑК当且仅当用k 加密的消息能被k ′解密;定义I (k )={k ′│(k ,k ′)ΑK};一个替换σ是一个满足条件σ(.)∶V →T 的偏序函数.替换可以作用于进程、项和表达式等.2　符号操作语义与具体语义规则不同的是,当执行符号语义中的进程输入动作时,用给输入变元赋值的消息是用含变元的项来替代的,而这种替代直到环境允许时才进行.此外,语义规则中布尔表达式满足的条件在进程迁移过程中被累积和满足[3].符号操作语义的迁移规则形式是P |→λbP ′,这里,λ∈A s ={c(x),c 〈t 〉},b ∈B ,则记为P |→λttP ′.当b =�,相应的对称规则省略.当布尔表达式条件为真时,符号操作语义传递规则跟具体语义是等价的.S pi 演算的符号操作语义如下:65　收稿日期　作者简介杨军(6),男,江苏盐城人,盐城工学院学生处硕士:2008-09-01:199-.2008年12月杨　军,孟海涛:一种自动验证网络安全协议的互模拟方法(S IN )--c (x )P |→c (y )ttP [y/x ]y =new {T},(S OU T )--c 〈t 〉P |→c 〈t 〉ttP,(S CH S I )P |→λbP ′b ′∶P ,Q |→λb ∧bP ′,(S PARI )P |→λbP ′P |Q |→λbP ′|Q,(S RES )P |→λbP ′(νa )P |→λb(νa )P ′a |{c}∪n (b),(S S PL 1)P[t 1/x 1]|→λbP ′ca se x of π1(t 1,t 2)in P |→λbP ′(S D EC )P[t/x ]|→λbP ′let x =D (E (t ,t ′),t ″)in P |→λb ∧b ′∧b ″P ′b ′ =(I (t ″)=t ′),b ″={t ′,t ″}∶N .引理2.1　PμP ′当且仅当存在赋值ρ和替换σ,且满足P |→λb P ′,这里,P ′=Q σ,μ=λ.σ,ρ(b.σ)=tt.3　格局的LTS 语义在Spi 演算中,密文协议被认为运行在能够攫取、伪造各种消息的环境中.进程P 的具体环境ce ν是由进程P 具体消息的输出和复合规则得到的消息集合,而符号环境eν是进程P 项输出和复合规则的集合.本节主要分析进程的符号环境(为方便起见,后文用“环境”指称“符号环境”).当一个进程输出一个消息时,它的环境将复制一份放入其消息集中.另一方面,当进程需要输入一个消息时,它的环境将试图伪造各种可能的消息给输入进程,这就导致了如引言中所述的难以处理的输入动作迁移后出现的无穷种可能分支问题.从环境e ν产生项t 的过程必须仔细地设计,首先看如下一个例子.P ≡c 〈E (M ,k )〉|c (x ).l et =Dec (x ,I (k ))inc 〈u 〉,eν=Φ.在上述进程的执行中,P 需要从环境中接收一个项=(y ,)由于密钥对环境依然是未知的,项=(y ,)的产生只能受限于替换σ(=[M y ]),且当环境知道消息(M ,)也即,假设(M ,)∈e ν;k |ev ,替换σ(=[M/y ])使得推理e ν|-t 成立,这里t =E (y ,k ).格局C =(eν,P )是进程P 和其符号环境ev 的二元组.格局的迁移对应于进程和其环境之间的交互.现在,定义格局的标号迁移语义(L TS 语义)(F IN )P |→c (x )b P ′[t/x ](e ν,P)|→c (x )b ∧[e ν|-t](e νσ,p ′[t/x ]σσ∶e ν|-t ,(F OUT )P |→c (x)bP ′(e ν,P)|→c(x)b(e ν∪{t},p ′),4　Reefe d 互模拟在Spi 演算中,互模拟等价是两个进程之间十分重要的关系.为了验证进程P 和Q 之间是否互模拟,通常需要在等价环境对中检验P 和Q 是否执行一致的动作.本文中所使用的互模拟关系(取名为Reef ed 互模拟),包含具体和符号互模拟.具体Reef ed 互模拟的定义类似于其他已存在的互模拟[2].定义4.1　一个协调的关系R c 是具体Reefe d 模拟的,当(e ν1,e ν2)|-PR cQ 可推出,无论(ce ν1,P )c(x)(ce ν′1,P ′),存在一个格局(ce ν′2,Q ′)和(ce ν2,Q)c(y)(ce ν′2,Q ′),且对所有的消息M 和N ,(ce ν1,ce ν2)|-(M ∴N ),满足(ce ν′,ce ν′2)|-P ′[M/x ]R cQ ′[N/y ];(ce ν,P )c〈M 1〉(ce ν′1,P ′),这里ce ν′1=ce ν1∪{M 1},存在一个格局(ce ν′2,Q ),且满足(ce ν2,Q )c〈M 2〉(ce ν′2,Q ′)ce ν2=ce ν′2∪{M 2}和(ce ν1,ce ν2)|-P′R C Q ′.一个具体的Reefed 互模拟是关系R c ,且满足R c和R cT都是具体Reefed 模拟的.具体的Reefed 互模拟类(Bi similarit y)(～c r )是所有具体Reefed 互模拟关系的集合.具体Reefed 互模拟即指具体Reef ed互模拟类,用符号～c r 来表示.定义4.2　一个协调的关系R b 是符号Reef ed模拟的,当(ν,ν)|R Q 可推导出,无论何时()　(ν,)|→(x )∧[ν|](ν′,′[x ]σ),这里75t E k .k t E k /ev E k .E k e 1e 2-P b i e 1P c b1e 1-t e P t/1内江师范学院学报第23卷第12期σ1∶eν1|-t且eν′1=eν1σ1,存在一个替换σ2和布尔集B,满足(1)σ2∶eν2|-t和eν′2=eν2σ2;(2)b∧b1]∪B,Πb′∈B,b′]b2满足(eν2,Q)|→c(x)b2∧[eν2|-t](eν′2,Q′[t/y]σ2)和(eν′1,eν′2|-P′[t/x]σ1R b Q′[t/y]σ2.(ii)　(eν1,P)|→c〈t1〉b1(eν′1,P′),这里eν′1=eν1∪t1,存在一个布尔集B,这里b∧b1]∪B,Πb′∈B,b′]b2,满足(eν2,Q)|→c〈t2〉b2(eν′2,Q′),这里eν′2=eν2∪t2,且(eν′1,eν′2)|-P′R b′Q′.定理4.1(可靠性)　如果ε|-P～b r Q,ε= (eν1,eν2),则存在一对合适的替换σ1,σ2和一个赋值函数ρ,满足εcσ1,σ2|-Pσ1～c r Qσ2.5　总结本文首先把Spi演算扩展为能描述所有加密系统的、具有清晰语义的计算模型.为解决进程接收具体信息的输入所带来的无穷种迁移问题,提出了进程符号环境和符号化的格局标号迁移语义.在此基础上,为S pi演算设计了解决此问题的符号互模拟关系———符号Reef ed互模拟,并证明了它是具体互模拟关系的可靠逼近.基于这项工作,显然可以实现基于Spi演算的协议安全属性自动化验证,我们相信这对于应用在软件和电路中的自动检测也有很大的启发作用.参考文献:[1]Abadi M and G or d o n A D.A bisimulation met h od fo rc rypto graphic protocols[J].No rdic Jo ur nal of Compu2ting,1998,5(4):2672303.[2]Boreale M,De Nicola R,and Pugliese R.Proof tech2nique s for cryptographic processes[J].SIAM Journal on Computing,2002,31(3):9472986.[3]Borgst r J om,Briais S a nd Nestmann U Symb olic bisimu2lations in the spi calcul us.Proc.of CONCU R2004,vol2 ume3170of LNCS,2004:1612170.[4]Boreale M Symbolic trace a nalysis of c ryptograp hic p ro2tocols[M].Proc of ICAL P200,2001:6672681.[5]ner,Pa rrow J,Walker D.A calc ulus of mobileproce sses,I a nd II[J].Infor mation a nd Computation, 1992,100(1):1277.A Bisimulation Method for Automatic Conf ir m a tionof N et w or k Secur ity Cr yptogra phic Pr otocolsY ANG jun,ME NG Hai2Tao(Y a ncheng Institute of Tecnology,Y anc heng,Jiangsu224051,China) Abstract:In order to find a solution to the infinite migra tio n p ro ble m caused by a process’s receipt of concrete infor mation input,by use of a sym b olic method,the idea of proce ss symbolic environment and symbolic migration se ma ntic s ar e put for th. The r elation of symbolic bisimulation(symbolic Reef ed bisimulation)is designed f or Spi calculus.The re sult shows:the symbol2 ic bisim ulation is reliable to the tr aditional concrete bisimulation.Since t he symbolic migration semantics i s a ble to confine the migr ation restric tio n,whic h arises f ro m the proce ss’s receipt of infinite input,to finite migration,it help s secure the realiza tio n of t he automatic securit y p ro tocol confirmation that is ba sed on such a relation. K ey w or ds:cr yptographic p rotocols;process calc ulus;symbolic bisimula tionn(责任编辑:胡　蓉　英文审译:阳卓胜) 85。

化测试分析 B2：结构化保护 E4：半形式化分析
GB5：访问验证保护级
B3：安全区域
E5：形式化分析
EAL6：半形式化验证设 计测试
--
A：验证设计
E6：形式化验证
EAL7：形式化验证和测
试
知识链接信息保障PDRR模型
Protect
Detect
Restore
React
网络安全与黑客攻防技术
华东交通大学理工学院 尧刚华
课程简介
计算机网络安全基础：包括信息安全、网络安
全、病毒、黑客以及基本网络技术等。
基本的黑客攻击技术：包括基本命令、扫描、
监听、入侵、后门、隐身、恶意代码等。
基本的防御技术：包括系统安全、加密、防火
墙、隔离闸、入侵检测、IP安全、Web安全等。 目的是使同学们可以进一步了解网络基本知 识，掌握初步的黑客攻击技术，提高网络安全意 识。
邮政系统的分层结构
发信者 书写信件 贴邮票 送邮箱 收集信件 盖邮戳 信件分拣 邮局服务业务 邮局服务业务 通信者活动 通信者活动 阅读信件 收信者
信件投递 信件分拣
信件打包 送运输部门
邮局转送业务
邮局转送业务
分发邮件 邮件拆包
路由选择 运输
转送邮局
运输部门的运输路线 接收邮包
分层的优点
各层功能明确，且相互独立易于实现。 各层之间通过接口提供服务，各层实
是网络安全橙皮书。
自从1985年橙皮书成为美国国防部的标准以来，
就一直没有改变过，多年以来一直是评估多用 户主机和小型操作系统的主要方法。
类别 级别
名称
主要特征
D
C
D
C1 C2
低级保护

计算机网络管理与安全技术
第5章 网络安全基础
1.
2.
3. 4. 5. 6. 7. 8.Biblioteka 9.10. 11.
为什么要学习网络安全 网络安全涉及的领域 安全问题的实质 安全问题现状 网络安全的概念 网络系统面临的威胁 计算机网络系统的脆弱性 网络安全技术的研究内容和发展过程 计算机网络安全的三个层次 网络安全的设计和基本原则 安全技术评价标准
3 威胁的具体表现形式
1）伪装 2）非法连接 3）非授权访问 4）拒绝服务 5）抵赖 6）信息泄露
威胁的具体表现形式
7）业务流分析 8）改动信息流 9）篡改或破坏数据 10）推断或演绎信息 11）非法篡改程序
网络攻击基本原理
漏洞
系统漏洞 人为因素 后门
系统后门 特洛伊木马 系统服务 不完善 社会工程
网络攻击手段
被动攻击 这类攻击一般在信息系统的外部进行，对信息网络 本身一般不造成损坏，系统仍可正常运行，但有用 的信息可能被盗窃并被用于非法目的。 主动攻击 这类攻击直接进入信息系统内部，往往会影响系统 的运行、造成巨大的损失，并给信息网络带来灾难 性的后果。
被动攻击
被动攻击一般是主动攻击的准备和前奏 信息窃取 密码破译 信息流量分析
I have set Back door, bye!
I just have a dream, what happened?
T
Internet
X
7 计算机网络系统的脆弱性


1 2 3 4 5
操作系统安全的脆弱性 网络安全的脆弱性 数据库管理系统安全的脆弱性 防火墙的局限性 其他方面的原因
第5章：网络安全基础
1 为什么要学习网络安全： 信息共享与信息安全总是互相矛盾的。 计算机犯罪的日益增多对网络的安全运行和进一 步发展提出了挑战。 要保证网络的安全以及保证网络上数据的完整性 Internet的发展使人们不再把信息安全局限于局 部范围，而是扩展到网络互连的世界范围。 安全技术得到新的发展，内容极为丰富。

隐私保护的需求： 在保护用户隐私的 同时，需要确保安 全算法的正确性和 安全性。
法律法规的限制： 在某些情况下，安 全算法可能受到法 律法规的限制，需 要遵守相关规定。
未来研究方向
新型加密算法：探索更高效、更安全的加密算法，以应对不断变化的网络威胁。
隐私保护：研究如何在保护用户隐私的同时，实现数据的共享和利用。
易用性
算法的复杂度：评估算法的易用性， 通常需要考虑算法的复杂度，包括 时间复杂度和空间复杂度。
算法的稳定性：在安全算法中，稳 定性也是一个重要的评估指标，指 的是算法在面对攻击时的鲁棒性。
添加标题
添加标题
添加标题
添加标题
算法的可读性：易用性还与算法的 可读性有关，易于理解和实现的算 法更易于使用。
加密算法的效率： 评估算法在执行过 程中的效率，包括 加密和解密的速度
加密算法的可靠性： 评估算法在执行过 程中的可靠性，包 括算法的错误率、 漏洞等因素
加密算法的适用性： 评估算法在特定场 景下的适用性，包 括算法的适用范围、 适用场景等因素
效率
算法复杂度：评估算法执行时间的长短 加密速度：评估加密算法的加密速度 解密速度：评估解密算法的解密速度 安全性证明：评估算法的安全性是否经过严格证明
安全算法及安全性分 析
,a click to unlimited possibilities
汇报人：
目录 /目录
01
点击此处添加 目录标题
04
安全性分析方 法
02
安全算法概述
05
安全算法的评 估指标
03
常见安全算法 介绍
06
安全算法的发 展趋势和挑战
01 添加章节标题
02 安全算法概述

（2）验证IP地址的真实性。
使用各种方法获取的IP地址的真实性必须经过认真验证，真实的IP地址才具有追查价值。造成IP地址不准确的原因有很多， 如从安全角度考虑隐藏IP地址造成的虚假、网络应用环境造成的IP虚假、人为伪造造成的IP虚假，不同情况应区别对待。
第7章 信息安全基础
说一说 制定防范攻击应急预案的重 要性。
1．发现入侵事件
发现入侵是响应入侵的前提，发现得越早，响应得越及时，损失就越小。非法入侵的特性决定了入侵的隐秘性，所以发 现入侵较为困难。一般情况下，可以考虑从以下几个方面入手，争取尽早发现入侵的迹象。
（1）安装入侵检测设备。 （2）对Web站点的出入情况进行监视控制。 （3）经常查看系统进程和日志。 （4）使用专用工具检查文件修改情况。
第7章 信息安全基础
360安全卫士提供4种木马查杀方式。 快速查杀：此方式仅扫描系统内存、启动对象等关键位置，由于扫描范围小，所以速度较快。 按位置查杀：由用户自己指定需要扫描的范围，此方式特别适用于扫描U盘等移动存储设备。 全盘查杀：此方式扫描系统内存、启动对象及全部磁盘，由于扫描范围广，速度较慢。由于木马可能会存在于系统的任 何位置，用户在第一次使用360安全卫士或者已经确定系统中了木马的情况下，需要采取此种方式。 强力查杀：正常模式下难以查杀的顽固病毒及木马，可使用强力查杀模式。 （4）扫描完成，显示使用360查杀木马的结果，如图所示。如发现在计算机中存在木马，单击“一键处理”按钮，删除 硬盘中的木马。
（2）根据《中华人民共和国刑法》第二百八十五、第二百八十六条的规定，对违反国家规定，侵入国家事务、国防 建设、尖端科学技术领域计算机信息系统的，要受到刑罚；即使侵入的是一般信息系统，如果造成严重后果，同样也要 受到刑罚，显然，黑客行为达到一定程度就是犯罪。

０ 安令协议的认证性。 仿真分析 的结果表 明，ｐ 演算能够为安全协议的分析和验证提供可靠和有效 的支持 。 Ｓｉ 关键词 ： 演算 ； 安全协议 ； 认证性 ； 仿真
中图分类号 ：Ｐ ０ ； Ｐ ０ Ｔ ３ １Ｔ ３ ９ 文献标识码 ： Ａ
Ｓ ｍｕ ａ ｉ ｎ Ａｎ ｌ ｓｓｏ Ｓ ． ｅ ｕ ｉｙ Ｐｒ ｔ ｃ ｌＢａ ｅ ｎ Ｓ ｉＣａ ｃ ｌ ｓ ｉ ｌ ｔｏ ａ ｙ ｉ ｆＳ Ｌ３ ０ Ｓ ｃ ｒ ｔ ｏ ｏ ｏ ｓ ｄ ｏ ｐ ｌ ｕ ｕ
研 究领域 。 文章介绍 了Ｓ Ｉ． Ｓ ０安全协议 的握手过程和 Ｓｉ ３ ｐ演算的基本概念 ， 包括基于 Ｓ ｉ ｐ 演算认证性的验证方法 。 存此基础 上， 基于Ｓ ｉ ｐ演算形式化地建立 了ＳＩ． 安全协议 的仿真模 型， Ｓ ０ ３ 给出了分析 ＳＩ． 安全协议的详细过程 ， Ｓ ０ ３ 最终验证 ＿ＳＬ ． ｒ Ｓ３
ＡＢＳ ＴＲＡＣＴ ： ｅ ｅ ｒ ｒ ａ ｄ ｖ ｌ ｅ ａ ｉ ｔ ｆ ｓ ｃ ｒｔ ｒ ｔ ｃ ｌ ｈ ｒ ｌ ａ ｅ ｃ ｍｐ ｅ ｅ ｙ ｆ ｕ ｄ ｍａ ｕ ｌ ． Ｔ ｅ Ｔｈ ｒｏ ｎ ｕ ｎ ｒ ｂ ｌ ｙ ｏ ｅ ｕ ｙ ｐ ｏｏ ｏ ａ ｄ ｙ ｃ ｎ ｂ ｏ ｌ ｔ ｌ ｏ ｎ ｎ ａ ｌ ｉ ｉ ｙ ｈ ａ ａ ｙ ｉ ａ ｅ ｎ ｆ ｒ ｌ ｍｅ ｈ ｄ ａ ｕ ｒ ｎ ｅ ｈ ｉ ｈ ｎ ｓ ｎ ｏ ｌ ｔ ｎ ｓ ｆ ｓ ｃ ｒｔ ｒ ｔ ｃ １ Ｎｏ ｈ ｎ ｌ ｓｓ ｂ ｓ ｄ ｏ ｏ ｍａ ｔ ｏ ｓ ｃ ｎ ｇ ａ ａ ｔ ｅ ｔ ｅ ｒｇ ｔ ｅ ｓ ａ ｄ ｃ ｍｐ ｅ ｅ ｅ ｓ ｏ ｅ ｕ ｉ ｐ ｏ ｏ ｏ ． ｙ ｗ ｔｅ ｆ ｒ ｌ ｅ ｎ ｌ ｓｓ ａ ｄ ｖ ｒ ｉ ａｉ ｎ ｏ ｅ ｕ ｉ ｒ ｔｃ ｌ ａ ｅ ｏ ｅ ｅ ｒ ｈｆ ｃ ｓｏ ｅ ｗ ｒ ｅ ｕ ｉ ，ｉ ｉｈ ｏ ｍａｉ ｄ ａ ａ ｙ ｉ ｎ ｅ ｉ ｃ ｔ ｆ ｃ ｒｔ ｐ ｏｏ ｏ ｓｂ ｃ ｍｅａ ｒ ｓ ａ ｃ ｕ ｆｎ ｔ ｏ ｋ ｓ ｃ ｒｔ ｎ ｗｈ ｃ ｚ ｆ ｏ ｓ ｙ ｈ ｏ ｙ ｔ ｅ ｍｏ ｅ ｅ ｉ ｃ ｔ ｎ ｍｅ ｈ ｄ ｂ ｓ ｄ ｏ ｐ ａｃ ｌ ｓｉ ｎ ｉ ｏ ｔ ｎ ｅ ｅ ｒ ｈ ｄ ｍａ ｎ ｎ ｔ ｅ ｐ ｐ ｒ ｈ ｄ ｌｖ ｒｆ ａｉ ｔ ｏ ａ ｅ ｎ Ｓ ｉ ｌ ｕ ｕ ｓａ ｍｐ ｒａ ｔ ｓ ａ ｃ ｏ ｉ ．Ｉ ｈ ａ ｅ ，ｗｅｉ ｔ ｄ ｃ ｉ ｏ ｃ ｒ ｎ ｒ ｕ ｅ ｏ

第28卷　第3期2005年3月计 算 机 学 报CH IN ESE J OU RNAL OF COM PU TERSVol.28No.3Mar.2005SPA :新的高效安全协议分析系统李建欣　李先贤　卓继亮　怀进鹏(北京航空航天大学计算机学院　北京　100083)收稿日期:2003201209;修改稿收到日期:2004212230.本课题得到国家自然科学基金(90412011)和国家“八六三”高技术研究发展计划项目基金(2003AA144150)资助.李建欣,男,1979年生,博士研究生,主要研究方向为网络安全、信任协商.E 2mail :lijx @ ;myjianxin @.李先贤,男,1969年生,博士,副教授,主要研究方向为信息安全、计算机科学理论.卓继亮,男,1976年生,硕士研究生,主要研究方向为网络安全.怀进鹏,男,1962年生,博士,教授,博士生导师,主要研究方向为计算机软件与理论、中间件与网格技术、网络安全.摘　要　研制高效的自动分析系统是密码协议安全性分析的一项关键任务,然而由于密码协议的分析非常复杂,存在大量未解决的问题,使得很多现有分析系统在可靠性和效率方面仍存在许多局限性.该文基于一种新提出的密码协议代数模型和安全性分析技术,设计并实现了一个高效的安全协议安全性自动分析系统(Security ProtocolAnalyzer ,SPA ).首先对协议安全目标进行规范,然后从初始状态出发,采用有效的搜索算法进行分析证明,试图发现针对协议的安全漏洞.使用该系统分析了10多个密码协议的安全性,发现了一个未见公开的密码协议攻击实例.实验数据显示,该系统与现有分析工具相比,具有较高的分析可靠性和效率,可作为网络系统安全性评测以及密码协议设计的有效辅助工具.关键词　信息安全;密码协议;形式化分析;搜索算法;攻击序列中图法分类号TP309SPA :A N e w E ff icient System for Security Protocol AnalysisL I Jian 2Xin L I Xian 2Xian ZHUO Ji 2Liang HUA I Jin 2Peng(S chool of Com puter Science ,Bei hang Universit y ,Bei j i ng 100083)Abstract Cryptograp hic protocols are communication p rotocols of dist ributed systems t hat use cryptograp hy to achieve various goals such as aut hentication and key dist ribution in t he open net 2work environment.Developing efficient automatic system is a crucial task in t he area of security analysis for cryptograp hic p rotocols.However ,t he security analysis for cryptograp hic protocols is very co mplex and difficult and a lot of unresolved p roblems still p resent in it ,which causes some limitations on reliability and efficiency of previously available automatic systems.An effi 2cient automatic analysis system (Security Protocol Analyzer ,SPA )for cryptograp hic p rotocols is designed and implemented based on t he CPA (Cryptograp hic Protocol Algebra )model and new a 2nalysis techniques.In t his system ,security p roperties of t he cryptograp hic protocols are specified firstly ,and t hen an effective p roof search algorit hm starting wit h t he initial state is applied and t ries to find all possible attack sequences on t hem.More t han ten cryptograp hic protocols are ana 2lyzed successf ully wit h t his system ,and moreover ,a new attack instance is also found.The anal 2ysis result s show t hat SPA has imp roved t he analysis reliability and efficiency compared wit h ot h 2er existing tools.It can be used as an efficient tool for t he evaluation of t he network security and t he design of cryptograp hic p rotocols.K eyw ords information security ;cryptograp hic protocol ;formal analysis ;search algorit hm ;at 2tack sequence1　引　言随着互联网技术及应用的飞速发展,如何保护网络传送信息的安全成为一项重要的任务.密码协议(也称为安全协议)是采用密码学技术来达到密钥分配、主体身份认证等目的的通信协议,在很大程度上为网络通信提供了安全性保证.这些密码协议都是经过精心设计的,角色间消息的交互存在着复杂的关系和制约,而且大部分的密码协议是运行在分布式网络环境中.分布式网络具有多主体参与、大规模并发和运行动态性等特点,正是由于这种运行环境的复杂性使得设计出的密码协议难免出现缺陷.大量的事例表明,许多密码协议在使用多年后才发现存在很严重的安全漏洞,例如著名的Needham2 Schroeder公开密钥协议在公开17年后,它存在的中间人攻击漏洞才被Lowe发现[1].由于密码协议的漏洞一般都很隐蔽,使用手工分析非常困难,易于出错,所以研制高效、可靠的自动分析工具成为密码协议安全性分析的一项关键任务.目前国际上推出了许多自动分析工具,然而它们大都仍然存在搜索状态数太多的问题,而且这些工具往往只面向研究人员,一般的技术人员难以使用.本文在文献[2]提出的密码协议形式模型———CPA (Cryptograp hic Protocol Algebra)模型的基础上,设计并实现了一个高效的安全协议分析系统SPA (Security Protocol Analyzer),能够有效分析多种类型的密码协议.2　相关工作采用形式化方法分析密码协议已有20多年的历史,一直属于国际上研究的热点[3].目前,对密码协议进行形式化分析广泛采用模型检测和定理证明的技术.针对密码协议进行形式化分析的特定模型检测工具包括Interrogator[4]、Brut us[5]等.其中Interro2 gator是比较早的基于状态空间搜索思想来发现协议安全缺陷的模型检测工具,它使用通信状态机描述协议的参与者,并赋予了攻击者对信息自动处理的能力;Brut us是采用一阶逻辑描述密码协议的属性,从协议运行的初始状态开始搜索所有合法主体和攻击模型的活动序列来检测是否存在协议的攻击序列,并使用偏序和对称的消减方式来限制状态搜索空间.通用模型检测工具包括FDR[1]、Murφ[6]等,其中FDR是基于进程代数理论CSP的自动模型检测工具,牛津大学的Lowe首先将其用于密码协议安全性的分析,方法是将协议参与主体视为CSP进程,攻击者的进程则描述多种攻击行为,协议的安全性目标被描述为主体的事件序列;Murφ是由斯坦福大学的Mitchell应用于密码协议的分析,它在许多方面的描述类似于FDR,但它是使用共享变量来描述协议主体事件,使用不变量描述协议的安全属性,同时采用对称消减、可逆规则等技术来提高系统效率.模型检测工具更有利于通过自动推理生成攻击实例的方法来检测协议的不正确性,但在证明协议正确性时,往往很难做到将无限状态空间映射为一个有限状态空间,从而容易出现无限搜索状态空间的问题.相对于模型检测,定理证明的技术可以处理无限状态空间,因而可以提供协议的正确性证明.采用定理证明技术的NRL协议分析器[7]是比较著名的密码协议分析工具,能够分析任意数量参与主体密码协议的安全性,它是以不安全的状态为开始进行回溯搜索,如果不安全状态不能够从初始状态达到,协议就是安全的,否则就是不安全的,同时搜索的过程就是一个攻击的过程.NRL分析器的缺点是自动化程度较低,往往需要人工干预,相对效率也比较低.At hena[8,9]是Dawn Song和Sergey Berezin等结合模型检测和定理证明的方法新开发的密码协议分析工具,它使用扩展的SSM模型[8,9]描述协议的运行,采用更为紧致的状态表示方法、变量替换和消减规则来减小状态的搜索空间.At hena的证明过程类似N RL分析器,都是以不安全状态为开始进行状态搜索的,但是它对攻击者的能力做了约束,且变量替换没有类型匹配的限制,在处理复杂密码协议时,容易产生搜索状态空间爆炸问题.3　密码协议的代数模型本文采用文献[2]提出的密码协议代数(CPA)模型规范密码协议,并运用了相应的安全性分析理论.为便于理解,这里对CPA模型只作简单介绍,关于本节内容的详细论述可参见文献[2],本文未特别说明的符号和术语均与文献[2]一致.3.1　密码协议代数原子消息.　PR I M=I D∪K E Y∪GEN.其中I D表示协议中主体的名称集合;K E Y表示密钥集,013计 算 机 学 报2005年包括非对称密钥中的公私钥和对称密钥;GEN =∪a ∈ID G a ,G a 对应协议中由标识名为a 的主体生成的所有消息集.消息项可如下递归定义:(i )若t 是原子消息,则t 是消息项;(ii )若t 1,t 2是消息项,则t 1・t 2是消息项;(iii )若t 是消息项,k ∈K E Y ,则{t}k ,M A C (t ,k )和H ash (t )是消息项.其中运算符・称为联接运算;{m}k 称为加密运算,满足:{{m}k }k -1=m 和{{m}k -1}k =m , 若k =k -1则称为对称密码运算;若k ≠k -1则称为公钥密码运算;H as h (m )称为哈希函数运算,M A C (m ,k )称为消息认证码函数,满足Has h (m 1)=Has h (m 2)Ζm 1=m 2和M A C (m 1,k 1)=M A C (m 2,k 2)Ζm 1=m 2∧k 1=k 2.消息项集M 与消息运算构成一个代数系统,称为密码协议代数CPA .迁移函数.　设A 是一个CPA 代数,σ是M n ∪{Δ}到M ∪{Δ}的一个映射,若对任何b =(b 1,b 2,…,b n )∈M n ,满足σ(b )∈A [b 1,b 2,…,b n ],则称σ为A 上的一个迁移函数.这里引入一个特殊符号“Δ”,表示空的消息项.变量替换.　一个变量替换<(t )=t{t 1/x 1,t 2/x 2,…,t n /x n }表示使用项t i 替换变量x i 在t 中的所有出现项.若变量替换满足<(t )=<(t ′),则称<是项t 和t ′的合一.3.2　密码协议的形式描述以下叙述中,均假设P 是一个N 方密码协议.基本事件.基本事件可表示为三元组〈σi j (α,l ),t ,t ′〉,其中σi j (α,l )为事件函数,l 为协议的会话轮数,α=(a 1,a 2,…,a N )为参与协议会话主体集,下标i 用于标识该事件主体在α中的位置,下标j 用于标识该事件所在事件序列的序号.t 和t ′分别表示接收到和发送出的消息项,满足映射关系t ′=σi j (α,l )(t ).事件函数偏序关系ΜP ,满足σi 1j 1(α1,l 1)ΜPσi 2j 2(α2,l 2)当且仅当i 1=i 2∧α1=α2∧(l 1<l 2∨(l 1=l 2∧j 1Φj 2)).设协议P 的有限序列Γ=τ1τ2…τn ,其中τi 表示事件函数,若满足:(1)对于任何1Φi <j Φn,不存在τi ,τj 使得τj ΜP τi ;(2)当σi j (α,l )∈Γ,对于1Φk Φj ,σik (α,l )∈Γ;则称Γ是协议P 的长度为n 的一条迹.当x =(x 1,x 2,…,x n )∈M n,则称序列Γ(x )为协议P 的迹序列.密码协议的形式定义.　一个N (Ε2)方密码协议是二元组,其中,(1)M 是基本消息代数空间;(2)P =〈P 1,P 2,…,P N 〉,其中P i 是N 方协议P 的第i 个角色,对Πα=(a 1,a 2,…,a N )∈I D (N ),l ∈N ,可以导出相应事件函数序列:Σi (α,l )=σi ,1(α,l )…σi ,s i (α,l ),其中σi ,j (α,l )为协议的原子事件函数.在这里,迹Σi (α,l )称为角色P i 的正则迹.当x =(x 1,x 2,…,x n )∈M n,则称迹序列Σi (α,l )(x )为角色P i 的正则迹序列.正合序列.　设Γ=σ1σ2…σn 是迁移函数序列,对于a i ∈M ∪{Δ},可得到消息迁移序列Γ(a )=〈σ1,a 1,σ1(a 1)〉〈σ2,a 2,σ2(a 2)〉…〈σn ,a n ,σn (a n )〉,D 0是攻击者初始知识,若满足a 1∈D 0,a i ∈D i -1,D i =D i -1[σi (a i )],i =1,2,…,n ,则称Γ(a )是一个正合的D 0序列.正合序列描述了攻击者的一个攻击过程.3.3　密码协议形式分析模型3.3.1　语法1133期李建欣等:SPA :新的高效安全协议分析系统Φ(X )∈Ex t (Φ(Σ)),即X 是正合的Σ2序列.(iv )M P 4a ∈ΣX 当且仅当Φ(Σ)∈R P 且Φ(a )∈Φ(Σ)Φ(X )(a ∈ΣX 为(a ,Σ)∈X 的简记,表示a ∈D 0[X ],其中D 0是关于正则迹Σ的攻击者初始知识).对含逻辑联接词?,∧和量词Π的公式语义解释是自然的.3.3.3　密码协议安全性描述秘密性安全目标.　协议的秘密安全性是建立共享秘密协议的安全要求,目的是保护某些数据(即会话目标消息)不被攻击者获取,表示为公式其中Σ是正则迹序列,t 是秘密消息项.对应性安全目标.　认证性是鉴别传输数据来源的真实性或新鲜性.CPA 模型将数据的源认证解释为一种对应性,即当认证方的正则迹序列属于一个正合迹序列,协议预先规定的角色正则迹序列(或部分)也属于这个正合序列.表示为公式ΠX.(EX T (Σ,X )∧ΣΑX )]ΛΑX(简略形式为ΣCorresp Λ),其中Λ是某个正则迹Σj (α,l )的部分或全部(简称子迹).密码协议的安全性定义.　设M P 是协议P 的一个模型,G P 是安全目标集,若G P 中的每个公式在模型M P 中都为真,则称P 是一个安全的密码协议.4　新的安全协议分析系统(SPA )基于文献[2]中的密码协议代数(CPA )模型,我们设计并实现了一个高效的密码协议自动分析系统(Security Protocol Analyzer ,SPA ),并应用该系统成功分析了一些密码协议的安全性.本节首先简要介绍系统的总体结构,然后介绍系统中的核心算法与技术.4.1　SPA 系统的总体结构SPA 系统的整体结构框架如图1所示,下面简要介绍各个模块的主要功能.(1)协议输入及其解析模块目前的公开密码协议大多使用半自然语言描述,这种描述不太严谨,容易产生二义性.由于SPA 系统仅能处理规范好的密码协议,我们采用EBN F (Extended Backus 2Naur Form )定义了一种与CPA 模型描述语言配套的协议规范描述语言,能够准确图1　SPA 系统结构框架描述密码协议组成要素.该模块提供了协议规范文本编辑器和协议辅助生成向导两种方式生成协议规范描述文本,以满足不同用户的需求.通过对生成的协议规范描述文本进行词法和语法解析,如果符合协议描述规范语法,则执行相应的语义动作,生成描述协议的静态数据.(2)分析过程控制及其管理模块这部分的主要功能是控制整个协议的分析过程,根据用户指令启动或停止分析进程.在实际运行过程中,还需要对数据的动态交换、存储进行管理,协调各个具体功能模块,保证以最优效率完成协议的分析.(3)协议数据预处理及其初始化模块该模块主要负责协议的预处理和初始化.首先,由于在协议会话过程中引入攻击者角色,所以需要构造扮演攻击者角色主体参与的会话组,生成各会话主体新的迹序列.同时,由于密码协议大多运行在开放的网络环境中,网络数据都是公开的,所以需要确定攻击者的初始知识集合,并根据其运算能力作相应的约简操作.最后,完成协议分析的初始化工作,包括为各个角色的安全目标定理证明分配独立的运行空间,建立对应的初始状态和证明树根节点,加载可能存在的用户预设策略(用户可对分析过程的证明树的深度、宽度以及状态迹序列长度等条件进行约束).(4)角色安全目标定理证明模块在CPA 模型中,密码协议P 的安全性被规范为安全目标定理集G P ,这里关键的问题就是通过一种有效的算法来证明G P 中的每条定理.本模块主要应用状态搜索算法S earchA l g 在有限的状态空间中对角色的安全目标定理进行严格的推理证明.在状态搜索过程中,需要判定各状态的安全性,其中攻击者不可达状态、攻击者可达但不违背安全目标状态都属于安全状态,攻击者可达而且违背安全目标状态属于不安全状态,对不能判定其安全性的状态,应用分裂算法S plit 扩张迹序列并生213计 算 机 学 报2005年成新的状态集(需要保证新状态的有效性和新鲜性).(5)协议分析结果输出模块为了便于分析人员了解协议分析的过程及结果,该模块既可显示协议分析结果的信息摘要(如搜索时间、搜索状态数目、攻击序列数目等),也可以通过Tree 结构图直观显示每个角色的证明状态树.这样,对于存在安全漏洞的协议,协议分析人员就能够直观、方便地了解它的攻击过程.SPA 系统的各模块间是一种松藕合关系,其总体结构框架具有良好的可扩展性,能够方便插入针对特殊协议的附加处理模块.4.2　SPA 系统的核心算法与技术我们使用Java 语言实现了SPA 系统,下面分别介绍系统三个组成部分中的一些关键算法及技术.4.2.1　输入部分在SPA 系统的输入部分,使用递归下降子程序解析协议规范描述文本,如果解析通过,将分离出它的三个主体描述类(如图2所示),其中特定迹序列是附带参数的迹序列,用于辅助表示安全目标定理中的正则迹序列Σ或其子迹Λ.对于角色P i 的迹序列Σi (α,l )中的消息项,按照其递归定义形式表示为消息树结构,其中叶节点为原子消息项.根据这些原子消息项来源和属性(在协议规范描述文本中,各角色中的原子消息属性由对应的参数表指定)的不同,采用唯一标识索引,存入Hash 表中统一管理,以提高核心算法频繁访问这些信息的效率.图2　协议P 的三个主体描述类4.2.2　协议分析核心部分在密码协议分析核心部分,首先需要完成协议的预处理和初始化,然后启用状态搜索算法从初始状态出发对协议描述的各个角色安全目标定理证明,在状态搜索过程中所采用的分裂算法则是SPA 系统能够快速构造出攻击序列的一个关键部分.协议的预处理过程.1.在确定的会话轮数l 下,对具有s 个可信服务器角色(该角色不可由非诚实主体扮演,如证书权威机构CA 等)的n 方密码协议P ,生成(n -s )!种除可信角色外诚实主体的会话组合,在具有攻击者协同参与情形下,引入p =n -s -1个可扮演各个诚实主体角色的攻击者(p 1,p 2,…,p n -s -1),生成(n -s )种主体会话组合,最后对(n -s )!+(n -s )种组合进行对称约简.例如对于双方密码协议P =〈a ,b 〉且l =1,会话组合为(a ,b ),(b,a ),(a ,p )和(p ,b ).2.对步1中的每种主体会话组合,主要应用变量替换等算法,生成各主体新的会话迹序列.进而求得所有诚实主体的规范序列空间N or Σ=∪(N orΣi (α,l )).3.设置攻击者本身知识集合D 0,D 0包括所有诚实主体I D 及其公钥,攻击者的密钥K E Y (私钥和共享密钥)及其生成的消息GEN ,也可是协议规范预设的其它公开信息.4.构造攻击者可以通过公开网络获取协议会话的知识集合D P ={t |〈σ,s ,t 〉∈N or Σ}.5.由步3和4生成攻击者的初始知识集合D =D 0∪D p .Πd ∈D ,若d ∈D 0,则记录d 的起源d →D 0;若d ∈D p ,则根据攻击者知识集D,对d 不断进行解密、分解等约简操作,直到D 集合中不再存在可约简的消息子项,对于d 的不可约简项d 1,d 2,…,d k ,分别记录d i 的起源节点d i →〈σs ,t s ,t ′s 〉.协议的初始化过程.在SPA 中,采用三元组(A ,B ,E )表示协议的运行迹状态(简称状态),其中A 为非空迹序列,B 为安全目标节点集,E 为正合节点集.针对CPA 模型描述的两类安全目标,分别采用如下方法来构造它的初始状态:(1)对于秘密性安全目标ΣSecret t ,构建一个新节点〈σ,t ,Δ〉,相应的初始状态为s 0=(Σ∪〈σ,t ,Δ〉, , ).(2)对于对应性安全目标ΣCorresp Λ,相应的初始状态为s 0=(Σ,Λ, ).建立初始状态后,SPA 采用宽度优先的原则进行状态搜索,主要包括状态搜索算法S earchA l g 和状态分裂算法S plit.算法1.　状态搜索算法.SearchA l g (){//建立初始状态StateS et ={(A 0,B 0,E 0)};while (S tateSet != ){//选取一个待分析状态(A i ,B i ,E i )=S elect (S tateS et );//用户预设处理策略处理该状态User Policy ((A i ,B i ,E i ));//判断迹序列A i 是否包含安全目标节点if (B i ΑA i ){//状态(A i ,B i ,E i )为安全状态S tateSet.Remove (A i ,B i ,E i );continue ;}//判断迹序列A i 中节点是否已全部正合if ((B i ⁄A i )&&(A i ΑE i ))//(A i ,B i ,E i )为不安全状态,3133期李建欣等:SPA :新的高效安全协议分析系统//正合序列A i描述了协议的一个攻击return FAL SE;//应用状态分裂算法,得到子状态集LL=S plit((A i,B i,E i));for each(A l,B l,E l)∈L{//状态有效性检查if(V ali date((A l,B l,E l))//将新状态并入集合S tateSetS tateS et=S tateSet∪{(A l,B l,E l)};}//状态(A i,B i,E i)分析完毕S tateSet.Remove(A i,B i,E i);}return TRU E;//协议无攻击}对于不能判定安全性的状态s=(A,B,E),其中A=〈σ1,t1,t′1〉,〈σ2,t2,t′2〉,…,〈σn,t n,t′n〉.是一个迹序列,SPA系统依据迹序列扩张方式,应用状态分裂算法S plit(算法3)求其子状态集,能够有效扩展状态搜索空间,避免大量冗余状态的产生.在状态分裂算法中首先需要应用算法Uni f y(算法2)求解出非正合节点的接收项t与攻击者初始知识集合D 的合一变量替换集合.变量替换合并运算Ψ.令集合A={a1,a2,…,a m},B={b1,b2,…, b n},其中a i=(<,d l,a,…,d j,a),b i=(δ,d l,b,…, d j,b),<,δ为变量替换,d l,…,d j∈D.变量替换合并运算Ψ的计算规则如下:(1)若集合A={(λ,d l,a,…,d j,a)},B={(δ,d l,b,…,d j,b)},则C=Ψ(A,B)定义为如果变量替换λ,δ不矛盾,则C={(λ∪δ,d l,a,…,d j,a,d l,b,…,d j,b)}, 否则C= ;(2)若集合A或B中的元素不只一项,则C=Ψ(A,B)定义为{Ψ(a,b)|a∈A,b∈B}. 特殊情况,当A= ,Ψ(A,B)=B;当B= ,Ψ(A,B)=A.算法从略.算法2.　U ni f y.输入:消息项t,攻击者初始知识集合D输出:t的子项组合与D中项可以合一的变量替换集合S Unif yUni f y(D,t){//初始化S Unif y为空集S Uni f y= ;//按照消息项递归定义方式求项t的子项组合集T={(t1,t2,…,t m)|u(t1,t2,…,t m)=t,u为代数式}for(each t的子项组合(t1,t2,…,t m)∈T){U= ;//U初始为空集//由合一算法M GU求项t i和d i的变量替换集合for(each t i∈{t1,t2,…,t m}){U i={(λi,d i)|λi(t i)=λi(d i),λi是变量替换,为项d i和t i最一般合一,d i∈D};//应用Ψ运算规则合并变量替换集合U=Ψ(U,U i);}//所有完全子项的合一集合求并集S Uni f y=S Unif y∪U;}}算法3.　状态分裂算法.输入:待分裂的状态s=(A,B,E)输出:分裂得到的子状态集合S′S plit(s){//从A中选取第一个非正合节点〈τ,t,t′〉=Sel N oEx t N ode(A);//标识〈τ,t,t′〉的前驱节点〈ω,p,p′〉=Prev N ode(A,〈τ,t,t′〉);//初始化子状态集为空集S′= ;//通过算法2求项t与D中元素的可合一变量替换集合Uni f y(D,t)={(<,m1,…,m k)|<(t)=u{<(m1)/x1,…,<(m k)/x k},u是代数式,m i∈D,i=1,2,…,k};for(each(<,m1,m2,…,m k)∈Uni f y(D,t)){//依据迹序关系,分为如下几类情形生成新的迹序状态if(Πm i,满足m i∈D0,1ΦiΦk){//添加一个新状态S′=S′∪{(<(A),<(B),<(E)∪{<(〈τ,t,t′〉)};continue;//处理下一个(<,m1,m2,…,m k)组}//集合M R包含所有不属于D0的m iM R={m1,m2,…,m k}-{m i|m i∈D0且1ΦiΦk};对于任一个m r∈M R,根据m r→〈σs,t s,t′s〉关系表可查询到其起源节点n s=〈σs,t s,t′s〉;if(ϖm r∈M R,其起源节点n s的变量替换满足<(〈σs,t s,t′s〉)∈<(A)且〈τ,t,t′〉ΜP n s){S′=S′∪ ;//不添加新状态continue;//处理下一个(<,m1,m2,…,m k)组}if(Πm r∈M R,其起源节点n s的变量替换满足<(〈σs,t s,t′s〉)∈<(A)且n sΜP〈τ,t,t′〉){S′=S′∪{(<(A),<(B),<(E)∪{<(〈τ,t,t′〉)};//添加一个新状态continue;//处理下一个(<,m1,m2,…,m k)组}413计 算 机 学 报2005年for(每个m r∈M R){if(m r起源节点n s的变量替换满足<(〈σs,t s,t′s〉)|<(A)){//正则迹中起源节点前的节点集G(m r)={<(〈σr1(α,l),t r1,t′r1〉),…,<(〈σrj(α,l),t rj,t′rj〉)};G=∪i G(m i)-<(A); //去除在A中已存在的节点for(G中节点每个满足偏序关系ΜP的有效排列Πi){A′=<(〈σ1,t1,t′1〉)…<(〈ω,p,p′〉)+Πi+<(〈τ,t,t′〉)…<(〈σn,t n,t′n〉);//添加一个新状态S′=S′∪{(A′,<(B),<(E)∪<(〈τ,t,t′〉))};}}}}//结束所有Uni f y(D,t)中项的遍历return(S′);//返回新生成的子状态集合}值得一提的是,由于SPA系统在协议预处理期间限制了攻击者角色数量和会话轮数,依据迹序关系,可匹配的节点将逐渐减少,从而保证了分裂算法收敛.除此外,算法中的变量替换都遵循类型匹配一致原则等方法都有效减小了状态搜索空间.与Athena系统的几点比较.　卡内基・梅隆大学的Song等[8,9]基于Strand空间研制的At hena系统是一种高效的密码协议自动分析工具.SPA与At hena、NRL协议分析器等分析工具共同之处是均采用构造攻击过程的方法分析协议的安全性;然而, SPA系统与At hena等其它系统相比采用了更有效的新模型和新的算法,主要体现在如下4个方面:(1)CPA模型中对密码协议的描述方式通常比Strand空间更为简洁.例如,用CPA模型描述Needham2Schroeder公钥协议[1]仅用4个节点(迁移函数),而在Strand空间中需要6个角色节点.(2)At hena基于的St rand空间模型属于图论方法,SPA基于的CPA模型侧重的是代数方法.在Strand空间中通过攻击者St rand处理消息运算,难以解决由运算产生的消息集无限性问题,因此,需要人为限制加密深度,并且消息项运算量大;而SPA 采用具有代数等式和自由生成元(基)的CPA代数方法解决消息运算无限生成问题,不需要限制运算方式(如加密深度),即解决了消息集无限性问题,因而分析结果更可靠.(3)协议的攻击序列表示方式不同,SPA采用算法更直接有效:At hena算法中St rand节点间属于一种消息绑定关系,搜索过程中状态图(bundles)无预期地生长;而SPA中迹序列是通过攻击者知识的递增过程表示.这些区别使基于CPA的SPA系统在序列生成过程中,收敛更集中,对于一些协议会显著提高其分析效率.(4)基于St rand的At hena系统在状态搜索中主体存在变量类型,从而变量替换中可能重复替换,出现冗余.基于CPA理论的SPA中,由于已有关于主体的约简理论,在预处理阶段对不同主体扮演各个角色已做了替换,状态搜索中迹序列中的主体都为常量类型.4.2.3　输出部分在SPA系统的输出部分,协议分析人员可以获得协议分析的结果信息以及各角色安全目标定理的证明树(结构如图3所示),其中每个节点除记录该状态的自身信息外,还包括分析过程中对该状态属性的判定结果等.图3　证明树结构对于证明树中的节点P i,如果其中存储的状态s=(A,B,E)属于不安全状态,则迹序列A是一个正合序列,描述了协议的具体攻击过程.一般来说,迹序列A中的节点是经过不断扩张生成的,它的来源可能是任意一个主体的迹序列,其中的消息项也都经过了多次的变量替换、等价变换,具体形式可以在下一节的应用实例分析中了解到.对于SPA系统的实现,我们在充分考虑协议分析算法实现效率的同时,提供了友好的人机交互界面和自动处理功能,以方便协议分析人员的使用.5　SPA系统的应用SPA系统是一个有效的网络系统安全性评测以及密码协议设计辅助工具.我们借助SPA系统分析了一些典型的密码协议,得到了较理想的结果,鉴于篇幅有限,这里仅给出BAN2Yahalom协议[10]的一个新攻击过程分析.5.1　BAN2Yahalom协议分析5133期李建欣等:SPA:新的高效安全协议分析系统。

2012年 序号 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
科研热词 推荐指数 形式化方法 2 马尔可夫链 1 非演绎模型 1 隐蔽技术 1 迹语义 1 证明搜索 1 相容性验证工具 1 模型驱动 1 模型开发环境 1 检测系统 1 时序行为 1 接入机制攻击 1 形式化验证 1 形式化分析 1 形式化 1 建模 1 嵌入式实时软件 1 密码协议 1 实时构件系统 1 实时性 1 安全进程代数 1 安全苛求系统 1 安全模型 1 安全性分析 1 多重代理签名 1 多次并发会话 1 基于身份的签名 1 基于身份的代理多重签名 1 可信计算 1 功能安全 1 信息流安全模型 1 串空间 1 uefi 1 tmn 1 csma/ca 1 cpn 1 bootkit 1 ad-hoc路由攻击 1
2008年 序号 1 2 3 4 5 6 7 8 9 10
科研热词 认证 机密性保护 最小特权 完整性保护 安全模型 安全协议 多级安全策略 多安全策略 串空间 802.11i
推荐指数 1 1 1 1 1 1 1 1 1 1
2009年 序号 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
科研热词 安全协议 形式化分析 远程证明 语义 访问控制 认证性 认证 计算机应用 角色 网络安全 模型检验 模型 时间模型 时间戳 无线传感器网络 无线ad hoc网络 形式化验证 工作流 委托授权 可追踪 双线性对 匿名认证 信任管理 保密性 串空间 webservice spin工具 spins协议 rbac promela p2p安全 kerberos 5 eca规则

对网络的被动攻击和主动攻击
源站 目的站 源站 目的站 源站 目的站 源站 目的站
截获 被动攻击
中断
篡改 主 动 攻 击
伪造
2．主动攻击与被动攻击
主动攻击：
对数据修改或创建，容易检测，很 难完全预防。
包括中断、修改和捏造 被动攻击： 偷听或监视传送，获得正在传 送的信息，很难被检测到。 截获属于被动攻击
对象加标签，而且给设备（如工作站、终端 和 磁盘驱动器）分配安全级别。如用户可以访问 一台工作站，但可能不允许访问装有人员工资 资料的磁盘子系统。
6、B3 级 B3级要求用户工作站或终端通过可信任途径连
接网络系统，这一级必须采用硬件来保护安全
系统的存储区。
7、A 级 这是橙皮书中的最高安全级别，这一级有时也称为 验证设计(ve-rified design)。A级附加一个安全系统 受监视的设计要求，合格的安全个体必须分析并通 过这一设计。另外，必须采用严格的形式化方法来 证明该系统的安全性。而且在A级，所有构成系统 的部件的来源必须安全保证，这些安全措施还必须 担保在销售过程中这些部件不受损害。例如，在A 级设置中，一个磁带驱动器从生产厂房直至计算机 房都被严密跟踪。
换一个角度讲，当今社会是一个信息化社会， 计算机通信网络在政治、军事、金融、商业、交
通、电信、文教等方面的作用日益增大。社会对
计算机网络的依赖也日益增强，尤其是计算机技
术和通信技术相结合所形成的信息基础设施已经
成为反映信息社会特征最重要的基础设施。
随着网络上各种新业务的兴起，比如电 子商务（Electronic Commerce）、电子现金 （Electronic Ｃash）、数字货币（Digital Cash）、网络银行（Network Bank）等的兴 起，以及各种专用网（比如金融网等）的 建设，使得安全问题显得越来越重要，因 此对网络安全的研究成了现在计算机和通 信界的一个热点。

网络安全概述摘要：当前网络及信息系统的安全日益突出，其所面临的各种各样的威胁问题，已经成为普遍的国际性问题。

面对安全威胁，网络及信息系统必须制定相应的安全策略。

当前网络及信息系统通过规定安全服务保证安全性，安全服务通过安全机制实现安全策略。

但在构建网络及信息系统的网络安全防护体系时有要考虑许多问题来合理的使用安全技术来应对安全问题。

网络安全防护体系是基于安全技术集成的基础之上，依据一定的安全策略建立起来的。

本文最初介绍了当前网络及信息系统所面临的各种安全威胁及及其特点，然后讲述了常见安全服务机制的原理及特点，最后讨论了具体一个网络及信息系统需要构建什么样的网络安全防护体系需要考虑的问题。

随着当今世界信息化建设飞速发展，计算机网络日益成为重要信息交换手段，认清网络的潜在威胁以及现实客观存在的各种安全问题，采取有效的安全技术，保障网络信息的安全。

网络安全威胁主要有对网络中信息的威胁和对网络中设备的威胁两种。

影响计算机网络的因素有很多，其所面临的威胁也就来自多个方面：计算机病毒的侵害：由于计算机病毒具有蔓延速度快、范围广等特点，是计算机网络系统的最大的威胁，造成的损失难以估计。

计算机病毒破坏的对象直接就是计算机系统或者网络系统。

一旦计算机感染病毒后，轻则使系统执行效率下降，重则造成系统死机或毁坏，使部分文件或全部数据丢失，甚至造成计算机系统硬件设备等部件的损坏。

黑客的威胁和攻击：黑客具有非常强的计算机网络系统知识，能熟练使用各种计算机技术和软件工具。

黑客善于发现计算机网络系统自身存在的系统漏洞。

漏洞成为黑客被攻击的目标或利用为攻击的途径，并对网络系统的安全构成了非常大的威胁。

目前，在各个国家计算机信息网络上的黑客攻击事件都是愈演愈烈。

软件设计的漏洞或“后门”而产生的问题：随着软件系统规模的不断增大，新的软件产品开发出来，系统中的安全漏洞或“后门”也不可避免的存在，比如我们常用的操作系统，无论是Windows还是UNIX几乎都存在或多或少的安全漏洞，众多的各类服务器、浏览器、一些桌面软件等等都被发现过存在安全隐患。

广 东 省 自然 基 金 资 助项 目 （ ｏ ０ ０ ３３ ） 中 山大 学 “ ８ ” 期 Ｎ ．６２１１， ９５ 二
基 金 资助 项 目 （ ｏ ９０ ３３ ７２ ０ Ｎ ． ０ １．２ ２４ ）
Ｉ 墨 ｌ 兰
（ Ｗ， ｉ Ｐ ， ） Ｉ Ｄ
ቤተ መጻሕፍቲ ባይዱ
１ ！．Ｊ ｌ一 ． ． ．＿ 读．． ． 器 ． ． ． ． ． Ｉ
Ｑ
Ｉ 堡 ｌ 竺
， ，） Ｄ
并转到第 ４ 否则， 步； 认证失败， 停止操作。 此次验
基：Ｐ ＝ ｌ ， Ｒ ＪＤ 以Ｉｗ ） ， ｐＩ ｝
验证 ：Ｐ Ｄ＝＝ １ ／ Ｉ ＰＤ， ｝Ｉ Ｒ Ｄｅ
一 １
尼
ｕｅ ｙ ｒ
产生： 兄
证实现了读写器对标签的身份认证。
Ｒ Ｒ）
计算 ：ＰＤ， 以 １＝ 小
Ｐ Ｄｅ 。 Ｉ Ｒ Ｐ Ｄ， Ｉ ：ＰＤ， ｑ Ｉ＝ Ｒ）
（）ｅｒ＿Ｒ ａｅ ｒｇ 服务器计算 Ｐ ＿ ４Ｓｎｅ ÷ ｅｄｒ ｒ ： ｒ ａ Ｉ－ Ｄ
ＨＩ ｉ Ｗｉ ｔ并将 肋 ｉ （ ｌ Ｉ） ＤＩ Ｉ ， Ｐ Ｒ 发给读写器， 读写器再将
１ 引 言
随着 Ｒ Ｉ ａｉ ｆｑｅｃ ｅｔ ｃｔｎ 射频识别） ＦＤ ｆｄ ｅｕｎｙ ｄｎｆａｏ， ｒ ｏｒ ｉ ｉ ｉ ｉ 的 广泛应用，Ｆ ＲＩ Ｄ系统的安全问题也日益突出。 ＦＤ系统存 ＲＩ 在的主要安全问题有保密性、 可跟踪性及个人隐私泄漏等，
这些问题已经严重地阻碍了 Ｒ Ｉ ＦＤ系统的进一步发展， 成
验证 ：ＰＤ，： Ｉ＝ Ｐ
算 ：ＰＤ ＤＩＷＩ） Ｉ ｝ ， Ｉ Ｉ Ｐ Ｒ
ＰＤ Ｉ
其转发送给标签。
图 １ ＲＦＤ 系 统 动 态 加 密安 全 协 议 Ｉ

V ol.14, No.10 ©2003 Journal of Software 软 件 学 报 1000-9825/2003/14(10)1740 安全协议20年研究进展∗卿斯汉+ (中国科学院 信息安全技术工程研究中心,北京 100080)(中国科学院 软件研究所 信息安全国家重点实验室,北京 100080)Twenty Years Development of Security Protocols ResearchQING Si-Han +(Engineering Research Center for Information Security Technology, The Chinese Academy of Sciences, Beijing 100080, China) (State Key Laboratory of Information Security, Institute of Software, The Chinese Academy of Sciences, Beijing 100080, China) + Corresponding author: Phn: 86-10-62635150, Fax: 86-10-62635150, E-mail: qsihan@Received 2003-02-20; Accepted 2003-07-07Qing SH. Twenty years development of security protocols research. Journal of Software , 2003,14(10): 1740~1752. /1000-9825/14/1740.htmAbstract : This paper is a survey on the twenty years development of security protocols research. The state of the art in the application of formal methods to the design and analysis of security protocols is presented. Some major threads and emerging trends of research in this area are outlined.Key words : security protocol; design; analysis; formal methods摘 要: 总结了安全协议的20年研究进展情况,指出形式化方法在安全协议的设计与分析中的重要应用.对安全协议的若干热点研究方向进行了归纳和展望.关键词: 安全协议;设计;分析;形式化方法中图法分类号: TP309 文献标识码: A安全协议提供安全服务,是保证网络安全的基础.近年来,安全协议越来越多地用于保护因特网上传送的各种交易,保护针对计算机系统的访问.但是,设计一个符合安全目标的安全协议是十分困难的.因此,我们必须借助形式化方法,对安全协议进行设计和分析.自20世纪70年代末期以来,安全协议的研究已经成为一个热点,有众多的形式化研究方法涌现出来.本文是对这一重要研究领域发展20年的简要概括和总结.本文第1节阐述安全协议的背景与基本概念;介绍重要的安全协议;对安全协议发展的20年作一简要回顾.第2节讨论安全协议的有代表性的形式化分析方法,其中包括基于知识与信念推理的模态逻辑方法、基于定理证明的分析方法、Spi 演算方法等.第3节讨论安全协议的设计,其中包括安全协议的设计原则、安全协议的形∗ Supported by the National Natural Science Foundation of China under Grant No.60083007 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.G1999035810 (国家重点基础研究发展规划(973))第一作者简介: 卿斯汉(1939－),男,湖南隆回人,研究员,博士生导师,主要研究领域为信息系统安全理论和技术.卿斯汉:安全协议20年研究进展1741式描述语言、安全协议的基本假设和针对安全协议的攻击.第4节进行展望,讨论安全协议研究领域今后的发展方向.1 安全协议1.1 背景与基本概念安全协议,有时也称作密码协议,是以密码学为基础的消息交换协议,其目的是在网络环境中提供各种安全服务.安全目标是多种多样的.例如,认证协议的目标是认证参加协议的主体的身份.此外,许多认证协议还有一个附加的目标,即在主体之间安全地分配密钥或其他各种秘密.非否认协议的目标有两个:一个是确认发方非否认(non-repudiation of origin),亦即非否认协议向接收方提供不可抵赖的证据,证明收到消息的来源的可靠性;另一个是确认收方非否认(non-repudiation of receipt),亦即非否认协议向发送方提供不可抵赖的证据,证明接收方已收到了某条消息.电子商务协议的目标除认证性、非否认性之外,还有可追究性、公平性等等.Needham-Schroeder协议[1]是最为著名的早期的认证协议,许多广泛使用的认证协议都是以Needham- Schroeder协议为蓝本而设计的.Needham-Schroeder协议可分为对称密码体制和非对称密码体制下的两种版本,分别简称为NSSK协议和NSPK协议.这些早期的经典安全协议是安全协议分析的“试验床”,亦即每当出现一个新的形式化分析方法,都要先分析这几个安全协议,验证新方法的有效性.同时,学者们也经常以它们为例,说明安全协议的设计原则和各种不同分析方法的特点.安全协议的设计极易出错,即使我们只讨论安全协议中最基本的认证协议,其中参加协议的主体只有两三个,交换的消息只有3~5条,设计一个正确的、符合认证目标的、没有冗余的认证协议也十分困难[2,3].因此,20年来,为了应对这一挑战,人们设计了不同种类的形式化分析方法,投入了大量的精力,取得了可喜的成果.安全协议设计与分析的困难性在于:(1) 安全目标本身的微妙性.例如,表面上十分简单的“认证目标”,实际上十分微妙.关于认证性的定义,至今存在各种不同的观点;(2) 协议运行环境的复杂性.实际上,当安全协议运行在一个十分复杂的公开环境时,攻击者处处存在.我们必须形式化地刻画安全协议的运行环境,这当然是一项艰巨的任务;(3) 攻击者模型的复杂性.我们必须形式化地描述攻击者的能力,对攻击者和攻击行为进行分类和形式化的分析;(4) 安全协议本身具有“高并发性”的特点.因此,安全协议的分析变得更加复杂并具有挑战性.1.2 重要的安全协议从1978年Needham-Schroeder协议的诞生算起,安全协议的发展已经历经20余年了.除了NSSK协议和NSPK协议之外,早期著名的经典安全协议还有Otway-Rees协议[4]、Yahlom协议[5]、大嘴青蛙协议[5]等,以及一些重要的实用协议,如Keberos协议[6]、CCITT X.509协议[7]等.1997年,Clark和Jacob[8]对安全协议进行了概括和总结,列举了一系列有研究意义和实用价值的安全协议.他们将安全协议进行如下分类:(1) 无可信第三方的对称密钥协议.属于这一类的典型协议包括以下ISO系列协议[9]:ISO对称密钥一遍单边认证协议、ISO对称密钥二遍单边认证协议、ISO对称密钥二遍相互认证协议、ISO对称密钥三遍相互认证协议、Andrew安全RPC协议[10]等.(2) 应用密码校验函数(CCF)的认证协议.属于这一类的典型协议包括以下ISO系列协议[11]:ISO应用CCF 的一遍单边认证协议、ISO应用CCF的二遍单边认证协议、ISO应用CCF的二遍相互认证协议、ISO应用CCF的三遍相互认证协议.(3) 具有可信第三方的对称密钥协议.属于这一类的典型协议包括NSSK协议[1]、Otway-Rees协议[4]、Yahlom协议[5]、大嘴青蛙协议[5]、Denning-Sacco协议[12]、Woo-Lam协议[13]等.(4) 对称密钥重复认证协议.属于这一类的典型协议有Kerberos协议版本5、Neuman-Stubblebine协议[14]、Kao-Chow重复认证协议[15]等.(5) 无可信第三方的公开密钥协议.属于这一类的典型协议包括以下ISO系列协议[16]:ISO公开密钥一遍单边认证协议、ISO公开密钥二遍单边认证协议、ISO公开密钥二遍相互认证协议、ISO公开密钥三遍相互认1742 Journal of Software 软件学报 2003,14(10) 证协议、ISO 公开密钥二遍并行相互认证协议、Diffie-Hellman 协议[17]等.(6) 具有可信第三方的公开密钥协议.属于这一类的典型协议有NSPK 协议[1]等.1.3 安全协议发展20年的简要回顾1.3.1 Needham-Schroeder 协议及其改进NSSK 协议如下所示,其中A 是发起者,B 是响应者,S 是认证服务器,用于为通信双方之间分配会话密钥..}1{: .5.}{: .4.},{: .3.}},{,,,{: .2.,,: .1AB AB BS AS BS K b K b K AB K K AB AB a a N B A N A B A K B A A K K B N A S N B A S A −→→→→→在协议的第1步,A 向S 发送A ,B 和临时值.第2步,S 生成A 和B 之间的会话密钥,并向A 发送,B 和以及用S 和B 之间的共享密钥加密的证书{.第3步,A 向B 转发这个证书.第4步,B 解密这个证书,得到,并用它加密临时值之后发送给A .第5步,A 向B 发送用加密的−1.这里,−1可用任何一个的函数代替,表示这一消息来自A ,并非来自B .a N AB K a N AB K bs K },A K AB AB Kb b N AB K b N b N N NSPK 协议如下:.}{: .3.},{: .2.},{: .1B A B K b K b a K a N B A N N A B A N B A →→→协议假定双方都知道对方的公开密钥.A 首先生成临时值N a ,与其标识符级连,用B 的公开钥加密后发送给B .B 生成临时值N b ,与N a 级连后用A 的公开钥加密后发送给A .因此,B 通过证明B 能读第1条消息从而响应了发起者的请求.最后,A 返回用B 的公开钥加密的.该协议的目标是,双方可以共享值N b N a 与N b ,每一方都将这些值与对方相结合,没有第三方可以掌握它们.例如,这个协议可以用于以下场合,即这两个值一起散列后,生成一个共享的对称密钥,作为一次会话密钥应用.NSSK 协议和NSPK 协议自问世以来,受到了广泛的关注.BAN 逻辑以NSSK 协议和NSPK 协议为试验床,对它们进行了分析.对NSSK 协议最为著名的攻击是Denning-Sacco 攻击[12].Denning 和Sacco 认为,NSSK 协议的主要安全问题在于响应者B 无法确定消息3的新鲜性.攻击者可以破译密钥,并重放消息3给B ,然后完成整个协议.Denning 和Sacco 建议应用时间戳修改NSSK 协议,修改后的Denning-Sacco 协议如下:.},,{: .3.}},,{,,,{: .2.,: .1BS AS BS K AB K K AB AB T K A B A T K A T K B A S B A S A →→→其中,T 是时间戳.在上述协议中,响应者B 可以验证消息3的新鲜性.因此,Denning-Sacco 协议不需要NSSK 协议中的第4和第5条消息.1990年,Boyd [18]通过实例指出,如果应用序列密码,则在NSSK 协议中,密文消息4与5之间的差别只有1个比特,协议极易受到攻击.针对NSPK 协议的最有名的攻击来自Lowe [19].Lowe 指出,NSPK 协议的主要安全缺陷在于其中的消息2.由于消息中没有B 的标识符,攻击者可以假冒B 的身份发送消息2.Lowe 改进后的NSPK 协议如下:.}{: .3.},,{: .2.},{: .1B A B K b K b a K a N B A N N B A B A N B A →→→从1978年NSPK 协议问世以来,到Lowe 于1996年发现NSPK 协议的安全缺陷,已经过去了大约17年之久.安全协议设计的困难性和安全协议分析的微妙性,由此可见一斑.卿斯汉:安全协议20年研究进展17431.3.2 Dolev-Yao 模型 1983年,Dolev 和Yao 发表了安全协议发展史上的一篇重要的论文[20].该论文的主要贡献有两点.其一是将安全协议本身与安全协议所具体采用的密码系统分开,在假定密码系统是“完善”的基础上讨论安全协议本身的正确性、安全性、冗余性等课题.从此,学者们可以专心研究安全协议的内在安全性质了.亦即,问题很清楚地被划分为两个不同的层次:首先研究安全协议本身的安全性质,然后讨论实现层次的具体细节,包括所采用的具体密码算法等等.第2点贡献是,Dolev 和Yao 建立了攻击者模型.他们认为,攻击者的知识和能力不能够低估,攻击者可以控制整个通信网络.Dolev 和Yao 认为攻击者具有如下能力:(1) 可以窃听所有经过网络的消息;(2) 可以阻止和截获所有经过网络的消息;(3) 可以存储所获得或自身创造的消息;(4) 可以根据存储的消息伪造消息,并发送该消息;(5) 可以作为合法的主体参与协议的运行.Dolev 和Yao 的工作具有深远的影响.迄今为止,大部分有关安全协议的研究工作都遵循Dolev 和Yao 的基本思想.1.3.3 BAN 逻辑BAN 逻辑[5]开创了安全协议形式化分析的先河,是一项开拓性的工作.BAN 逻辑简单、实用,抽象程度高,可以揭示安全协议中的安全缺陷与冗余性.例如,BAN 逻辑分析发现了CCITT X.509标准[7]推荐草案中的安全漏洞.BAN 逻辑的直观性与简单性主要表现在:第一,BAN 逻辑不区分看见一条消息和理解一条消息;第二,BAN 逻辑的信念演化过程是单调递增的;第三,BAN 逻辑不讨论trust;第四,BAN 逻辑不讨论知识;第五,BAN 逻辑假设参加协议的主体是诚实的,他们都忠诚地根据协议的法则执行协议;第六,BAN 逻辑假设加密系统是完善的(perfect)等等.但是,BAN 逻辑的简单性也为BAN 逻辑分析方法带来了局限性,使BAN 方法的抽象级别过高,分析范围过窄.例如,由于BAN 逻辑不能对知识进行推理,因此BAN 逻辑只能分析协议的认证性质,而不能分析协议的保密性质.然而在现实中,通常的密钥分配协议要实现保密性质和认证性质两个重要目标.1990年,Nessett [21]引入一个简单的例子,试图说明BAN 逻辑本身存在一个重要的安全问题.Nessett 协议如下:{}{}.: .2.,: .11AB A K b K AB a N A B K N B A →→−Nessett 用BAN 逻辑分析上述协议,得出是良好的会话密钥这一结论.但是,任何主体都可以通过A 的公开密钥获得.据此,Nessett 认为,BAN 逻辑本身存在一个重要缺陷,该缺陷源于BAN 逻辑的分析范围.因为BAN 逻辑只考虑分配密钥和身份认证的问题,但未考虑哪个主体不应当获得密钥的问题,亦即,未考虑保密性的问题.AB K AB K BAN [22]对Nessett 的批评答复如下:在BAN 逻辑的论文中已经清楚地说明,BAN 逻辑只讨论诚实主体的认证问题,并不关心检测非授权地暴露秘密的问题.在Nessett 协议中,A 在消息1中公开了,故Nessett 的假定不符合BAN 的基本假定.因此,Nessett 从不合理的初始假定推导出了不合理的结论,而BAN 逻辑本身并不能防止建立不合理的初始假定集合.AB K B A A AB K →← believes 虽然,我们不能通过Nessett 协议说明BAN 逻辑本身存在缺陷,但Nessett 的反例启示我们,BAN 逻辑的推理分析依赖于我们所作的基本假设和初始假设.如果非形式化的初始假设错了,则通过形式化分析之后常常得出错误的结论.1.3.4 CSP 方法与模型校验技术1996年,Lowe [19]首先采用CSP(通信顺序进程)方法和模型校验技术对安全协议进行形式化分析.他应用CSP 模型和CSP 模型校验工具FDR 分析NSPK 协议,并令人惊讶地发现了一个近17年来未知的攻击.Lowe 的论文发表不久,Roscoe [23]对CSP 和FDR 的组合作了进一步的研究.他们认为,CSP+FDR 是形式化分析安全协议1744Journal of Software 软件学报 2003,14(10)的一条新途径. 模型校验技术是验证有限状态系统的自动化分析技术,是一种安全协议的自动验证工具.Lowe 等学者应用CSP 方法的成功,促进了这一领域的发展.Schneider [24~26]发表了一系列关于CSP 方法应用的论文,应用CSP 方法讨论安全协议的安全性质、匿名等问题;分析了各种安全协议,例如NSPK 协议、非否认协议等.美国卡内基-梅隆大学以Clarke 教授为首的研究小组,长期从事定理证明和自动校验的研究.他们提出了一种通用的模型校验器,构造了一种新型的模型及其代数理论,并证明了该模型的有效性.Marrero,Clarke 和Jha [27]应用该方法对NSPK 协议进行分析,得到了与Lowe 相同的结论[19].Mitchell [28]的方法是通过状态计数工具Murphi 分析安全协议,从安全协议可能到达的状态,分析安全协议是否安全.他应用Murphi 分析了一系列著名的安全协议,成功地发现了所有已知的攻击.1.3.5 串空间方法Thayer,Herzog 和Guttman [29~31]提出了串空间(strand space)模型,这是一种结合定理证明和协议迹的混合方法.事实证明,串空间模型是分析安全协议的一种实用、直观和严格的形式化方法.串(strand)是参与协议的主体可以执行的事件序列.对于诚实的主体,该事件序列是根据协议定义,由发送事件和接收事件组合而成的.此外,该模型还定义了攻击者串,描述攻击者的行为.串空间是由协议参与者,包括诚实主体和攻击者的串组成的串集合.串集合之间可以穿插组合,使一个串的发送消息对应于另一个串的接收消息.丛(bundle)是串空间中的重要概念,表示一个完整的协议交换串空间的子集.丛可以表示为有限无环图,其中的边表示结点间的因果依赖关系.在串空间模型中,共有两种不同类型的边:(1) ,表示n 发送消息M 被接收;21n n →12n (2) ,表示n 是在同一个串上的直接因果前驱.21n n ⇒12n Thayer,Herzog 和Guttman 应用串空间模型,分析了多个经典安全协议,成功地找到目前已经发现的攻击. Perrig 和Song [32]等人对串空间模型进行了重要的扩展,将其增强和优化,并将串空间模型推广到分析三方安全协议.Song [33]应用串空间模型,研制出安全协议自动检验工具——Athena.Athena 结合定理证明和模型校验技术,证明从一些初始状态开始,进行回退搜索.初始状态是满足某种安全属性的丛.1.3.6 安全协议目标的讨论关于协议安全目标最早的讨论源于1993年van Oorschot 的工作[34].van Oorschot 给出了关于认证协议的6种不同形式的认证目标:(G1) Ping 认证:.says believes Y B AG1说明,A 相信B 最近发送过消息Y ,隐含B 当前是激活的,亦即协议本回合开始后,B 采取了行动.(G2) 实体认证:)).),((,( says believes Y R G R Y B A AA 不仅认证B 在A 所执行的当前协议回合中是激活的,而且B 参与了与A 在当前协议回合中的对话. (G3) 安全密钥建立:. believes B A A K →←−这里,表示K 是A 的适用于B 的未经确认的密钥.除了A 和B 之外,任何其他主体都不知道也不能推导出K .G3说明,A 相信除了B 之外,任何其他主体都不会与A 共享密钥K .当B 最终获得K 之后,A 相信K 是A 和B 之间良好的会话密钥.B A K →←−(G4) 密钥确认:. believes B A A K →←+这里,表示K 是A 的适用于B 的已经确认的密钥.A 知道K ,且A 已经从B 那里收到了证据(密钥确认),说明B 确实也知道K .其他任何主体都不知道也不能推导出K .G4说明,A 相信K 是A 和B 之间的共享密钥,且B 向A 提供了知道K 的证据.G4表示K 是A 和B 之间良好的会话密钥,且确认B 知道K .B A K →←+卿斯汉:安全协议20年研究进展1745(G5) 密钥新鲜性:).( believes k fresh A G5说明,A 相信密钥K 是新鲜的.(G6) 互相信任共享密钥:. believes believes A B B A K →←− G6说明,A 相信B 相信K 是适用于A 的未经确认的密钥.注意,此处B 的信念超出了A 的控制范围.因此,以A 的观点,G6的意义在于B 已经确认了A 的身份,即B 确认A 是与B 共享密钥K 的主体.1996年,Gollmann [35]正式提出讨论认证协议的目标,其论文的题目就是“实体认证的含义是什么?”.关于安全目标的进一步讨论,可参见文献[19,35,36].2 安全协议的形式化分析2.1 基于知识与信念推理的模态逻辑方法模态逻辑方法是分析安全协议最直接、最简单的一种方法.它们由一些命题和推理规则组成,命题表示主体对消息的知识或信念,而应用推理规则可以从已知的知识和信念推导出新的知识和信念.Syverson [37]阐述了在安全协议的分析中,知识、信念和语义之间的关系与相互作用.在这类方法中,最著名的是BAN 类逻辑,其中包括BAN 逻辑[5]、GNY 逻辑[38]、AT 逻辑[39]、VO 逻辑[34]和SVO 逻辑[40].其他相近的工作还包括:Bieber 逻辑——CKT5[41];Syverson 逻辑——KPL [42];Rangan 逻辑[43]; Moser 逻辑[44];Yahalom,Klein 和Beth 的YHK 逻辑[45];Kessler 和Wedel 的AUTOLOG 逻辑[46]等.1999年,Kindred 在他的博士论文[47]中提出了密码协议的生成理论——RV 逻辑,是这方面的又一个新成果.BAN 逻辑问世后,第一个对它进行增强的是GNY 逻辑.GNY 的逻辑公设有44个之多.并且,若21C C 是逻辑公设,则对任何主体P ,21||C P C P ≡≡也是逻辑公设. GNY 逻辑对BAN 逻辑的重要改进与推广有以下几个方面:(1) 通过新增加的逻辑构件与法则,推广了BAN 逻辑的应用范围,例如,GNY 逻辑不局限于分析认证协议,还可以分析某些应用单向函数的密码协议;(2) 增加了“拥有密钥”的表达式,增强了GNY 逻辑本身的表达能力;(3) 在GNY 逻辑中,区分一个主体收到的消息和一个主体可用的消息;(4) 在GNY 逻辑中,进一步区分一个主体自己生成的消息和其他消息;(5) 在GNY 逻辑的分析中,在理想化协议中保留明文,而在BAN 逻辑分析中,明文在认证过程中不起作用.GNY 逻辑的缺点是过于复杂,因此不实用.但是,它仍然在安全协议20年的发展史中占有重要的地位.GNY 逻辑的出现,使我们对BAN 逻辑有了更加深刻的认识.AT 逻辑为BAN 逻辑构造了一个简单的语义模型,是对BAN 逻辑的一种重要改进.类似于GNY 逻辑,AT 逻辑对BAN 逻辑的本质与局限性进行了深入的分析,并获得相近的结论.但是,GNY 得到的是一个更加复杂的逻辑.AT 逻辑比BAN 逻辑更接近传统的模态逻辑:它包含一个详细的计算模型,增加了模型论语义,表达能力更强,因而将BAN 逻辑向前推进了一大步.AT 逻辑对BAN 逻辑的改进还包括:(1) 对BAN 逻辑中的定义和推理法则进行整理,抛弃其中语义和实现细节中不必要的混和;(2) 对某些逻辑构件引入更直接的定义,免除对诚实性进行隐含假设;(3) 简化了推理法则,所有的概念都独立定义,不与其他概念相混淆;(4) 整个逻辑只有两条基本推理规则,即Modus Ponens 规则和Necessitation 规则.VO 逻辑的贡献则是扩展了BAN 逻辑的应用范围.Diffie-Hellman 协议[17]是许多近代密钥分配协议的基础,VO 逻辑的设计目标之一就是增加分析Diffie-Hellman 协议的能力,进而可以分析IETF 标准——因特网密钥交换协议IKE [48]和SSL 等.VO 逻辑的另一个重要特点是,细化了认证协议的认证目标,给出了6种不同形式的认证目标.1746 Journal of Software软件学报2003,14(10)SVO逻辑吸取了BAN逻辑、GNY逻辑、AT逻辑和VO逻辑的优点,将它们集成在一个逻辑系统中.在形式化语义方面,SVO逻辑对一些概念作了有别于AT逻辑的重新定义,从而取消了AT逻辑系统中的一些限制.SVO逻辑所用的记号与BAN类逻辑相似,其中特有的符号共有12个.应用SVO逻辑对安全协议进行形式化分析可以分为3个步骤:(1) 给出协议的初始化假设集Ω,即用SVO逻辑语言表示出各主体的初始信念、接收到的消息、对所收到消息的理解和解释;Γ(2) 给出协议可能或应该达到的目标集,即用SVO逻辑语言表示的一个公式集;(3) 在SVO逻辑中证明结论Ω┣Γ是否成立,若成立,则说明该协议达到了预期的设计目标,协议的设计是成功的.SVO逻辑是BAN类逻辑中的佼佼者,它的理论基础更加坚实,在实用上仍然保持了BAN逻辑简单、易用的特点,因此被广泛接受.应用SVO逻辑,不仅成功分析了各种认证协议,也成功地分析了在电子商务中应用日益广泛的非否认协议[49,50].2.2 基于定理证明的分析方法这种方法可以分为两类,一类是推理构造方法,另一类是证明构造方法.在推理构造方法中,重要的工作包括:(1) Meadows的NRL协议分析器方法[51].它发现了许多已知的和未知的安全协议漏洞,并成功地用于分析IETF标准——因特网密钥交换协议IKE[52];(2) Cervesato等学者的基于线性逻辑的协议验证方法[53];(3) Millen 等学者的基于逻辑规则的协议验证方法[54].推理构造方法的优点是可以发现攻击,并可以证明协议在多回合运行下的正确性.其缺点是需要用户介入,防止状态爆炸.Kemmerer等学者研制的Ina Jo和ITP是证明构造方法的典型代表[55].这一领域的另一项重要工作是Paulson的基于归纳的定理证明方法[56,57].他研制的定理证明器Isabelle可以应用归纳方法分析安全协议.Thayer,Herzog和Guttman随后提出的串空间模型,在很多方面继承和发扬了Paulson方法的基本思想.证明构造方法的优点是可以分析无限大小的协议,不限制主体参与协议运行的回合.其缺点是证明过程不能全部自动化,需要人工进行“专家式”的干预,在使用范围上受到一定的限制.2.3 Spi演算方法1997年,Abadi和Gordon在Pi演算[58]的基础上建立了Spi演算[59]方法.这种方法根据Dolev-Yao模型,假定协议执行的每一步都可能与攻击者的执行步骤交叉.Pi演算是并发计算的基础,它引入了通道和作用域的概念.由于作用域之外的进程不能访问通道,在一定程度上保证了通道通信的安全性.Spi演算对pi演算进行了增强与扩充,增加了支持密码系统的原语,使Spi演算可以描述基于密码系统的安全协议.除了Abadi和Gordon的研究之外,应用Spi演算分析安全协议的重要工作还有文献[60~62].Amadio和Lugiez[60]应用Spi演算方法分析对称密钥安全协议;Abadi和Blanchet[61]应用Spi演算方法分析公开密钥安全协议;Amadio和Prasad[62]在应用Spi演算方法分析时,对攻击者的消息构造能力进行了刻画和限制.目前,针对Spi演算的研究主要集中在以下两个方面:一方面对Spi演算进一步扩展,扩大它的应用范围;另一方面.进一步研究Spi演算的语义,为安全协议的分析提供更为坚实的基础.3 安全协议的设计在安全协议发展的20年历史中,形式化方法主要用于分析安全协议.但是,形式化方法用于指导安全协议的设计同样有效.近年来,关于这方面的研究日益增多[63~65].3.1 安全协议的设计原则在设计协议时,如何保证安全协议能够满足保密性、无冗余、认证身份等设计目标呢?经过总结,我们可以提出以下安全协议的设计原则.(1) 设计目标明确,无二义性;。

暗入口，英文名为trap door，一种隐蔽的软件或硬件机制。

激活后，就可避过系统保护机制，从而绕过安全性控制获得系统或程序的访问权。

安全协议（Security protocol，又称密码协议，Cryptographic protocol）。

安全协议是建立在密码体制基础上的一种交互通信协议，它运用密码算法和协议逻辑来实现认证和密钥分配等目标。

安全协议可用于保障计算机网络信息系统中秘密信息的安全传递与处理，确保网络用户能够安全、方便、透明地使用系统中的密码资源。

目前，安全协议在金融系统、商务系统、政务系统、军事系统和社会生活中的应用日益普遍，而安全协议的安全性分析验证仍是一个悬而未决的问题。

在实际社会中，有许多不安全的协议曾经被人们作为正确的协议长期使用，如果用于军事领域的密码装备中，则会直接危害到军事机密的安全性，会造成无可估量的损失。

这就需要对安全协议进行充分的分析、验证，判断其是否达到预期的安全目标。

安全状态secure state：在未授权情况下，不会出现主体访问客体的情况。

安全需求security requirements：为使设备、信息、应用及设施符合安全策略的要求而需要采取的保护类型及保护等级。

安全特征security features：与安全相关的系统的软硬件功能、机理和特性。

安全评估security evaluation：为评定在系统内安全处理敏感信息的可信度而做的评估。

安全配置管理secure configuration management：控制系统硬件与软件结构更改的一组规程。

其目的是来保证这种更改不致违反系统的安全策略。

安全内核security kernel：控制对系统资源的访问而实现基本安全规程的计算机系统的中心部分。

安全过滤器security filter：对传输的数据强制执行安全策略的可信子系统。

安全过滤带宽是指防火墙在某种加密算法标准下，如DES(56位)或3DES(168位)下的整体过滤性能。