计算机技术与发展
計算機技術與髮展
계산궤기술여발전
COMPUTER TECHNOLOGY AND DEVELOPMENT
2012年
10期
177-180
,共4页
连续ARQ协议%洪水攻击%模型检测%SPIN%Promela
連續ARQ協議%洪水攻擊%模型檢測%SPIN%Promela
련속ARQ협의%홍수공격%모형검측%SPIN%Promela
通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性.模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证.文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性.然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储.这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性.
通信協議設計時的疏漏很容易造成嚴重的後果,因此有必要採用形式化的方法來保證協議的安全性和可靠性.模型檢測是一種具有工業應用前景的形式化分析方法,併具有很高的自動化程度,適閤于協議的分析與驗證.文中採用模型檢測工具SPIN對連續ARQ協議建模,通過驗證該協議的基本屬性證明所建模型的正確性.然後依據Dolev和Yao的思想加入攻擊者模型再進行分析,髮現瞭連續ARQ協議的一箇新漏洞,攻擊者能夠利用這箇漏洞造成大量冗餘數據的傳輸和存儲.這種攻擊建立在互信的數據傳輸基礎上,且攻擊者併不直接髮送冗餘數據,因此具有很高的隱蔽性.
통신협의설계시적소루흔용역조성엄중적후과,인차유필요채용형식화적방법래보증협의적안전성화가고성.모형검측시일충구유공업응용전경적형식화분석방법,병구유흔고적자동화정도,괄합우협의적분석여험증.문중채용모형검측공구SPIN대련속ARQ협의건모,통과험증해협의적기본속성증명소건모형적정학성.연후의거Dolev화Yao적사상가입공격자모형재진행분석,발현료련속ARQ협의적일개신루동,공격자능구이용저개루동조성대량용여수거적전수화존저.저충공격건립재호신적수거전수기출상,차공격자병불직접발송용여수거,인차구유흔고적은폐성.
