中国科学E辑
中國科學E輯
중국과학E집
SCIENCE IN CHINA (SERIES E)
2005年
4期
337-351
,共15页
形式化验证%安全协议%认知逻辑%知识结构
形式化驗證%安全協議%認知邏輯%知識結構
형식화험증%안전협의%인지라집%지식결구
认知逻辑的Kripke语义,已被成功地运用到分析无黑客存在的安全网络下的通信协议.提出认知逻辑的Kripke语义的一种简单而自然的形式,称之为知识结构,并把这种语义用到分析黑客存在的非安全网络环境中的通信协议,特别是认证协议.与类BAN的那一类逻辑相比,文中的方法可以直接转化成算法实现,对协议本身进行操作,而不需对协议进行一些难以把握的抽象判断.而且,在这套理论的基础上开发了安全协议分析器SPV.文中的方法是基于证明的而不是证伪的,即证明协议的正确性而不是找协议漏洞.
認知邏輯的Kripke語義,已被成功地運用到分析無黑客存在的安全網絡下的通信協議.提齣認知邏輯的Kripke語義的一種簡單而自然的形式,稱之為知識結構,併把這種語義用到分析黑客存在的非安全網絡環境中的通信協議,特彆是認證協議.與類BAN的那一類邏輯相比,文中的方法可以直接轉化成算法實現,對協議本身進行操作,而不需對協議進行一些難以把握的抽象判斷.而且,在這套理論的基礎上開髮瞭安全協議分析器SPV.文中的方法是基于證明的而不是證偽的,即證明協議的正確性而不是找協議漏洞.
인지라집적Kripke어의,이피성공지운용도분석무흑객존재적안전망락하적통신협의.제출인지라집적Kripke어의적일충간단이자연적형식,칭지위지식결구,병파저충어의용도분석흑객존재적비안전망락배경중적통신협의,특별시인증협의.여류BAN적나일류라집상비,문중적방법가이직접전화성산법실현,대협의본신진행조작,이불수대협의진행일사난이파악적추상판단.이차,재저투이론적기출상개발료안전협의분석기SPV.문중적방법시기우증명적이불시증위적,즉증명협의적정학성이불시조협의루동.
