ARP协议的描述与TLA验证

The Description and Validation of ARP Protocol Based on TLA

随着计算机网络的发展,网络的安全性日益受到人们的关注。ARP攻击是一种非常专业化的网络攻击方式,它会给网络管理员增加很大的负担,破坏主机数据,窃取主机信息。Lesilie Lamport提出了一种新的逻辑,即行为时序逻辑(TLA)理论体系,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达程序与属性。文中介绍了ARP协议,用基于行为时序逻辑TLA的建模语言TLA+对ARP协议进行建模分析。构造了一个ARP欺骗的攻击者模型,用基于TLA的模型检测工具TLC对其进行验证并找出一条攻击者路径。

With the development of computer network,more and more people are paying attention to the security of network.The ARP attacking is a very special mode of network attacking,it will destroy the data of host computer.In recent years,a foreign researcher,Lesilie Lamport,puts forward a new logic： temporal logic of actions（TLA）,modeling the concurrent system to put to use this logic can relieve the pressure caused by the state space exposion to some extent,it can express process and attributes in a language at the same time.Introduce ARP protocol.Specify the ARP protocol with TLA＋ based on the temporal logic of actions and validate it with TLC and find a path of attacker.