Authenticated key agreement in wireless networks with automated key management

Authenticated key agreement protocols provide wireless technologies with fundamental mechanisms such as session key generation and device authentication. Many of these protocols have been designed specifically for those technologies, but most of them do not integrate all the security requirements, and others have been attacked. Another important issue that arises in practice is related to key management, since the deployement and replacement of keying material is costly and may potentially lead to security vulnerabilities. For these reasons, we propose a generic authenticated key agreement protocol in which the long term secret is automatically and periodically renewed. The focus of this work is to formally assess the security offered by the protocol's key renewing in the case of a long term use of the system. The formal analysis is carried using the automated tools ProVerif and AVISPA. The protocol is designed to rely only on symmetric key algorithms and is suitable for devices that have limited hardware capabilities.