Abstract
For efficient network applications, it's necessary to build security mechanisms for a secure communication. End-to-end security plays a crucial role for the communication in the network, to provide the confidentiality, the authentication and mostly the prevention from DOS attacks at high level. The main downside of the key generation and key exchange are that, the attackers might access the transmitted data and use it to obtain the key and even generate new keys. Also, the process of generating the key is inefficient and time consuming. This paper, propose a fast and secure key exchange protocol in the TVWS. In order to check these security properties, this paper used a formal verification tools called A VISPA.