基于SAT的安全協(xié)議自動(dòng)化檢測(cè)技術(shù)研究.pdf

1、安全協(xié)議是以密碼學(xué)為基礎(chǔ),在通信網(wǎng)絡(luò)和分布式系統(tǒng)中提供各種安全服務(wù)的一種協(xié)議,在信息系統(tǒng)安全中占據(jù)重要的位置。然而對(duì)安全協(xié)議進(jìn)行分析和驗(yàn)證是一項(xiàng)非常有挑戰(zhàn)的工作,成為安全協(xié)議發(fā)展與應(yīng)用的瓶頸。由于安全協(xié)議的發(fā)展已經(jīng)超出了人們進(jìn)行嚴(yán)格分析和驗(yàn)證的能力,因此有必要對(duì)安全協(xié)議自動(dòng)化檢測(cè)技術(shù)進(jìn)行研究。
　　 本文研究了基于SAT(Satisfaction)的安全協(xié)議自動(dòng)化檢測(cè)的關(guān)鍵技術(shù),并指出現(xiàn)有檢測(cè)工具在檢測(cè)協(xié)議類(lèi)型上的局限性,然后針

2、對(duì)該問(wèn)題,對(duì)檢測(cè)協(xié)議類(lèi)型進(jìn)行擴(kuò)展,提出了無(wú)類(lèi)型消息和多協(xié)議中的候選輔助協(xié)議的概念,設(shè)計(jì)并實(shí)現(xiàn)了基于SAT的安全協(xié)議自動(dòng)化檢測(cè)系統(tǒng)SAT-ADS(Automatic Detection System ofSecurity Protocols Based SAT),使SAT-ADS可以檢測(cè)類(lèi)型缺陷攻擊和多協(xié)議攻擊,并經(jīng)過(guò)實(shí)例驗(yàn)證檢測(cè)的可行性。
　　 最后,應(yīng)用SAT-ADS檢測(cè)系統(tǒng)對(duì)BAN modified Andrew Secur