Summary
The 2018 International Symposium on Information Theory and Its Applications　(ISITA2018)
2018
Session Number:Tu-AM-1-2
Session:
Number:Tu-AM-1-2.5
Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif
Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai,
pp.326-330
Publication Date:2018/10/18
Online ISSN:2188-5079
DOI:10.34385/proc.55.Tu-AM-1-2.5
PDF download
Summary:
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.