Internet of Things (IoT) devices have restricted resources and energy; however, they require regular updates and identification from other devices and the backend server. Thus, security is also a major concern, and the most common way to do it is mutual authentication between the communicating parties. Provable security aims to provide concrete mathematical proof for ensuring the protocol’s security. Modern cryptographic protocols deploy “game-based” security models, which have an adversary that can carry out potential attacks over the concerned system. The adversary in the universally composable security model interacts with both real-world and ideal-world environments. The adversary can eavesdrop into all the communications and can schedule the activation sequence of the entities. The real spreading of IoT services requires customized security and privacy levels to be guaranteed. K. Ouafi et al. have extended Vaudeney’s model to incorporate the notion of strong privacy.