The Description and Validation of ARP Protocol Based on TLA
Li Xiang · Computer Technology and Development · 2010
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.