Modeling and Formal Verification of DHCP Using SPIN

The Dynamic Host Configuration Protocol (DHCP) is a widely used communication protocol. In this paper, a portion of the protocol is chosen for modeling and verification, namely the assignment of new IP address to a newly arriving host. PROcess Meta LAnguage (PROMELA) is used for modeling and the verification is performed using SPIN. SPIN can verify most of the communication protocols either by performing random simulations or by generating a C program. It can perform an exhaustive verification that can establish with mathematical certainty whether or not a given behavior is error-free. PROMELA is used to specify a system behavior in a formal validation model that defines interactions of processes in a distributed system and allows for the dynamic creation of concurrent processes. We have analyzed and verified various properties of the DHCP protocol such as absence of deadlock, livelock, and improper termination under various conditions such as message loss or arbitrary errors. We obta...

• Type: Journal
• Year: 2006
• Where: IJCSA
• Authors: Syed M. S. Islam, Mohammed H. Sqalli, Sohel Khan
• Keywords: Communication Protocols, Dynamic Host Configuration Protocol, IJCSA 2006, IP Address