Formal Analysis of MPKE Protocol in Wireless Mesh Network Using ProVerif

The MPKE protocol on Wireless Mesh Network (WMN) is a multi-party protocol that uses tickets in the authentication process. The MPKE protocol was created by Roy et al. in 2022 and is intended for the authentication process at the time of handover from the Home Mesh Access Point (HMAP) to the Foreign Mesh Access Point (FMAP). This protocol was claimed by Roy et al. to fulfill the aspects of confidentiality and mutual authentication. This statement is described informally, so security claims cannot be formally confirmed. A formal analysis is needed to be able to objectively verify the claims based on automated analysis tools. In addition to verifying security claims, formal analysis can also be used to prove vulnerabilities in the protocol. In this research, ProVerif was used, which is a formal analysis tool with a symbolic method to prove claims. ProVerif could model Roy et al.'s MPKE protocol well with the security claim of mutual authentication aspect fulfilled, but the security claim of message confidentiality was not fulfilled. This caused the possibility of attacks, namely man-in the-middle-attack, impersonation attack and replay attack. Therefore, an improvement scheme was made with the addition of a digital signature function for the authentication process in the key exchange phase of the MPKE protocol. In this study, verification using ProVerif was also carried out on the repair scheme and proved to be able to fix the vulnerabilities in the MPKE protocol.