On the logical verification of a group key agreement protocol for resource constrained mobile devices

Due to the rapid growth of mobile networks, many advanced applications have been deployed. However, security of data will be an important factor for their full adoption. Most of these applications will be utilized on resource constrained devices, which makes security protocols currently used in wired networks not fully applicable to mobile networks. Recently, a number of key agreement protocols have been proposed for use with wireless networks involving resource-limited devices. These include the DDH-based group key agreement protocol [1], the protocol proposed by Bresson et al. [2] and Tsengpsilas protocol [3]. In order to provide assurance that these protocols are verifiably secure and trustworthy it is necessary to perform a formal verification on their design specifications. In this paper Tsengpsilas protocol is discussed and a formal verification is performed using the Coffey-Saidha-Newe (CSN) modal logic[4]. As a result of this verification some potential problems with the protocol are presented.