We propose a security verification framework for cryptographic protocols using machine learning. In recent years, as cryptographic protocols have become more complex, research on automatic verification techniques has been focused on. The main technique is formal verification. However, the formal verification has two problems: it requires a large amount of computational time and does not guarantee decidability. We propose a method that allows security verification with computational time on the order of linear with respect to the size of the protocol using machine learning. In training machine learning models for security verification of cryptographic protocols, a sufficient amount of data, i.e., a set of protocol data with security labels, is difficult to collect from academic papers and other sources. To overcome this issue, we propose a way to create arbitrarily large datasets by automatically generating random protocols and assigning security labels to them using formal verification tools. Furthermore, to exploit structural features of protocols, we construct a neural network that processes a protocol along its series and tree structures. We evaluate the proposed method by applying it to verification of practical cryptographic protocols.

翻译：我们提出了一种利用机器学习对密码协议进行安全验证的框架。近年来，随着密码协议日益复杂，自动验证技术的研究受到广泛关注，其中主要技术为形式化验证。然而，形式化验证存在两大问题：需要大量计算时间且无法保证可判定性。我们提出了一种方法，通过机器学习实现与协议规模呈线性关系计算时间的安全验证。在训练用于密码协议安全验证的机器学习模型时，从学术论文等来源难以获取足够的数据——即带有安全标签的协议数据集。为解决这一问题，我们提出通过自动生成随机协议并利用形式化验证工具为其分配安全标签的方式，创建任意规模的数据集。此外，为充分利用协议的结构特征，我们构建了一个能够沿协议序列与树状结构进行处理的神经网络。通过将所提方法应用于实际密码协议的验证，对其有效性进行了评估。