计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2015年
1期
149-154,169
,共7页
安全协议%形式化分析%串空间%认证测试
安全協議%形式化分析%串空間%認證測試
안전협의%형식화분석%천공간%인증측시
Security protocol%Formal analysis method%Strand space%Authentication test
认证测试是一种新型的在串空间模型基础上提出来的用于分析协议认证属性的形式化方法,该方法因简单实用而受到学者的广泛关注,但其不能分析协议中认证测试组件嵌套加密的情况,这极大地限制了它的应用范围.而现存的针对该局限性的改进方案,由于没有从本质上对串空间模型中关于消息项结构关系方面的语义进行完善,很难彻底突破认证测试的局限性.为此,通过在串空间模型中引入等价类、类组件、安全加密元及安全包裹元等概念,提高了串空间刻画消息项之间及内部结构关系的能力,并结合实例来阐明引入这些概念的必要性.在此基础上,提出一种可以分析测试组件嵌套加密的通用的认证测试方法,并从形式化证明与实例分析两方面验证了新测试方法的正确性与有效性.
認證測試是一種新型的在串空間模型基礎上提齣來的用于分析協議認證屬性的形式化方法,該方法因簡單實用而受到學者的廣汎關註,但其不能分析協議中認證測試組件嵌套加密的情況,這極大地限製瞭它的應用範圍.而現存的針對該跼限性的改進方案,由于沒有從本質上對串空間模型中關于消息項結構關繫方麵的語義進行完善,很難徹底突破認證測試的跼限性.為此,通過在串空間模型中引入等價類、類組件、安全加密元及安全包裹元等概唸,提高瞭串空間刻畫消息項之間及內部結構關繫的能力,併結閤實例來闡明引入這些概唸的必要性.在此基礎上,提齣一種可以分析測試組件嵌套加密的通用的認證測試方法,併從形式化證明與實例分析兩方麵驗證瞭新測試方法的正確性與有效性.
인증측시시일충신형적재천공간모형기출상제출래적용우분석협의인증속성적형식화방법,해방법인간단실용이수도학자적엄범관주,단기불능분석협의중인증측시조건감투가밀적정황,저겁대지한제료타적응용범위.이현존적침대해국한성적개진방안,유우몰유종본질상대천공간모형중관우소식항결구관계방면적어의진행완선,흔난철저돌파인증측시적국한성.위차,통과재천공간모형중인입등개류、류조건、안전가밀원급안전포과원등개념,제고료천공간각화소식항지간급내부결구관계적능력,병결합실례래천명인입저사개념적필요성.재차기출상,제출일충가이분석측시조건감투가밀적통용적인증측시방법,병종형식화증명여실례분석량방면험증료신측시방법적정학성여유효성.
