Designing and verifying a P2P service security protocol in M2M environment

Multifunctional high-performance electronic systems in M2M(Machine-to-Machine) industry have been evolving substantially in tandem with the advancement of IT. M2M, standing for machine-to-machine communication, replaces people in cases where human intervention is hardly viable or in such fields as weather, environment or disasters where long-term monitoring is required. Yet, due to the nature of M2M devices involving wireless communication, they are exposed to intruders’ attacks. Thus, the overriding concern in M2M communication is mutual authentication and security. In this context, security communication protocols are considered worth exploring. This paper concerns designing a safe communication protocol by applying hash locks, random numbers and session keys. Instead of arguing for the security of the protocol based on mathematical theorem proving as most previous studies did, the present paper demonstrates the proposed protocol is safe against a variety of intruders’ attacks by formally verifying it using Casper/FDR. In short, the proposed protocol is verified in terms of safety, deadlock and livelock.