With the rapid proliferation of various cloud storage services in recent years, the development of technology to efficiently search data while ensuring its confidentiality during cloud usage is an important issue. The technology that enables keyword searches on encrypted files using previously set keywords is called searchable symmetric encryption (SSE). In this paper, we propose a method formally representing encrypted document, and verify the security of SSE using the formal verification tool ProVerif. Our proposed method considers the channel-type terms of ProVerif as a Document that includes different keywords to verify the indistinguishability of encrypted documents.

Symbolic verification tools such as ProVerif can analyze the security of cryptographic protocols automatically. However, if the formal definitions of cryptologic functionalities are incomplete, then the results will be incorrect. Unfortunately, there has so far been no way to analyze the symbolically behavior of such functionalities in the formalization. Furthermore, we have not been able to describe attacker models using such tools. In this paper, we propose a method of defining cryptologic functionalities that uses ProVerif to verify their cryptographic requirements. In addition, by using symbolic verifiers, the proposed method makes it possible to verify cryptographically meaningful security requirements. We therefore expect that this method will contribute to formally defining advanced cryptologic functionalities and accurately verifying the security of cryptographic protocols involving such functionalities.

In this paper, we introduce our formalization of the definitions and theorems related to an elliptic curve over a finite prime field. The elliptic curve is important in an elliptic curve cryptosystem whose security is based on the computational complexity of the elliptic curve discrete logarithm problem.