Resumen
A new class of cryptosystems called verifiable encryption (VE) that facilitates the verification of two plaintexts without decryption was proposed in our previous paper. The main contributions of our previous study include the following. (1) Certain cryptosystems such as the one-time pad belong to the VE class. (2) We constructed an authentication algorithm for unlocking local devices via a network that utilizes the property of VE. (3) As a result of implementing the VE-based authentication algorithm using the one-time pad, the encryption, verification, and decryption processing times are less than 1 ms even with a text length of 8192 bits. All the personal information used in the algorithm is protected by Shanon?s perfect secrecy. (4) The robustness of the algorithm against man-in-the-middle attacks and plaintext attacks was discussed. However, the discussion about the security of the algorithm was insufficient from the following two perspectives: (A) its robustness against other theoretical attacks such as ciphertext-only, known-plaintext, chosen-plaintext, adaptive chosen-plaintext, chosen-ciphertext, and adaptive chosen-ciphertext attacks was not discussed; (B) a formal security analysis using security verification tools was not performed. In this paper, we analyze the security of the VE-based authentication algorithm by discussing its robustness against the above theoretical attacks and by validating the algorithm using a security verification tool. These security analyses, show that known attacks are ineffective against the algorithm.