用串空间分析路由协议SGSR.pdfVIP

第28卷第4期 淮北煤炭师范学院学报(自然科学版) V01．28 No．g 2007年1 2月 Joumal of Huaibei Coal Industry Teachers College(Natural Science) Dec．2007 用串空间分析路由协议SGSR 郭宇燕 ，魏仕民2 (1．淮北煤炭师范学院数学系，安徽 淮北235000；2．淮北煤炭师范学院计算机科学与技术系，安徽 淮北 235000) 摘 要：用形式化方法分析安全协议是协议分析的有效手段，近年来，出现了众多的研究方法．串空问模型是一种新 兴的形式化分析工具，其中，“理想”和“诚实”两个概念简化了分析协议的步骤．首次利用串空间理论对由徐兰芳提出 的一种安全的Ad Hoc网络路由协议SGSR进行分析，并分析了它的认证性和机密性，结果证明此协议能够达到协议 的目标． 关键词：SGSR协议；串空间；认证性；机密性 中图分类号：TN 918．1 文献标识码：A 文章编号：1672—7177(2007)04—0049—03 串空间是近几年来出现的一种分析安全协议的新方法，1998年由Thayer F6brega，Herzog和Guttman 等人提出的。串空间模型是一种结合迹和定理证明的混合方法，它最大的优点是简洁，串空间模型既可以证 明协议的正确性，还可以找出协议本身的缺陷，它的出现引起人们的广泛关注． 1 串空间 (Strand space)模型 串是协议中诚实者或攻击者行为的一个序列，即发送接受消息的序列．记A为协议执行中所有可能消 息的集合，可以分为明文消息集 和密钥消息集 K两部分，其中元素称为项(term)．若 Ot∈A，0∈{+，一)， 称为有符号项，可记为+ 或一 ．(A) 是全体有符号的有限序列集合．它的元素形式为( ， … )． 串空间是指一个集合∑，并在此集合上有一个轨迹映射(trace)tr：∑一(A) ．下面是串空间的基本概念 f】J． ‘ 定义1．1 结点和串 结点凡是二元组(s， )，其中s∈∑，(1≤islength(tr(s)))．结点集合记为Ⅳ．则称结点s， 属于串 s．显然每个结点属于唯一的串．若 n=s， ∈N，则index(n)：i，strand(n)=s．term(n)记为(tr(s)) ，即 串s路径中的第i个消息项．Un_term(n)记为((tr(s)) )z，即串s路径中的第 个消息项中的无符号部分， 成为无符号语句． 定义1。2 人点 ， 令，为无符号项集合．节点／-t E N是，的进入点，当且仅当term(／-t)=+n，其中n∈L且对所有的／-t +／-t，term(／-t )簪L 定义1．3 起源 无符号项 t起源于 n∈N，当且仅当term( )的符号为正，且对 ／-t的任何一个前驱节点 ／-t ，有 t甓term (／-t，)．无符号项t是唯一起源的，当且仅当z唯～起源于 n． 定义1．4 h为g的一个子项，即h c g，该关系用理想的概念可以定义为g∈Ikl h】． 串空间基本理论(详细理论见文献[1—21) 定义1-5 设K K，K=eku sk u hk， ∈，c其中e 为加密密钥集 s 为签名密钥集，触为HMAC函数 收稿日期：2007—10—25 基金项目：国家自然科学基金项目；安徽省自然科学舔金项日(070412052) 作者简介：郭字燕(1984一 )，女，安徽淮北人，硕士生，研究方向：信息安全． 通讯作者：魏fj民(1962 )，男，安徽巢湖人，博士，教授，研究方向：网络与信息安全 5O 淮北煤炭师范学院学报(自然科学版) 2007年 密钥集．子集 ，c A称为 的K理想( 一idea1)，如果对所有的h∈，，g∈A，且 ，满足：(1)hg，gh∈， (2) {h} ∈，，K∈ek．包含 h的最小，c理想记为lk【h】．并且若 S A，则 ， 【S】=u s [ 】． 定理1 6 假设 ∈ S A，且对任意 s