停等式ARQ协议的SPIN模型检测
|
摘要
介绍停等式ARQ协议的工作原理,并使用Promela对其进行建模,利用SPIN对所建模型进行检测,证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法,使用Promela语言对攻击者进行建模,并利用SPIN的图形界面工具XSPIN模拟了攻击过程,验证了攻击的有效性。
The working principle of the stop-and-wait ARQ was introduced,whose model was established by using the Promela language. The established model was proved,through model testing conducted with SPIN,to have the nature of the stop-and-wait ARQ. Then the method of attacking the ARQ protocol was discussed,and the attacker was modeled by using the Promela language. The attack process was simulated by using SPIN's graphical interface tool XSPIN,which proved the effectiveness of the attack.
The working principle of the stop-and-wait ARQ was introduced,whose model was established by using the Promela language. The established model was proved,through model testing conducted with SPIN,to have the nature of the stop-and-wait ARQ. Then the method of attacking the ARQ protocol was discussed,and the attacker was modeled by using the Promela language. The attack process was simulated by using SPIN's graphical interface tool XSPIN,which proved the effectiveness of the attack.
引文
[1]李新宇.用于通信网络协议开发的形式化方法[J].中国新通信,2014(15):100-101.
[2]LU D L,CHANG J F.Performance of ARQ protocols in nonindependent channel errors[J].IEEE Trans Commun,1993,41(5):721-730.
[3]徐佑军,谭敦茂,朱建武,等.蓝牙无线链路质量的分析、测试与改善[J].计算机工程与应用,2004,40(12):129-131,211.
[4]HOLZMANN G J.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.
[5]陈义,唐郑熠.通信协议的Promela语言建模与检测[J].福建电脑,2016,32(3):39-40.
[6]徐永生.带参性质的形式化描述与证明[D].成都:电子科技大学,2015.
[7]吴勇,李祥.基于TLA的ARQ协议描述与验证[J].计算机安全,2012(8):40-43.
[2]LU D L,CHANG J F.Performance of ARQ protocols in nonindependent channel errors[J].IEEE Trans Commun,1993,41(5):721-730.
[3]徐佑军,谭敦茂,朱建武,等.蓝牙无线链路质量的分析、测试与改善[J].计算机工程与应用,2004,40(12):129-131,211.
[4]HOLZMANN G J.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.
[5]陈义,唐郑熠.通信协议的Promela语言建模与检测[J].福建电脑,2016,32(3):39-40.
[6]徐永生.带参性质的形式化描述与证明[D].成都:电子科技大学,2015.
[7]吴勇,李祥.基于TLA的ARQ协议描述与验证[J].计算机安全,2012(8):40-43.