A formal environment for MANET organization and security

Abstract

A Mobile Ad-hoc Network (MANET) allows the communication of autonomous nodes without any preexistent network infrastructure. This main characteristic may introduce several vulnerabilities which can be exploited by malicious nodes. Thus, one of the basic requirements for the well behavior of such network is to detect and isolate such nodes. Recently, we proposed a reputation based trust management scheme detecting and isolating malicious nodes. This scheme was built upon a specific clustering algorithm baptized MCA (Mobility-based Clustering Approach) and based on two phases: the setting up and the maintenance. In the setting up phase, stable clusters are generated with one-hop members and elected cluster-heads (CHs). In the maintenance phase, the organization of the clusters is maintained in presence of mobility using adequate algorithms. The whole proposition was called TMCA (Trust based MCA) and was also extended with a delegation process resulting a proposition baptized DTMCA (Delegation process TMCA). Once DTMCA is defined, we have found important to validate formally each one of its components in order to avoid any conflict, lack or misbehaving situations. This process requires in a first step a formal specification. This is our main concern in this paper where we propose in a first part a formal specification using inference systems based on logical rules. Two inference systems are proposed. The first one handles the MCA maintenance phase and the second one specifies the TMCA scheme on which the delegation process is integrated. A formal validation using these inference systems is proposed in a second step in order to prove the soundness and the completeness of the various propositions.