A formal verification of ARPON - a tool for avoiding Man-in-the-Middle attacks in Ethernet networks

Since the nineties, the Man-in-The-Middle (MITM) attack has been one of the most effective strategies adopted for compromising information security in network environments. In this paper, we focus our attention on ARP cache poisoning, which is one of the most well-known and more adopted techniques for performing MITM attacks in Ethernet local area networks. More precisely, we will prove that, in network environments with at least one malicious host in the absence of cryptography, an ARP cache poisoning attack cannot be avoided. Subsequently, we advance ArpON, an efficient and effective solution to counteract ARP cache poisoning, and we use a model-checker for verifying its safety property. Our main finding, in accordance with the above impossibility result, is that the only event that compromises the safety of ArpON is a cache poisoning that nevertheless is removed by ArpON itself after a very short period, thus making it practically infeasible to perpetrate an ARP cache poisoning attack on network hosts where ArpON is installed.