Biblio
We conduct formal verification of the divide and conquer key distribution scheme (DC DHKE)-a contributory group key agreement that uses a quasilinear amount of exponentiations with respect to the number of communicating parties. The verification is conducted using both ProVerif and TLA+ as tools. ProVerif is used to verify the protocol correctness as well as its security against passive attacker; while TLA+ is utilized to verify whether all participants in the protocol retrieve the mutual key simultaneously. We also verify the ING and GDH.3 protocol for comparative purposes. The verification results show that the ING, GDH.3, and DC DHKE protocols satisfy the pre-meditated correctness, security, and liveness properties. However, the GDH.3 protocol does not satisfy the liveness property stating that all participants obtain the mutual key at the same time.
Mobile Ad-hoc Network (MANET) is an autonomous collection of mobile nodes and communicate among them in their radio range. It is an infrastructure less, bandwidth constraint multi-hop wireless network. A various routing protocol is being evolved for MANET routing and also provide security mechanism to avoid security threads. Dynamic Source Routing (DSR), one of the popular reactive routing protocols for MANET, establishes path between source to destination before data communication take place using route request (RREQ) and route reply (RREP) control messages. Although in [1] authors propose to prevent route diversion due to a malicious node in the network using group Diffie-Hellman (GDH) key management applied over source address, but if any intermediate trusted node start to misbehave then there is no prevention mechanism. Here in this paper, we applied Hash function scheme over destination address to identify the misbehaving intermediate node that can provide wrong destination address. The path information towards the destination sent by the intermediate node through RREP is exactly for the intended required destination or not, here we can identified according to our proposed algorithm and pretend for further data transmission. Our proposed algorithm proves the authenticity of the destination and also prevent from misbehaving intermediate nodes.