Smart cities optimize traffic management and vehicle communication through Intelligent Transportation Systems (ITS), with Vehicular Ad-hoc Networks (VANET) serving as a core infrastructure. In these environments, security vulnerabilities can severely impact the smart city traffic system, leading to traffic congestion, blockage of emergency vehicle routes, and disruption of autonomous driving systems. Unfortunately, identifying security vulnerabilities of the system in VANET is complex due to various attack types and the dynamic nature of the network, requiring systematic verification techniques for effective analysis. Recently, Nath et al. proposed an authentication protocol for VANETs using LWE-based lattice signatures and tokens, however the protocol has not been sufficiently validated. This study utilizes AVISPA (Automated Validation of Internet Security Protocols and Applications) to analyze Nath et al.’s protocol. AVISPA, an automated security verification tool based on the Dolev-Yao(DY) attacker model, is effective in assessing various threats such as replay attacks and man-in-the-middle attacks, making it ideal for evaluating security in the VANET environment. The security analysis reveals that the protocol is vulnerable to multiple attacks due to the lack of message freshness verification and user authentication. To address these vulnerabilities, we propose countermeasures to enhance message freshness verification and user authentication mechanisms, and validate the improved protocol’s security through AVISPA simulation. Finally, we verify the security of the authentication scheme which is applied the countermeasures through AVISPA. The result shows that the security of smart city vehicular networks can be strengthened through AVISPA-based security verification and this can provide valuable insights for designing security protocols in smart cities.