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.

A formal verification of ARPON - a tool for avoiding Man-in-the-Middle attacks in Ethernet networks / D. Bruschi, A. Di Pasquale, S. Ghilardi, A. Lanzi, E. Pagani. - In: IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING. - ISSN 1545-5971. - (2021). [Epub ahead of print] [10.1109/TDSC.2021.3118448]

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

D. Bruschi
Primo
;
S. Ghilardi;A. Lanzi
Penultimo
;
E. Pagani
Ultimo
2021

Abstract

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.
ARP; formal verification; Internet; Local area networks; Man-in-the-Middle attacks; Network protocols; Payloads; Protocols; Safety; secure ARP; Task analysis; Tools
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
7-ott-2021
Article (author)
File in questo prodotto:
File Dimensione Formato  
TDSC2021.pdf

accesso aperto

Descrizione: articolo principale
Tipologia: Publisher's version/PDF
Dimensione 1.39 MB
Formato Adobe PDF
1.39 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/903256
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact