A Model for Specification and Validation of a Trust Management based Security Scheme in a MANET Environment

Recently, we proposed a reputation based trust management scheme built upon a Mobility-based Clustering Approach (MCA) organizing Mobile Ad hoc NETwork MANET and detecting and isolating malicious behaviors. The whole scheme was called TMCA (Trust based MCA) and was extended in a second time with a delegation process resulting a proposition baptized DTMCA (Delegation TMCA based process). However, deploying such scheme is error prone and it appears necessary to validate it before its real implementation. In fact, scheme specification and validation constitute two fundamental challenges in the development of secure communication systems ensuring that the scheme is correctly enforced and complete. Hence, the main contribution of this paper concerns a validation framework for DTMCA scheme. The first step towards validation process is its formal specification. This is our first concern in this paper: a formal specification language called SCMSL (Secured Clustered MANET Specification Language) defined through a syntax based on authorization and obligation rules and a clear semantics. The second part of this paper proves the two major characteristics that must be guaranteed in such case: consistency and completeness. Consistency is proved by showing that there is no conflict in our scheme whereas completeness is proved by assessing that all potential situations are handled. The proof of consistency and completeness is made using automated systems through the definition of adequate algorithms.