Formal Security Verification for Searchable Symmetric Encryption Using ProVerif

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.