资源描述:
《不可否认协议分析的增广csp方法》由会员上传分享,免费在线阅读,更多相关内容在教育资源-天天文库。
1、第10期韩志耕等:不可否认协议分析的增广CSP方法·17·不可否认协议分析的增广CSP方法韩志耕,罗军舟,王良民(东南大学计算机科学与工程学院,江苏南京210096)摘要:提出一种适用于不可否认协议分析的增广CSP(communicatingsequentialprocesses)方法。检验有效性时使用它分析了Zhou等人于1996年提出的公平不可否认协议及其变体的安全性。结果表明该方法不仅能分析一些其他方法无法描述的协议性质,而且还发现了该协议的一个许多其他方法不能发现的已知缺陷;同时还证明协议变体增强了安
2、全性。最后从语义和理论依赖2个角度讨论了方法正确性,并给出与其他方法相比所具备的优势。关键词:不可否认;增广CSP方法;公平性;时限性;形式化方法中图分类号:TP393文献标识码:A文章编号:1000-436X(2008)10-0008-11Extended-CSPbasedanalysisofnon-repudiationprotocolsHANZhi-geng,LUOJun-zhou,WANGLiang-min(SchoolofComputerScienceandEngineering,Southeast
3、University,Nanjing210096,China)Abstract:Anewformalmethodnamedextended-CSPapproachwasproposedfornon-repudiationprotocols.Forcheckingitsvalidity,boththewell-knownZhou-Gollmannfairnon-repudiationprotocolpresentedbyZhouetal.in1996andoneofitsvariantprotocolwerea
4、nalyzedwiththismethod.Theresultshowedthatthismethodnotonlycouldbeusedtoanalyzesomesecuritypropertiesthatcouldnotbedescribedbyothermethods,butalsodetectedaknownflawoftheprotocolwhichcouldnotbefoundbyothers,andmeanwhileprovedthevariantprotocolreallyenhancingi
5、tssecurity.Finally,thecorrectnessofthismethodwassurveyedfromthepointsofbothitssemanticandtheorydependency,andsomeadvantagesincomparisonwithotherswerealsoshowedtogether.Keywords:non-repudiation;extended-CSPapproach;fairness;timeliness;formalmethod第10期韩志耕等:不可
6、否认协议分析的增广CSP方法·17·1引言收稿日期:2008-06-21;修回日期:2008-09-20基金项目:国家自然科学基金资助项目(90604004,60703115);江苏省自然科学基金资助项目(BK2007708,BK2008030);江苏省“网络与信息安全”重点实验室基金资助项目(BM2003201);科技部国际科技合作项目FoundationItems:TheNationalNaturalScienceFoundationofChina(90604004,60703115);TheNatura
7、lScienceFoundationofJiangsuProvince(BK2007708,BK2008030);TheKeyLaboratoryofNetworkandInformationSecurityofJiangsuProvince(BM2003201);InternationalScienceandTechnologyCooperationProgramofChina第10期韩志耕等:不可否认协议分析的增广CSP方法·17·新技术的不断发展,网络系统愈加复杂异构,网络异常及攻击行为日益多样化,服务
8、质量的需求不断演化,这一切使得构建可信可控的网络体系来保障网络的安全性、可信性及可扩展性具有重要的意义。纵观现存的网络体系结构要么是基于边缘论和面向非连接的设计思想,使得分组传输路径不可控,要么是重新设计现有网络的体系结构,代价巨大。认为新体系结构可在不破坏网络现有架构的基础上通过增加一个可信可控的4层逻辑结构来构建,以此确保网络组元及用户行为的可预期、可管理。不可否认服务作为保障该架构正确实施的关