搜索
276200611MICROCOMPUIERAPPLICATIONSVol.27No.6Nov.20062004-11-24:(410076):,,,,,,:Cross-Tree:ADateStructureforAnalysisofSecurityProtocolsLUOYingying(ComputerSchool,ChangshaUniversityofScience&Technology,Changsha,410076,China)Abstract:Thisarticleproposesadatastructrrecalledcross2tree.whichisaspecialtreewithsomenodescrossedtorepresentmessagesinsecurityprotocols.Severalcross2treescanconstituteacross2forestwhentheyhavecrossedmodes.Across2treecorrespondsuniquelywithamessage,andacross2forestrepresentsthosemessagesthataresentorreceivedbythesameprinci2palinaprotocolexecution.Thesameatomicmessagesinonemessageorseveralmessagesarerepresentedsathecrossednodesinacross2treeoracross2forest;henceitiseasytoguaranteetheconsistencyoftheatomicmessagesandtheconsistencyofthepublickeysanditsowners.iInaddition,across2treecanbeusedtoconstructacceptablemessagesforamessagetemplate,whichismecessaryfortheanalysisofsecurityprotocolsbasedonmodelchecking.Keywords:securityprotocols,protocolrepresentation,cross2tree;cross2froest,formalmethods1,[1],,Needham2Schr2oederIKE[2],BANNRLStubblebine2Gligor[3],,,,[4],,,,21,1,,1:,TVValue6::T=0,V=0,V=1,Value2:,1,T=13:,TName2PointerT=2,Name2Pointer4:,TDegP1P2PnT=3,Degm,P1Pnm5:,TKey2PointerEncrypted2Msg2PointerT=4,Key2Pointer,Encrypted2Msg2Pointerm,CT(m)=(N(m),E(m)),N(m),E(m),,mn,n,33.1,mCT(m)1:generate(m)(1)ifmNAMEthen//n=search(NAME,m);//ifn=NULLthen//n=create(NAME);//n.T=0;n.Value=m;ifmisavariablethenn.V=1;elsen.V=0;returnn;(2)ifmNONCEthen//n=search(NONCE,m);ifn=NULLthenn=create(NONCE);n.T=1;n.Value=m;ifmisavariablethenn.V=1;elsen.V=0;returnn;(3)ifmKEYthen//n=search(KEY,m);ifn=NULLthenn=create(KEY);n.T=2;n.Name-Pointer=generate(owner(m));returnn;(4)ifmENCRYPTIONthen//n=create(ENCRYPTION);n.T=4;n.KEY-Pointer=generate(k);n.Encrypted-Msg-Pointer=generate(m();returnn;(5)ifmCOMPOSITIONthen//n=create(COMPOSITION);n.T=3;n.Deg=degree(m);fori=0todegree(m)-1don.Pi=generate(sequence(m,i));returnn;,,,,,,3.2,,n,n.V=1,n;n,n1n2,n1n2,n2n1,n1n2[5],,[6]n1n2:(1)n1n1.V=0,n2,n2.V=0,n1.Value=n2.Value;n1.V=1,n2(2)n1n1.V=0,n2,n2.V1662006=0,n1.Value=n2.Value;n1.V=1,n2(3)n1,n2,n2.Name-Pointern1.Name-Pointer,n1n2(4)n1,n2,n2.Keyn1.Key,n2.Encrypted-Msg-Pointern1.En2crypted-Msg-Pointer(5)n1,n2,n1.Deg=n2.Deg,n2.Pin1.Pim1m2,root(CT(m1))root(CT(m2)),CT(m1)CT(m2)m1,m2m1,m,CT(m),2:generate_compatible_class(n)(1)C=;S=leaf(CT(message(n)));foreachnSdoifn.V=0thenremove(n.CT(message(n)));//nS=leaf(CT(message(n)));foreachmSdoifparent(m)=ENCRYPTIONthenremove(patent(m),CT(message(n)));elseifparent(m)=;thenC=C{parent(m)};(2)S=C;//S=S;while(S=)//SS{S=;foreachCSdoifchild(c)thenC=C-{c}child(c);S=S{C};S=S;S=SS;}returnS;,,,,,,,,,3:generate_acceptable_msgs(n)R=;S=generate_compatible_class(n);foreachCSdo//Cm=|C|;fori=0tom-1doSi=matched_node(C(i));//C(i)Cin=duplicate(n);S=S0S1Sn;foreachCSdon=substitute(n,C,C);//CnCnR=R{n};returnR;matched_node,,,4,,,,,,1,.-.:,1999.3743882..,2004,30(12):1291313,,..:,2002,2102124..:,1998,40435.IPsecNAT.,2003,29(4):2532556..(1969),,,266