节点基于串空间极小元理论改进woo-lam协议认证性分析

基于串空间极小元理论的改进Woo-Lam协议的认证性分析基于串空间极小元理论的改进Woo-Lam协

议的认证性分析

电脑编程技巧与维护

基于串空间极小元理论的改进Woo-Lam协议的认证性分析

余磊,顾维娜,王猛

(淮北煤炭师范学院计算机科学与技术学院,淮北235000)

摘要:通过对Woo—Lam协议自身特点的分析,把协议分为信息收集和主体认证两

部分;并参考原协议的攻击方

—Lain协议的认证部分进行认证式,基于串空间模型运用极小元理论对改进Woo性分析.

关键词:串空间;极小元;认证性

AuthenticationAnalysisofImprovementWoo-LamProtocolB as edonthe

MinimalMembersTheoryofStrandSp ace

YULei.GUWeina,WAN GMeng

(SchoolofComputerScience&Technology,HuaibeiCoalIndustryTeacherCollege,Huaibei235000)

Abstract:ThroughtheanalysistotheWoo-LalTIprotocolSowncharacteristics,theprotocolwasdividedintotwosectionswhichrespectivelyweretheinformationcollectionpartandtheauthenticatespart,andreferredtotheattackformsoftheoriginalprotocol,basedontheminimalmemberstheoryofstrandsp acemodel,theauthenticat

ionanalysiswascarriedontotheauthenticatespartoftheimprovementWoo-Lainprotoco1.

Keywords:Strandspace;minimalmembers;authentication 1串空间模型【l1习

串是协议中诚实主体或入侵者行为的一个发送接收消息

的有限序列.设集合A是在协议执行过程中所有可能交换的

消息的集合,A中的元素称为项,tl c t表示tl是t的子项.T C_

A是正文集合.K C_A是密钥集合,其中KN T=Rb. 1.1串空间基本概念

定义1符号项是一个二元组&l t;o r,a>,其中ae A且o r={+,一

},记符号项为+t或一t.(士A)是符号项的有限序列集合,记(士A)中的元素为《,a,>,.. .<,ar.一个串空间是指一个定义在A上的集合乏以及该集合上的迹映射:tr:一f士A】 '.定义2节点是一个二元组&l t;s j),其中s E?且i为满足1?^朗fsJ的整数;节点集合记为?,称节点s,i)属

于串s;定义term为((tr)S),即串S中的第个符号项;定义uns_term(n)=((tr(s))J:,即串S的迹中的第i个符号项的无符号部分.

定义3无符号项t起源于节点,lE』 v,当且仅当sign(n)=+,且tCterm(nJ,并且对Vnj n,必须满足t簪term(J 1';无符号项t是唯一起源的,当且仅当t唯一起源于节点n.定义4设S是一个边的集合,即S一U,Ns是附带有边在S中的节点结合.定义<s为S的传递闭包,s为s的自反传递闭包,关系<s和S为NsxNs的一个子集.定义5入侵者迹描述了入侵者所具有的原子行为,入侵者迹包括如下内容:

M:Textmessage:<+t>,t~Tp F:Flusbing:<-g>

T:Tee:<-g>+g,+g>收稿日期:2009—11—22

—

50一

C:Concatenation:<-g,b,?>

S:S eparationc omponents:<一gh,g,+h>K:Key:<+KwherKekv>

E:Encryption:<-K,-h,+7h/D:Decrption:<-K-l,,一/hfb>,'Ek 1.2极小元基本定理

定理1设C是一个丛,则是一个偏序关系,具有自反性,反对称性和传递性.丛C的任何非空节点子集,在偏序关系下都有极小元.

定理2设C为丛,SC_C是节点集合且满足下述性质:m,m;usn_term(=uns_tenn(埘,,则腻s当且仅当珊,E5.若n是S的一个极小元,则n的符号为正.

2改进的Woo—Lain协议

2.1描述

M1A—}B

M2 B—A:N B

M3A—B:{NB}K^s

M4B---~S:{A,{NB}K^s}K M5S_B:{A,NR{Kas

A,B是分别是协议的发起者和响应者,S是主体可信的认证服务器;j,K醛是主体A,B分别与认证服务器S之间的共享密钥;?B是协议响应者B产生的临时值;协议的目的是响应者曰通过认证服务器S认证发起者A.2.2解析

通过协议描述可以看出Woo—Lam是有两部分组成的, (1)是发起者A与响应者B之间的通信部分,由MI,M2和M 3组成;(2)是响应者B与认证服务器S之间的通信部分,S O FrWAREDEVEL0PMENTANDDESIGN软件开发与设计

.第一部分只是起到响应者B收集发起者A由M4和M5组成

的认证信息的作用,响应者B收集到的信息可能来自合法主

体也可能来自攻击者,但是响应者B并不能根据已掌握的信息来确认发送者的合法身份.第二部分响应者B把收集到的可能来自合法主体A的信息提交给可信认证服务器s,通过与S的交互来认证发起者,所以该协议的主要认证任务在第二部分.

通过对未改进版本的Woo—Lam协议的攻击分析可知,存在3种攻击方式:(1)是攻击者冒充协议主体A,B和认证服务器s采取重放攻击;(2)是利用采取重放攻击终止协议执行;(3)是针对满足交换律的对称密码系统冒充协议主体和认证服务器5采取重放攻击.可以看出第二种攻击方式不能破坏协议的设计目标,完全可以通过软件机制来避免;在剩下的两种攻击方式中都存在攻击者冒充认证服务器s的现象,因此在改进的Woo—Lain协议的M5中通过增加主体标示符A来避免.

在改进的Woo—Lam协议的执行系统中,假设响应者B能够顺利完成一轮协议的执行,现证明响应者能否确定认证服务器s的身份,即是否存在唯一的认证服务器与响应者B对应.3协议的串空间模型

3.1代数的精确化

集合表示主体标示符集合,中的变量用A,

B等表示;表示不是主体标示符的正文消息集合,该集合中的变量用N等字符表示;K中的变量用,K:<+K>表示,映射K是单射,如XE,则函数K=K,

Kx s表示主体x与认证服务器s的共享密钥.

3.2串空间模型定义

由以上分析可知,协议的第一部分只是起到响应者B收集发起者A的认证信息的作用,协议的认证性目标的实现主要在协议的第二部分,因此在对协}义进行认证性分析时,可以忽略第一部分.

定义6设(?,P)是Woo—lain协议第二部分的一个渗透串空间,其中的串定义如下:

…1响应者串集合Re s o=Resp[A,B,s,,对应的协议主体是B,其中元素sE的迹为:<+M//f,,

{ANH}Kf2)服务器串集合Serv=-Serv[A,B,S嘲,对应的协议主体是S,其中元素sE?的迹为:<一/A//K/s,+M/K.

(31入侵者串:sEp.

4协议的认证性分析

命题1假设下列条件成立:

(1)是一个Woo—lain协议的认证部分串空间,C是中的一个丛,s是一个

Resp[A,B,S,G]中的响应者串,且C-heightfsJ=5;

(2)KK;

(3)在是唯一起源的项;

于是,C中包含唯一的服务器串Serv[A,B,S,,且C—heightfsJ=2.

在证明该命题之前先证明以下引理.任意选定一个满足命题中假设的?,C,s,A,B,%,.节点<s,1>发送f/j/K,称这个节点为n.,它的项记为Voo节点<s,2>

收到fA_?B/s,将这个节点记为n,,它的项记为v,.在证明的过程中还要用到另外两个节点13.,n:,它们满足13.<n,<n2<1"13o

引理1N起源n. .

证明由于c 『A7%//KVo,且no=<S,1>的符号为正,因此NR起源/lOo

引理2集合s={r~C:IV,Cterm(n)AVoterm(}有一个?极小元『J2,节点1"1:是正则节点且符号为正.

证明因为眯C且term(=/A%/,满足%cterm(AVOterm(nj),故njE5,因此s为非空集合.根据定理1可知,s中至少有一个极小元n2,由定理2,啦的符号为正.

现证明n不可能在入侵者串上.根据定义5知,明显玎2不能位于F,T,K,C串上,考虑剩下情况:

(1)<+其中拒因此必然有f:,%起源于此串;

由引理1?B起源于正则节点n.,再由命题1假设条件(3)%在?中唯一起源的,因此?R唯一起源于正则节点no,产生矛盾.所以112不可能位于M串上.

(2)E:<一K,,+/h/>,如果n2位于此串上,则%c {_}1}^{h}因为%?{h},所以%ch.如果noCh,则VoC{h}I与vo~{h}矛盾,如果h,那么与刀2的极小性相矛盾.因此I1.不可能位于E上.

(3)D:(-j ,,一7 h,>,这里K-,E,如果n2位于此

串上,由n2的极小元性质,%ch^_b且%c{h}^vo~{h},由vo=_/a,?B}}可知h=A{}^K-.因此Kr~kl,,与命题1假设(2)相矛盾,因此不可能位于D串上.

(4)<,>,如果n位于此串上,这里假设term(=g,另一种情况elII](=^可以类似地进行证明.因为5,故?Bcg^yogo由112的极小性有voC.根据连接加密互斥可以得?,因此voCh.通过分析得出%Cg^g,voCh.令{m~C:m?-2Acterm(m)},从定义6可以看出没有正则节点包含子项形如,因此T中每个元素都是攻击者节点.因为<p,l>eT,所以T是非空集合,由定理1可知T中存在一个极小元in,再由定理2可知m的符号为正.所以再次考虑所以入侵者串来验证这个极小元的存在性,显然T中的极小元不可能位于M,F,S,E,D,K型的串

上.考虑C:<-g,h,+g^>,若Cterm(m)此处113是一个正则节点,位于c型攻击者串P,且m是T中的极小元.因而有=fe册(m),因此re fill((p,J>)=term(n且

<p,J>n2,与112在5中的极小性相矛盾.

由以上分析可得n.不可能位于攻击者串上,因此n.必然在一个正则串上,引理得证.

引理3存在一个串t上的节点n2的前驱节点nJ,且term tn:{A{NBtKtK.

证明由引理1知?日起源于nO,且由命题1假设(3)知一

51—

电脑编程技巧与维护

?R在中是唯一起源的.因为voCterm(no)且Voterm(J】 2),所以n2#no且%不起源于n2.从而在串t上存在一个n2的先驱节点11.,使得%cte rm(n.由n2的极小性,Vo=/A,%//cterm(n.从定义1中项的形式可以看出只可能

/K~term(n,引理得证.

引理4包含n和n2的正则串t是一个丛C中的服务器串.

证明节点n是一个符号为正的正则节点,且它的前驱节点u,具有形式{x{M}}},其中,KE,X,

YE.如果t是一个响应者串,则在形如{X{M}}斯}的项之后,只能是一个符号为负的节点.因此t是一个服务器串.从而和11:分别是t上的第1个和第2个节点.由于t的最后一个节点包含在丛c中,故有C-height(0=2.引理5丛存在唯一的服务器串t.

证明由命题1假设条件(3)知%隹ke,并且K是主体B与可信认证服务器S之间的长期共享密钥,由与映射艮_+k是单射,即如果一,则函数K):且函数Kl(J=K船为单射,因此密钥K鹅是可信认证服务器5与唯一主体B之间的共享密钥.由{A%}cte rm(<s,2>)可知

{A}KRs来自唯一的服务器串t~S erv[A,B,S,?.

由引理1—5,命题1得证.

5结语

根据命题l的证明可以看出改进后的Woo—Lam协议满足

响应者单向认证发起者的设计目标,与基于认证测试方法的证明结果[31相同.通过证明过程还可以得出以下结论:无论证明过程基于极小元理论还是基于认证测试理论,都是以协议主体与认证服务器之间的长期共享密钥,K岱隹为前提.

参考文献

【1】 FdbregaFJT,Herz ogJC,GuttmanJ D.S trandspac e s:Whyis

asecurityprotocolcorrect? 【C】 //Proceedingofthe1998

IEEESymposiumonS ecurityandPrivacy.LosAlamitos:

IEEEComputerPress,1998:160—171.

【2】 F6bregaFJT,Herzogj c,GuttmanJD.Strandspaces:Provingsecurityprotocolscorrect[J】 .JournalofComputerSecurit

1999,7(2-3):191-230.

[3]李廷元,秦志光,刘晓东,张选芳.基于认证测试方法的Woo—Lam协议的分析及改进[J].计算机科学,2009,36(4B):206-218.

[4]卿斯汉.安全协议【M】 .北京:清华大学出版社,2005:98一】 00.

作者简介

余磊,男(1978一),硕士研究生,研究方向:信息安全.

顾维娜,女,硕士研究生,研究方向:信息安全.

王猛,男,硕士研究生,研究方向:信息安全.

(上接第49页)

束排列( 【23],4)的最大排列,飓=9一(2+3)=4.再看右边数

起的后三位322.由于max([423】 ,7)=421,所以322不是约束排列( 【423】 ,7)的最大排列,其中M2=9—2=7.于是将第二位上的3改为4,后两位取mi n( 【23】 ,3)=03,其中M'3=9一(2+4)=3.输出的下一个排列是2403,它正是第8号排列.

3算法优化

此问题的核心是查找自右向左的序列中的位,第一个不是约束排列( 【.‰,…^,)的最大排列的位.而在实际代码编写过程中,对于k的锁定,可以通过用已知序列ala:…am与约束排列位的上限M. .…逐一对应相减比较得到,即【r.,r2….rm】 =[,,…?川】一【ala:…aj .其中?0,(r=l,2….埘).直接找到从倒数第二位起,向左的第一

个非零的位置S即可.

4代码实现a=z e ro s(1,4);limit= 【3423】 ;

Const=9;

Boundary=a:

X=inpu t(输入当前排列:);

%一一一spotforJ=length(x):一1:2

Boundary(j)=sum(x(1:(j—1)));end

Boundary(1)=0;

BoundaryConst—Boundary;

T_line=limit—x:spot=length(T_line);fori=(1 ength(r_line)-1):-l:l

一

52一ifT_line(i),=0spot:i;break;endend

%===一=一x+1x(spot)=x(spot)+l;

T_left=Boundary(spot+1)一1;

T_vector=x((spot+1):length(a));T_Vector=zeros(1,length(T—Vector));