计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2002年
17期
125-128
,共4页
BAN逻辑 模型检查 NRL FDR SMV 定理证明
BAN邏輯 模型檢查 NRL FDR SMV 定理證明
BAN라집 모형검사 NRL FDR SMV 정리증명
该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型.利用该计算模型对Denning-Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改.
該文採用近世代數和時序邏輯的方法提齣併描述瞭密碼協議的形式化安全需求,併在AT模型的基礎上加入信任和知識的非單調邏輯,建立瞭安全協議的計算模型.利用該計算模型對Denning-Sacco公鑰協議進行瞭驗證,髮現瞭對此協議的重放攻擊,併對協議進行瞭脩改.
해문채용근세대수화시서라집적방법제출병묘술료밀마협의적형식화안전수구,병재AT모형적기출상가입신임화지식적비단조라집,건립료안전협의적계산모형.이용해계산모형대Denning-Sacco공약협의진행료험증,발현료대차협의적중방공격,병대협의진행료수개.
