# A Security Verification Framework of Cryptographic Protocols
Using Machine Learning

Kentaro Ohno
NTT Computer & Data Science Laboratories  Misato Nakabayashi
NTT Social Informatics Laboratories

###### Abstract

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.

##  1 Introduction

Today, cryptographic protocols are used in a variety of important situations
and are indispensable technologies. For example, TLS 1.3 is used for
confidentiality, tamper detection, and authentication of communication
partners on the Internet [39]. Vulnerabilities in cryptographic protocols can
compromise communications over the Internet and tamper with electronic
transactions. The impact is serious, and therefore the security of
cryptographic protocols is important. However, the design of cryptographic
protocols is generally complex and error-prone.

To design complex and correct cryptographic protocols, designers often use
computer aids such as automated verification tools. As we input the protocol
specification and security requirements, an ideal automated verification tool
instantly outputs whether the protocol satisfies the security requirements or
not. A typical example of such an automatic verification tool is a formal
verification tool based on model checking. Formal verification is a technique
that describes a target using a formal language and verifies whether or not
the target satisfies certain requirements by using mathematical techniques. In
particular, formal verification tools based on model checking provide
exhaustive verification by thoroughly enumerating possible states of the
target and verifying all possible paths to the target. There are many formal
verification tools for cryptographic protocols; ProVerif [8, 10] and Tamarin
prover [3, 38] are well-known examples. These tools are used in the design of
widely used cryptographic protocols and contribute to the design of secure
protocols. For example, formal verification tools were used in the
standardization process of TLS 1.3 and 5G authentication protocols, and many
vulnerabilities were found by these tools [47, 7, 5, 26, 9, 24, 25, 27, 4,
22]. As shown in these examples, the strength of formal verification tools is
that they can find vulnerabilities that are difficult for the human eye to
detect.

The problem with formal verification is the time required to perform
exhaustive verification. In addition, verification may never be completed
because the verification tools do not have decidability [29, 43]. For example,
the TLS verification by Bhargavan et al. [7] took up to 35 hours. Therefore,
the verifier should devise ways to formalize the protocol and use the tools to
complete the verification within the effective time. This requires high-level
expertise. This is one reason that many excellent formal verification tools
for cryptographic protocols exist but have not received enough attention in
the industry.

(a) An example of protocol conversion by the method TLM [37].

(b) An example of protocol conversion by our proposed method.

Figure 1: Comparison of protocol conversion between the previous method [37]
and our proposed method. The previous method loses information on the
hierarchical structure such as the order of application of operations such as
signing and encryption during the conversion (see Section 4.3). In contrast,
the proposed method enables the conversion that reflects the order of
application of operations by using a neural network that incorporates a tree
structure.

To perform verification in practical time, we focus on machine learning
techniques, in particular deep learning, as a verification tool. In general, a
machine learning model makes inferences on a single input decisively in a
short time. Thus, the verification of the security of cryptographic protocols
is expected to always terminate in a short period of time. We consider using
deep learning, which is expected to be highly accurate among machine learning
methods. Deep learning has achieved great successes in a wide range of areas
such as image classification [31], image generation [32], and language
processing [13], particularly where abundant training data are available. The
goal of this paper is to construct a verifier for cryptographic protocols
using machine learning that is practically fast, decidable, and accurate.

To achieve this, large amounts of training data and an appropriate model are
desirable [31, 13]. At present, such a verifier using machine learning has not
been realized. One reason is the difficulty of collecting training data. The
training data consists of pairs of cryptographic protocols and their security
label. This information is usually obtained from papers, textbooks, and
standardization documents. They are few in number, and there are not enough
pairs of cryptographic protocols and their security labels for training.
Therefore, a sufficient amount of training data is difficult to collect. There
are two previous studies using machine learning to verify the security of
cryptographic protocols [37, 45], but the number of training data in those
studies is only 500 to 1000, which is insufficient. Another issue is
construction of machine learning models suitable for processing cryptographic
protocols. Since cryptographic protocols can easily violate the security
requirements if the protocols are slightly changed [12], detailed information
of protocols including hierarchical structures of messages in the protocols
should be encoded to a vector by a machine learning model. However, this makes
it difficult to construct a model that can appropriately handle cryptographic
protocols. Previous studies have proposed methods for converting protocols to
vectors of fixed length, but there is no one-to-one correspondence between
protocols and converted vectors, i.e., multiple different protocols are
converted to the same vector (Figure 1). Such conversion causes the loss of
structural information of the cryptographic protocols, which prevents the
achievement of high verification accuracy. Therefore, for accurate protocol
verification, machine learning models need to be generated that reflect
information on hierarchical structures that are ignored by existing methods.
The construction of a model that adapts to the data structure of cryptographic
protocols is expected to improve the accuracy of security verification and
lead to more advanced applications such as automatic modification of
protocols.

We address the aforementioned two problems. First, we propose a method to
automatically generate training data, i.e., pairs of cryptographic protocols
and security labels. Specifically, we propose a method that automatically
generates a random cryptographic protocol, converts the protocol to the input
format of a formal verification tool, and obtains a security label. This
enables us to prepare arbitrarily large training datasets without manually
collecting protocol data from the literature. Moreover, we propose a method to
construct a model that has both a sequence structure and a tree structure as a
model that can handle cryptographic protocols (Figure 1). This is based on the
idea that a cryptographic protocol is a sequence of messages, i.e., has a
series structure, and each message has a syntax tree structure with encryption
operations, etc. as nodes. The proposed model is suitable for capturing a
hierarchical structure of protocols and thus should verify the security of
protocols more correctly than the previous methods. Furthermore, we show that
the processing time of the model depends linearly on the size of protocols,
which is desirable for practical use. In summary, we propose a novel security
verification framework of cryptographic protocols based on machine learning
that provides practically fast, decidable, and accurate verification.

As a feasibility test, we implemented the proposed method and verified the
confidentiality of the key exchange protocol using practical protocols. In the
results, we achieved a 79.5% verification accuracy.

The contributions of this paper are summarized as follows. To construct a
protocol verifier that is practically fast, decidable, and accurate, we do the
following:

  1. 1.

We propose a method to automatically generate a large training dataset to
achieve a highly accurate security verifier using machine learning for
cryptographic protocols without manually collecting protocol data from the
literature.

  2. 2.

We propose a model having both series and tree structures that is suitable for
handling cryptographic protocols. The proposed model further improves the
accuracy of verification.

  3. 3.

We validate our framework for security verification of cryptographic protocols
based on the method in 1 and the model in 2 above by feasibility tests. The
proposed method achieves 79.5 percent accuracy in verification of practical
protocols.

The paper is organized as follows: Section 2 describes the related works, and
Section 3 briefly introduces cryptographic protocols, their formal
verification techniques, and neural networks. In Section 4, we introduce the
proposed method. Section 5 describes the implementation and experiments, and
Section 6 summarizes this paper.

##  2 Related Work

Several methods have been proposed to verify cryptographic protocols on the
basis of machine learning [37, 45]. Our work is novel in that it tackles two
problems for constructing an accurate verification model: accessing numerous
training data and exploiting detailed hierarchical features of protocols for
learning. Ma et al. [37] were the first to construct an automatic verification
framework for authentication and key exchange protocols using machine
learning. They proposed a method to transform protocols into a vector of fixed
length (Figure 1), created a training dataset from 500 protocols that had
already been verified for security, and built a model to identify security
using machine learning methods such as support vector machine (SVM).
Zahednejad et al. [45] proposed an improvement on Ma et al.’s transformation
of protocols. They also formulated the security verification as a multi-label
classification instead of a multi-class classification and prepared about
1,000 training data, i.e., protocols with security labels to improve the
performance of the classification model. Both of these methods collect
training data manually and ignore the hierarchical structure of messages in
protocols.

Our approach uses machine learning to reduce the computational complexity of
protocol verification. Formal verification of cryptographic protocols has long
been studied in terms of its decidability and computational complexity [29,
43, 40, 2, 18, 1, 15, 16, 17, 19, 36], in particular to complete the
computation in practical time by restricting the class of protocols and the
adversary. Although the verification is generally not decidable, some
subclasses are. However, they all restrict the modeling of the protocol or the
ability of the adversary. For example, verification is decidable when the
number of sessions is bounded or when the adversary is passive, i.e., can
eavesdrop on messages but cannot modify or retransmit them [36, 43]. Durgin et
al. [29] analyzed the complexity of verification under various restrictions
and showed that several subclasses of protocols could be decidable. DEEPSEC
[14] provides a decision procedure and its tools for a limited number of
sessions. Our approach does not require these restrictions on the class of
protocols and the adversary.

##  3 Preliminaries

###  3.1 Cryptographic Protocols

Cryptographic protocols ensure the confidentiality and integrity of data
flowing through a communication channel by using cryptographic primitives such
as public-key cryptography and digital signatures. Key exchange protocols,
authentication protocols, and electronic voting protocols are examples of
cryptographic protocols. Here, we explain several concepts of cryptographic
protocols, using key exchange protocols as an example. A _key exchange
protocol_ is for sharing a session key, which is a common secret key, with a
communicating party over an unreliable communication channel such as the
Internet [12]. The executor of a protocol is called a _party_ , and one action
of executing the party’s protocol (i.e., from the start of message exchange to
the establishment of the session key) is called a _session_. We assume that
there are two parties: the _initiator_ (denoted by $I$), who starts the
session, and the _responder_ (denoted by $R$), who is the communication
partner of the initiator. Each party is assigned a unique identifier called a
_party ID_ , a _long-term secret key_ (denoted by $\mathit{lsk}$), and a
_public key_ (denoted by $\mathit{pk}$) corresponding to the long-term secret
key, and each session is assigned a unique identifier called a session ID. In
addition, ephemeral secret information (e.g., random numbers generated in the
session) used by each party in the protocol is called an _ephemeral secret
key_ (denoted by $\mathit{esk}$). There are two types of key exchange
protocols: transport, in which one party generates a session key and sends it
to the other party, and establishment, in which both parties generate a
session key using the information they exchange.

Key exchange protocols have two main security requirements: session key
confidentiality and authentication. Session key confidentiality means that an
adversary cannot obtain all or part of the session key. Authentication assures
the correctness of the communicating party and prevents an adversary from
impersonating the communicating party.

###  3.2 Formal Verification of Cryptographic Protocols

In formal verification of cryptographic protocols, we describe the protocol
specification and security model (i.e., adversary’s model and security
requirements) in a formal language and mathematically analyze whether the
protocol specification satisfies the security model.

There exist formal verification tools that automatically obtain verification
results, such as ProVerif [8, 10], Scyther [20, 21], Tamarin prover [3, 38],
and Verifpal [34, 35]. These tools have successfully found vulnerabilities and
ensured the security of various cryptographic protocols [4, 6, 24, 25, 44, 47,
48]. For example, formal verification tools have been used to verify TLS 1.3
[25, 24, 6, 7] and 5G authentication protocols [4, 23, 47, 46].

Formal verification, specifically symbolic formal verification techniques,
provides security verification against the Dolev-Yao model [28] and
symbolically models protocol execution, and the adversary’s behavior against
it. In the Dolev-Yao model, key information and protocol messages flowing in
the communication channel are assumed as terms rather than strings.
Furthermore, cryptographic primitives such as public-key cryptosystems are
formalized as idealized ones in which ciphertext can only be decrypted when
the decryption key is possessed (i.e., no plaintext information can be
obtained unless the decryption key is possessed). The adversary is then
modeled as an active adversary who can eavesdrop, tamper, delete, and
retransmit any message that flows through the communication channel.

Formal verification of the Dolev-Yao model has been shown theoretically to be
undecidable [29, 43]. Therefore, verifiers need to manually add lemmas,
restrict network configuration and adversary capabilities, etc., when
verifying protocols. However, this is a practical issue because it requires
expert knowledge.

###  3.3 Deep Learning Models

In this section, we briefly explain classification models based on neural
networks and deep learning [30]. Multi-class classification is the task of
outputting an associated label for input data, and the classification model
estimates the probability distribution $p(y\mid x)$ of label $y$ for input
$x$.

A model structure of a neural network is generally defined by the repetition
and combination of matrix products and nonlinear functions. The most basic
model taking a fixed-length vector as an input is known as _multi-layer
perceptron_ (MLP). Vectors computed in the deep learning model are called
_latent vectors_ of the input data and considered to represent complex
features of the data. Depending on the structure and prior knowledge of the
input data, a suitable model structure should be chosen. Such a dependence is
usually called an inductive bias. For example, for image classification, a
convolutional neural network is the most standard network structure. In this
section, we introduce two model structures that involve sequence and tree
structures, respectively.

A _recurrent neural network_ (RNN) takes series data as input. Let
$(x_{t})_{t=1}^{T}$ be the input series data, where $x_{t}\in\mathbb{R}^{d}$
is a real vector representing the data at time $t$. Let $n$ be the dimension
of the latent vector, and the latent vector $h_{t}\in\mathbb{R}^{n}$ (also
called the state) of RNN is updated at each time $t=1,2,\cdots,T$ as follows:

$\displaystyle h_{t}=\tanh(Wx_{t}+Uh_{t-1}+b),$ (1)

where weight matrices $W\in\mathbb{R}^{n\times d},U\in\mathbb{R}^{n\times n}$
and bias $b\in\mathbb{R}^{n}$ are the parameters of the model. $\tanh$ is a
hyperbolic tangent function, acting on each vector component. The initial
state $h_{0}$ is typically defined as the zero vector. In this way, the latent
vector $h_{t}$ of RNN represents complex temporal dependencies of the series
data $(x_{t})_{t=1}^{T}$. Training of RNN is typically unstable, and thus a
more sophisticated model called a _long short-term memory_ (LSTM) [33] is
commonly used. LSTM is a variant of RNN with another state $c_{t}$ called a
memory cell, equipped with a _gating mechanism_ to control information flow by
utilizing a gate function taking a value in the interval $[0,1]$. The states
in LSTM are updated through gate functions:

$\displaystyle c_{t}$ $\displaystyle=f_{t}\odot
c_{t-1}+i_{t}\odot\tanh(Wx_{t}+Uh_{t-1}+b),$ (2) $\displaystyle h_{t}$
$\displaystyle=o_{t}\odot\tanh(c_{t}),$ (3)

where $f_{t},i_{t},o_{t}\in[0,1]^{n}$ are functions of the state $h_{t-1}$ and
input $x_{t}$ called a forget, input, and output gate, respectively, and
$\odot$ denotes the element-wise product of vectors.

Neural networks that process tree-structured data are constructed by extending
neural networks that process serial data. Child-Sum Tree-LSTM [42] (which we
simply call _Tree-LSTM_) is an extension of LSTM to a tree structure. In the
same way as the LSTM has a state $h_{t}$ and a memory cell $c_{t}$ at each
time step $t$, each node $j$ is associated with a state $h_{j}$ and a memory
cell $c_{j}$ in the Tree-LSTM that are computed on the basis of those of its
child nodes. Let $C(j)$ be the set of child nodes of node $j$. The state
update rule for the latent vector $h_{j}\in\mathbb{R}^{n}$ of node $j$ and the
memory cell $c_{j}\in\mathbb{R}^{n}$ is as follows:

$\displaystyle\tilde{h}_{j}$ $\displaystyle=\sum_{k\in C(j)}h_{k},$ (4)
$\displaystyle c_{j}$ $\displaystyle=i_{j}\odot u_{j}+\sum_{k\in
C(j)}f_{jk}\odot c_{k},$ (5) $\displaystyle u_{j}$
$\displaystyle=\tanh(W_{c}x_{j}+U_{c}\tilde{h}_{j}+b_{c}),$ (6) $\displaystyle
h_{j}$ $\displaystyle=o_{j}\odot\tanh(c_{j}),$ (7)

where $x_{j}$ is an input vector of node $j$. The vectors
$i_{j},f_{jk},o_{j}\in[0,1]^{n}$ denote input, forget, and output gates
computed from the states $h_{j}$ of the child node and the input $x_{j}$,
respectively, controlling the information flow through the node.

Given a latent vector $h\in\mathbb{R}^{n}$ of the input $x$, the distribution
of labels $p(y|x)$ is estimated by linearly transforming $h$ into a vector of
dimensions of the number of label types and applying the softmax function

$\displaystyle\mathrm{softmax}(x)_{i}=\frac{e^{x_{i}}}{\sum_{j}e^{x_{j}}}.$
(8)

The prediction of the model is defined as the label for which this probability
takes the maximum value.

In the training phase, the model parameters are optimized with respect to the
loss function

$\displaystyle L=\frac{1}{N}\sum_{i=1}^{N}-\log p(y_{i}|x_{i})$ (9)

on the basis of a gradient method, where $p(y_{i}|x_{i})$ is the output
distribution of the model. The loss function is averaged over the training
data $\mathcal{D}=\\{(x_{i},y_{i})\\}_{i=1}^{N}$ that consists of a pair of an
input data $x_{i}$ and the label $y_{i}$ of $x_{i}$.

##  4 Proposed Method

In this section, we propose a security verification framework of cryptographic
protocols using machine learning. Our framework has three processes.

The first is generating a dataset for training a machine learning model using
formal verification (Figure 2). This dataset is a set of pairs of a
cryptographic protocol and its security evaluation label. To generate the
dataset, we construct a random automatic cryptographic protocol generator, see
Section 4.2. Generated protocols are input to the formal verification tool and
assigned with security evaluation labels. This process is fully automated and
can generate over tens of thousands of training data.

The second process is to construct the protocol verifier using machine
learning (Figure 2). A machine-learning-based verifier is trained on the
dataset constructed in the first process. We describe the construction of the
model in Section 4.3.

The third process is the verification of cryptographic protocols using a
trained verifier (Figure 2). Users (e.g., the protocol designer) will verify
the security of cryptographic protocols using the verifier constructed in the
second process. Using machine learning, users can verify cryptographic
protocols in practical time, see Section 4.4.

To establish these processes, we utilize a tree representation of the abstract
syntactic structure of messages in protocols. In the first process, we utilize
the tree structure of messages in protocols to automatically generate
protocols and process them for verification. Moreover, in the second process,
we construct a neural network that reflects the tree and series structure of
the cryptographic protocols. In this way, protocols can be input into the
machine learning model with no loss of structural features of the protocols.

[Generate datasets using formal verification tool.]
[Generate verifier using machine learning.]
[Security verification of cryptographic protocols using a verifier with
trained parameters.]

Figure 2: Overview of our proposed framework.

###  4.1 Representation of Cryptographic Protocols

In this section, we introduce representing protocols as sequences of abstract
syntax tree for protocol generation and modeling.

Cryptographic protocols are represented by a sequence of messages exchanged
between parties. Each message of a cryptographic protocol is a string of
letters in which operations such as hash functions and encryption functions
are applied in sequence to message elements such as the party’s ID and secret
key. Therefore, each message of a cryptographic protocol can be represented by
a syntax tree that consists of a leaf node for message elements such as the
party’s ID and session key, an internal node for operations such as
encryption, and a root node for message transmission. Figure 3 shows an
example of the representation of a cryptographic protocol using a syntax tree.
This figure represents the following authentication protocol (ISO/IEC 11770-3
Key Transport Mechanism 4 [41]).

$\displaystyle\begin{split}&I\rightarrow R:\mathit{esk}_{I}\\\ &R\rightarrow
I:\mathit{ID}_{I},\mathit{esk}_{I},\mathit{esk}_{R},\mathrm{aenc}_{I}(\mathit{ID}_{R},\mathit{SK}),\\\
&\hskip
36.98866pt\mathrm{sign}_{R}(\mathit{ID}_{I},\mathit{esk}_{I},\mathit{esk}_{R},\mathrm{aenc}_{I}(\mathit{ID}_{R},\mathit{SK})).\end{split}$
(10)

Figure 3: The representation of ISO/IEC 11770-3 Key Transport Mechanism 4 [41]
using a syntax tree. The colored square nodes represent behavior nodes, the
(white) square nodes represent function nodes, and the round nodes represent
atomic nodes.

Here, $\mathrm{aenc}_{P}$ means a public key encryption operation using party
$P$’s public key, and $\mathrm{sign}_{P}$ means a signature generation
operation using party $P$’s signature key (See Table
LABEL:tab:structual_operation). The meanings of the elements of each message
are shown in Table LABEL:tab:structual_element.

We call an _atomic node_ an element of a message, such as the ID of a party or
a generated random number. $\mathbf{AN}=\\{a_{1},\ldots,a_{N}\\}$ denotes the
set of atomic nodes. We call a _function node_ such as encryption and digital
signature creation operation nodes. $\mathbf{FN}=\\{f_{1},\ldots,f_{M}\\}$
denotes the set of function nodes. A party behavior, such as sending a message
or accepting a session key, is called a _behavior node_.
$\mathbf{BN}=\\{b_{1},\ldots,b_{L}\\}$ denotes the set of behavior nodes. The
elements of each node are defined in accordance with the protocol to be
verified. We define the elements we focus on in this paper in Section 5.1.

###  4.2 Generation of Dataset

To verify the security of a cryptographic protocol using machine learning, a
large amount of training data must be prepared. Since the protocols are few in
number and must be obtained from scattered sources such as academic papers,
they are not easy to manually collect. In this paper, we use a formal
verification tool to generate such a dataset automatically. First, we describe
how to automatically generate the protocols in Section 4.2.1 and then how to
attach evaluation labels to the protocols in Section 4.2.2. Further
improvement on the dataset generation is explained in Section 4.2.3.

####  4.2.1 Automatic Generation of Protocols

To generate a training dataset, we need to generate a grammatically and
functionally correct protocol automatically. A protocol is represented as a
sequence of messages composed of elements (e.g., party IDs and secret keys)
and cryptographic primitives (e.g., encryption, signatures, etc.). Therefore,
we consider here a method to generate protocol messages in accordance with the
protocol grammar.

Algorithm 1 GenerateProtocol

1:Maximum number of message exchanges $m_{\max}$, maximum number of message
elements $c_{\max}$, set of public atomic nodes $\mathbf{AN}_{\mathbf{Pub}}$

2:Protocol $S$

3:$\mathbf{AN}_{I}\coloneqq\mathbf{AN}_{\mathbf{Pub}}\cup\\{\mathit{esk}_{I},\mathit{lsk}_{I},\mathit{K}\\}$

4:$\mathbf{AN}_{R}\coloneqq\mathbf{AN}_{\mathbf{Pub}}\cup\\{\mathit{esk}_{R},\mathit{lsk}_{R},\mathit{K}\\}$

5:$m\xleftarrow{\$}\\{1,\ldots,m_{\max}\\}$

6:for $i=1,\ldots,m$ do

7: if $i$ is odd then

8: $N_{i}\coloneqq\textsc{AddChild}(\\_,\mathrm{sendIR})$

9: $P\leftarrow I$, $Q\leftarrow R$

10: else if $i$ is even then

11: $N_{i}\coloneqq\textsc{AddChild}(\\_,\mathrm{sendRI})$

12: $P\leftarrow R$, $Q\leftarrow I$

13: end if

14: GenerateMessage$(c_{\max},\mathbf{AN}_{P},P,N_{i})$

15: UpdateKnowledge$(\mathbf{AN}_{Q},N_{i},Q)$

16:end for

17:$S:=[N_{1},\ldots,N_{m_{\max}}]$

18:return $S$

Algorithm 2 GenerateMessage

1:Maximum number of message elements $c_{\max}$, set of knowledge of $P$
$\mathbf{AN}_{P}$, party $P$, node $N$

2:function GenerateMessage($c_{\max}$, $\mathbf{AN}_{P}$, $P$, $N$)

3: $c\xleftarrow{\$}\\{1,\ldots,c_{\max}\\}$

4: for $i=1,\ldots,c$ do

5: $e\xleftarrow{\$}\mathbf{AN}_{P}\cup\mathbf{FN}$

6: $N^{\prime}=\textsc{AddChild}(N,e)$

7: if $e\in\mathbf{FN}$ then

8: $\textsc{GenerateMessage}(c_{\max},\mathbf{AN}_{P},P,N^{\prime})$

9: end if

10: end for

11:end function

We show pseudocodes of an algorithm for generating protocols in Algorithm 1
and 2. The outline is as follows:

  1. 1.

Determine the maximum number of message exchanges $m_{max}$ and the maximum
number of message elements $c_{max}$.

  2. 2.

Randomly determine the number of message exchanges from $1,\ldots,m_{max}$
(line 5 in Algorithm 1).

  3. 3.

Set the root node of each message alternately to the operation of sending
messages from $I$ to $R$ and from $R$ to $I$ (lines 7 to 13 in Algorithm 1).

  4. 4.

Randomly select a child node element from the selectable atomic nodes or
function nodes and repeat the process until the message is complete. (lines 5
to 9 in Algorithm 2).

Each party is allowed to use only the information it knows in messages it
sends. This set of information is called the knowledge set, consisting of
atomic nodes and generated messages such as ciphertexts. In step 4 above, each
party selects elements from its own knowledge set. When the party receives
messages, the knowledge set is updated on the basis of the received messages.
In addition to the received messages themselves, information that can be
computed using the information in the knowledge set is added to the knowledge
set. For example, if the knowledge set contains a ciphertext and its
corresponding secret key, then the plaintext of the ciphertext is added to the
knowledge set.
$\mathbf{AN}_{\mathbf{Pub}},\mathbf{AN}_{I},\mathbf{AN}_{R}\subseteq\mathbf{AN}$
in the algorithms represent the knowledge sets of parties.
$\mathbf{AN}_{\mathbf{Pub}}$ is a set of public information from atomic nodes,
including party’s ID, public keys, and timestamps. $\mathbf{AN}_{I}$ and
$\mathbf{AN}_{R}$ are the sets of information known by parties $I$ and $R$,
respectively. These sets contain unique information for each party such as
secret keys. The symbol $\xleftarrow{\$}$ means uniform random choice from a
set.

The algorithm GenerateProtocol takes as input the maximum number of messages
$m_{\max}$, the maximum number of child nodes $c_{\max}$, and the set
$\mathbf{AN}_{\mathbf{Pub}}$, and $\mathbf{FN}$, and outputs the protocol $N$.
First, the knowledge set $\mathbf{AN}_{I},\mathbf{AN}_{R}$ is set as
$\mathbf{AN}_{\mathbf{Pub}}\cup\\{\mathit{esk}_{P},\mathit{lsk}_{P},\mathit{K}\\}$
($P\in\\{I,R\\}$) (lines 3 and 4). Then, the number of messages $m$ is
randomly determined between $1$ to $m_{\max}$ (line 5). Each message is
represented by a syntax tree. The root node of each message is set alternately
by $\mathrm{sendIR}$ and $\mathrm{sendRI}$, which means send a message from
$I$ to $R$ (from $R$ to $I$) (lines 7 to 13). Here, AddChild$(N,e)$ is a
function that adds a child node labeled with
$e\in\mathbf{AN}_{P}\cup\mathbf{FN}$ to the node $N$ and returns the child
node. After that, a message is constructed by adding a child node to the root
node (line 14). GenerateMessage function (see Algorithm 2) generates protocol
messages in accordance with the protocol grammar. Details are described below.
Then, the knowledge set of the communication partner is updated in accordance
with the received messages (line 15). UpdateKnowledge function updates the
knowledge set of party $Q$ with the information of message $N$ from
$\mathbf{AN}_{Q}$. This can be implemented straightforwardly by reading the
generated message $N_{i}$ in the reverse order, that is, from the root to the
leaf nodes, and collecting elements unknown to the party $Q$. The above
process is repeated for the number of message sentences to generate $m$
messages. Finally, they are concatenated and the protocol is output as
$N:=[N_{1},\ldots,N_{m_{\max}}]$.

The recursive function GenerateMessage takes the maximum number of message
elements $c_{\max}$, the knowledge set of party P $\mathbf{AN}_{P}$, and node
$N$, and adds $c$ child nodes to node $N$. $c$ is randomly selected from
$\\{1,\ldots,c_{\max}\\}$.

By generating protocols using the above process, we can automatically generate
protocols. We show an example of protocol generation in the following.

######  Example.

We assume $m_{max}=3$ and $c_{max}=5$. Next, the number of message exchanges
is randomly determined. Here, we assume that $2\in\\{1,2,3\\}$ is chosen as
the number of rounds.

$\displaystyle I\rightarrow R$ $\displaystyle:\ldots$ $\displaystyle
R\rightarrow I$ $\displaystyle:\ldots$

Next, the number of elements in the first message is randomly determined.
Here, we assume that $3\in\\{1,\ldots,5\\}$ is chosen.

$\displaystyle I\rightarrow R$ $\displaystyle:\\_\;,\;\\_\;,\;\\_$
$\displaystyle R\rightarrow I$ $\displaystyle:\ldots$

Next, the parent node of the first element, i.e., the outermost operation, is
randomly determined. Here, we assume that public key encryption
$\mathrm{aenc}\in\mathbf{FN}\cup\mathbf{AN}_{I}$ is chosen.

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\ldots,\mathit{pk}_{R})\;,\;\\_\;,\;\\_$
$\displaystyle R\rightarrow I$ $\displaystyle:\ldots$

Then, the number of message elements to be subjected to public key encryption
is randomly determined. Here, we assume that $1\in\\{1,\ldots,5\\}$ is chosen
at random.

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\\_\;,\mathit{pk}_{R})\;,\;\\_\;,\;\\_$
$\displaystyle R\rightarrow I$ $\displaystyle:\ldots$

Next, the message to be subjected to public key encryption is randomly
determined from the information known to the initiator. Note that since this
is the first message, the initiator only knows the public information and its
own information. Here, we assume that
$\mathit{ID}_{R}\in\mathbf{FN}\cup\mathbf{AN}_{I}$ is chosen.

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\mathit{ID}_{R},\mathit{pk}_{R})\;,\;\\_\;,\;\\_$
$\displaystyle R\rightarrow I$ $\displaystyle:\ldots$

The other two elements of the first message are determined in the same way.
Here we assume that the following selections are made.

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\mathit{ID}_{R},\mathit{pk}_{R})\;,\mathrm{hash}(\mathrm{senc}(\mathit{esk}_{I},\mathit{K}))\;,\mathit{esk}_{I}$
$\displaystyle R\rightarrow I$ $\displaystyle:\ldots$

The first message (from I to R) is now complete. Then, the knowledge set of R
is updated on the basis of the first message, and the next message (from R to
I) is created in the same way.

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\mathit{ID}_{R},\mathit{pk}_{R})\;,\mathrm{hash}(\mathrm{senc}(\mathit{esk}_{I},\mathit{K}))\;,\mathit{esk}_{I}$
$\displaystyle R\rightarrow I$
$\displaystyle:\mathrm{hash}(\mathit{esk}_{I}),\mathit{ID}_{I}$

When generating an establishment-type key exchange protocol, determining what
kind of key to accept as a session key after sending and receiving
(exchanging) messages is necessary. The above algorithms can easily be
extended to such cases. Specifically, the session key is chosen randomly from
the intersection $\mathbf{AN}_{I}\cap\mathbf{AN}_{R}$ of the knowledge set of
the parties. The following is an example:

$\displaystyle I\rightarrow R$
$\displaystyle:\mathrm{aenc}(\mathit{ID}_{R},\mathit{pk}_{R})\;,\mathrm{hash}(\mathrm{senc}(\mathit{esk}_{I},\mathit{K}))\;,\mathit{esk}_{I}$
$\displaystyle R\rightarrow I$
$\displaystyle:\mathrm{hash}(\mathit{esk}_{I}),\mathit{ID}_{I}$
$\displaystyle\mathrm{acceptI}$
$\displaystyle:\mathrm{hash}(\mathit{esk}_{I},\mathit{pk}_{R})$
$\displaystyle\mathrm{acceptR}$
$\displaystyle:\mathrm{hash}(\mathit{esk}_{I},\mathit{pk}_{R})$

####  4.2.2 Automatic Evaluation Labeling of Protocols

For a set of random protocols generated by the method described in the
previous section, the labels for security evaluation are obtained by
converting them to the input format of a formal verification tool and
inputting them to the tool. The method of conversion to the input format of
the formal verification tool strongly depends on the tool. In most cases, a
protocol tree structure can be used for successful conversion. For example,
the ISO/IEC 11770-3 Key Transport Mechanism 4 (see Section 4.1) in the input
format of the formal verification tool ProVerif is shown in Code 1.

Code 1: ProVerif Code of Protocol 10

⬇

1(* Initiator *)

2let Initiator(lsk_I:bitstring, pk_I:bitstring, pk_R:bitstring, K:bitstring) =

3 event protocol_start_I(ID_R);

4 new esk_I1:bitstring;

5 new esk_I2:bitstring;

6 new T_I:bitstring;

7

8 out (c, T_I);

9 in (c, T_R:bitstring);

10

11 (* AUTOMATIC_I *)

12 out(c,(esk_I1));

13 in(c, (=ID_I,=esk_I1,esk_R1:bitstring,m5:bitstring,m6:bitstring));

14 let (=ID_R,SK:bitstring) = adec(m5,lsk_I) in

15 if verif(m6, (ID_I,esk_I1,esk_R1,aenc((ID_R,SK),pk_I)),pk_R)=true then

16 event acceptI(SK);

17 out(c, senc(message, SK)).

18

19(* Responder *)

20let Responder(lsk_R:bitstring, pk_R:bitstring, pk_I:bitstring, K:bitstring)
=

21 event protocol_start_R(ID_I);

22 new esk_R1:bitstring;

23 new esk_R2:bitstring;

24 new SK:bitstring;

25 new T_R:bitstring;

26

27 in (c, T_I:bitstring);

28 out (c, T_R);

29

30 (* AUTOMATIC_R *)

31 in(c, (esk_I1:bitstring));

32
out(c,(ID_I,esk_I1,esk_R1,aenc((ID_R,SK),pk_I),sign((ID_I,esk_I1,esk_R1,aenc((ID_R,SK),pk_I)),lsk_R)));

33 event acceptR(SK).

Lines 1 to 19 represent the initiator’s behavior. Lines 11 to 15 are the code
that is automatically converted from the protocol, which includes sending
(line 12) and receiving (line 13) messages, decrypting the ciphertext (line
14), and verifying the signature (line 15). Lines 22 to 38 represent the
responder behavior, and lines 33 to 35 represent the part that is
automatically converted from the protocol. For details of the ProVerif
grammar, please refer to the official manual [11]. This process allows
automatic collection of protocol-security label pairs without having to
manually collect protocols from papers.

####  4.2.3 Data Augmentation

Automatic protocol generation in the above method results in a high
probability of insecure and unnatural protocols. If those protocols are used
as they are for learning, learning verification tends to fail since the data
distributions of generated protocols and practical ones are much different.
Therefore, we further utilize suitable augmentation of protocol data to
improve training.

Machine learning models are good at capturing patterns in training data. To
train our models to learn patterns in vulnerable protocols, we change parts of
secure protocols to make them insecure and use them as training data. Here, we
convert a secure protocol into a similar insecure one in the following way:

  * •

Sending the session key or secret key over the communication channel.

  * •

Using keys known to the adversary for encryption.

  * •

Creating a session key from information known to the adversary.

For example, modifying protocol 10 in the first way would result in the
following:

$\displaystyle I\rightarrow R:\mathit{esk}_{I}$ $\displaystyle R\rightarrow
I:\mathit{ID}_{I},\mathit{esk}_{I},\mathit{esk}_{R},\mathrm{aenc}_{I}(\mathit{ID}_{R},\mathit{SK}),$
$\displaystyle\hskip
36.98866pt\mathrm{sign}_{R}(\mathit{ID}_{I},\mathit{esk}_{I},\mathit{esk}_{R},\mathrm{aenc}_{I}(\mathit{ID}_{R},\mathit{SK})),\mathit{SK}.$

Thus, by creating pairs of similar secure/insecure protocolsthe model can
learn the patterns that make a protocol insecure, which is expected to improve
the accuracy of verification.

###  4.3 Construction of Machine Learning Model

Common machine learning models such as SVM and MLP take fixed-length vectors
as input. Therefore, cryptographic protocols must be converted to fixed-length
vectors in some way to be taken as inputs [37, 45]. Existing transformation
methods such as TLM [37] ignore the grammatical structure of the message and
cause the loss of structural information of the cryptographic protocol, thus
reducing the accuracy of the security verification. For example, in existing
methods, the protocols

$I\rightarrow
R:\mathrm{sign}_{I}(\mathrm{aenc}_{R}(\mathit{ID}_{I},\mathit{SK}))$

and

$I\rightarrow
R:\mathrm{aenc}_{R}(\mathrm{sign}_{I}(\mathit{ID}_{I},\mathit{SK}))$

are converted to the same vector. That is, the converted vectors cannot be
distinguished between protocols. The elements of each message are shown in
Table LABEL:tab:structual_element. In this section, we propose a new machine
learning model that can accept cryptographic protocols directly by
constructing a neural network that reflects the data structure of the
protocols.

As described in Section 4.1, each message of a cryptographic protocol can be
represented by a syntax tree. Therefore, we construct a new neural network
that processes cryptographic protocols by combining neural networks that deal
with the sequence and tree structures (see Figures 1 and 4). That is, the
proposed model processes a protocol in two stages: it first takes each message
with the tree structure as an input and then processes the latent vector of
each message in sequence. To this end, we utilize the Tree-LSTM for the first
stage and LSTM for the second stage. Since each node in the tree should be
associated with a vector, i.e., $x_{j}$ in Equation 6, to be an input to the
Tree-LSTM model, we assign a random vector sampled from normal distribution to
each behavior, function, and atomic node. After every message in a protocol is
processed in the Tree-LSTM, the sequence of obtained outputs is passed as the
input to the LSTM. Using the output of the LSTM, the protocol is classified as
secure or vulnerable through a linear output layer. The whole model is trained
in a usual way by minimizing the cross-entropy loss with gradient methods.

Figure 4: A neural network for processing protocols. Each message is processed
by a Tree-LSTM with a tree structure, and its output is processed by the LSTM.
Then, through the linear classification layer, which is the output layer, the
prediction of the security label is output as a probability.

###  4.4 Computational Complexity of Verification

After completion of training, the model is used for verification. The main
advantage of our framework is that the verification can always terminate in
practical time. Specifically, we show that our model processes a protocol with
a linear order of time with respect to the size of the protocol. Here, the
size of the protocol is defined as the total number of nodes in the messages.

First, the Tree-LSTM in our model processes each message in a protocol,
reading each node in the message exactly once along the tree structure of the
message. At each node, the Tree-LSTM requires a constant amount of
computational time under the state update rule (6). Thus, the Tree-LSTM
processes a message in a protocol with a linear order of time with respect to
the number of nodes in the message. After that, the LSTM in our model
processes the latent feature of each message returned by the Tree-LSTM along
the sequence structure of the protocol. The computational time of the LSTM is
proportional to the sequence length, i.e., the number of messages in a
protocol, which is bounded by the total number of nodes in the messages. Thus,
the total computational time of our model has a computational complexity of
the linear order with respect to the size of the protocol.

##  5 Experiments

To validate the effectiveness of the proposed method, we evaluate the
performance of the security verification of cryptographic protocols using the
training data generated by the method in Section 4.2 and the machine learning
model constructed by the method in Section 4.3.

###  5.1 Target Protocols and Security Requirement

Our target protocols and security requirements to be verified in this study
are the two-party key exchange protocol and the session key confidentiality
requirements. This is the most standard of all cryptographic protocols.

We cover both transport and establishment type key exchange protocols. We set
the maximum number $m_{\max}$ of messages to 5 and the maximum number of child
nodes $c_{\max}$ to 3. The following describes the elements that compose the
messages and party behavior of the target protocol.

####  5.1.1 Protocol Message Components

The components of protocol messages and their notation are shown in Table
LABEL:tab:structual_element. Here $P$ in the table represents initiator $I$ or
responder $R$, i.e., $P\in\\{I,R\\}$. An ephemeral secret key $\mathit{esk}$
means session-specific secret information such as random numbers, and a static
secret key means a secret key used for decryption of public key encryption,
which is known only to the corresponding party, i.e., $\mathit{esk}_{P}$ and
$\mathit{lsk}_{P}$ are known only to party $P$. The party ID
$\mathit{ID}_{P}$, the public key $\mathit{pk}_{P}$ used to encrypt the public
key cryptography, and the timestamp $T$ are public information, and are known
to parties $I$ and $R$ as well as the adversary. The pre-shared secret key
$\mathit{K}$ is the secret key used to encrypt and decrypt the symmetric key
cryptography, and is known only to parties $I$ and $R$. The session key
$\mathit{SK}$ is shared between parties through message exchange.

Table 1: Protocol Message Components Component |  Notation
---|---
ID of party $P$ |  $\mathit{ID}_{P}$
ephemeral secret key of party $P$ |  $\mathit{esk}_{P}$
static secret key of party $P$ |  $\mathit{lsk}_{P}$
public key of party $P$ |  $\mathit{pk}_{P}$
timestamp of party $P$ |  $T_{P}$
pre-shared secret key of parties |  $\mathit{K}$
session key of party $P$ |  $\mathit{SK}_{P}$

####  5.1.2 Protocol Message Structure

The operations of the parties in composing the message and their notations are
shown in Table LABEL:tab:structual_operation. Here $\vec{m}$ in the table
represents the sequence of messages, i.e., those generated from the components
of the message on the basis of composition method.

We assume that the pre-shared secret key $\mathit{K}$ is used as the symmetric
key when generating the symmetric key ciphertext, the public key
$\mathit{pk}_{Q}$ of communicating party $Q$ is used as the public key when
generating the public key ciphertext, and party $P$’s long-term private key
$\mathit{lsk}_{P}$ is used as the private key when generating the digital
signature.

Table 2: Message Structure Operation |  Notation
---|---
Symmetric key ciphertext of $\vec{m}$ using symmetric key $\mathit{K}$ |  $\mathrm{senc}(\vec{m};\mathit{K})$
Public key ciphertext of $\vec{m}$ using public key $\mathit{pk}$ |  $\mathrm{aenc}(\vec{m};\mathit{pk})$
Digital signature of $\vec{m}$ using static secret key $\mathit{lsk}$ |  $\mathrm{sign}(\vec{m};\mathit{lsk})$
Hash value of $\vec{m}$ |  $\mathrm{hash}(\vec{m})$
Exponent ($m_{0}$ to the power of $m_{1}$) |  $\mathrm{exp}(m_{0};m_{1})$

####  5.1.3 Party Behavior

The party behaviors in the protocol and their notation are shown in Table
LABEL:tab:party_behavior. Note that $m$ in the table denotes an arbitrary
message.

As party operations, we consider the operations of public key encryption,
symmetric key encryption, digital signature, and hash value calculation for
some values (e.g., a message). The value that is the target of the operation
can take the concatenation of multiple values.

Table 3: Party Behavior Behavior |  Notation
---|---
Send $m$ from $I$ to $R$ |  $\mathrm{sendIR}(m)$
Send $m$ from $R$ to $I$ |  $\mathrm{sendRI}(m)$
$I$ accepts $m$ as session key |  $\mathrm{acceptI}(m)$
$R$ accepts $m$ as session key |  $\mathrm{acceptR}(m)$

###  5.2 Evaluation Metrics

We evaluate verification accuracy of trained models with two types of test
datasets. One consists of randomly generated protocols (_Random_) and the
other consists of manually collected practical protocols (_Practical_). The
former includes an equal number of secure and insecure protocols randomly
generated by a method explained in Section 4.2 (without augmentation). The
number of such protocols is 384. The latter consists of protocols collected
manually from a textbook [12]. There are 26 protocols subject to our
verification setting in Section 5.1. The protocols used for evaluation and
their security labels are listed in Table 4. The numbers in the table
represent the protocol numbers in the textbook [12]. Since most of them are
secure, a model judging all protocols as secure achieves high accuracy on
these data, which is not desirable. Therefore, we make insecure protocols by
manipulation similar to the augmentation in Section 4.2.3 and add them to the
test data, which increases the number of practical test data to 44.

Table 4: Protocols Used for Evaluation [12] Protocol | No. | Round | Attack found
---|---|---|---
STS protocol | 1.9 | 3 | no
STS protocol modified to include identifiers | 1.10 | 3 | no
Protocol ntor of Goldberg, Stebila and Ustaoglu | 1.15 | 2 | no
Revised Andrew protocol of Burrows et al. | 3.14 | 4 | yes
Boyd two-pass protocol | 3.16 | 2 | no
ISO/IEC 11770-2 Key Establishment Mechanism 1 | 3.17 | 1 | no
ISO/IEC 11770-2 Key Establishment Mechanism 2 | 3.18 | 1 | no
ISO/IEC 11770-2 Key Establishment Mechanism 3 | 3.19 | 1 | no
ISO/IEC 11770-2 Key Establishment Mechanism 4 | 3.20 | 2 | no
ISO/IEC 11770-2 Key Establishment Mechanism 5 | 3.21 | 2 | no
ISO/IEC 11770-2 Key Establishment Mechanism 6 | 3.22 | 3 | no
ISO/IEC 11770-3 Key Transport Mechanism 1 | 4.11 | 1 | no
ISO/IEC 11770-3 Key Transport Mechanism 2 | 4.12 | 1 | no
ISO/IEC 11770-3 Key Transport Mechanism 3 | 4.13 | 1 | no
Denning-Sacco public key protocol | 4.14 | 1 | no
ISO/IEC 11770-3 Key Transport Mechanism 4 | 4.15 | 2 | no
ISO/IEC 11770-3 Key Transport Mechanism 5 | 4.16 | 3 | no
ISO/IEC 11770-3 Key Transport Mechanism 6 | 4.17 | 3 | no
Helsinki protocol | 4.18 | 3 | yes
Blake-Wilson-Menezes key transport protocol | 4.19 | 3 | no
Needham-Schroeder public key protocol | 4.20 | 3 | yes
Needham-Schroeder-Lowe protocol modeified by Basin et al. | 4.22 | 3 | no
X.509 one-pass authentication | 4.24 | 1 | no
X.509 two-pass authentication | 4.26 | 2 | no
X.509 three-pass authentication | 4.27 | 3 | no
Diffie-Hellman key agreement | 5.1 | 2 | yes

###  5.3 Training Setup

For creating a training dataset, we generate 50,000 protocols following the
method described in Section 4.2.1. Then, we use ProVerif [8, 10], a formal
verification tool of cryptographic protocols, to assign security evaluation
labels to each generated protocol. ProVerif does not ensure decidability and
may require a large amount of verification time, depending on the protocol. In
this experiment, we only deal with protocols that can be verified within five
seconds. After the labeling, we collect the protocols verified as secure and
then generate insecure protocols by data augmentation explained in Section
4.2.3. The resulting number of the training data is 16,371.

We train the model proposed in Section 4.3 on the training dataset. The number
of dimensions of the latent vector of the LSTM and Tree-LSTM in the model is
set to 128. We use RMSprop with batch size 100 to optimize the model with 200
parameter updates. The learning rate is set to 0.001.

As baselines, we apply the previous methods in [37, 45] using the same
generated training dataset. We used TLM [37] and the method of Zahednejad et
al [45] for converting the training data to vectors of fixed size. Since their
conversion rules (e.g., which element corresponds to which scalar) are not
fully explained in either the papers or the public
codes111https://github.com/zahednejad/protocol-analysis-with-machinelearning
of [45], we re-implemented these methods on our own. For learning models, we
adopted XGBoost and 3-layer MLP implementation from the public codes of [45].

###  5.4 Results

Table 5: Accuracy of Verification on Test Sets Conversion | Model | Random | Practical
---|---|---|---
TLM | MLP | 71.6 | 52.3
TLM | Xgboost | 72.3 | 54.6
[45] | MLP | 58.8 | 52.3
[45] | Xgboost | 62.5 | 50.0
N/A | Ours | 85.3 | 79.5

We evaluate the performance of verification by a trained model on the test
datasets. The overall accuracy is shown in Table 5. Note that previous methods
utilize conversion methods of translating protocols into vectors, whereas our
proposed model does not require conversion since protocols are input into the
model with its original tree and sequential structures. The models with
previous methods on modeling protocols [37, 45] verify randomly generated
protocols correctly to some extent, though they almost completely fail to
verify practical protocols. TLM [37] performs better than the method of
Zahednejad et al. [45]. This indicates that TLM provides more natural modeling
of protocols on the basis of their structures than the method of Zahednejad et
al. Our proposed model performs best on both randomly generated protocols and
practical protocols. These results show that our model has a better inductive
bias for dealing with cryptographic protocols.

Figure 5: Processing time for verification with respect to protocol size.

As explained in Section 4.4, the processing time grows linearly with respect
to protocol size in theory, where the protocol size is defined as the total
number of nodes of syntax trees of messages in a protocol. To confirm this
property, we further measured processing time of our model on each protocol in
the randomly generated test set. The results in Figure 5 show that the
processing time indeed grows linearly with respect to the protocol size.
Therefore, our proposed model can manage verification on large protocols.

##  6 Conclusion

In this paper, to construct a security verifier for cryptographic protocols
with practical speed, we proposed a security verification framework for
cryptographic protocols using machine learning. To improve the accuracy of
verification, we established a method to generate cryptographic protocols and
add security labels to the generated protocols using a formal verification
tool to automatically generate large amounts of training data for machine
learning. Furthermore, we constructed a model able to handle both tree and
series structures that is suitable for processing cryptographic protocols. We
implemented the proposed method, conducted a feasibility test for practical
protocols, and achieved an accuracy of 79.5%. These results indicate that the
proposed verification method is more accurate than the previous method with a
practical verification time.

Future issues include further improvement of verification accuracy. To achieve
this, we consider that a method will need to be established for automatically
generating training data that more closely follows actual protocols.
Furthermore, future prospects for the application of machine learning to the
field of cryptographic protocols include inferring the cause of protocol
vulnerabilities, automatically fixing vulnerabilities, and automatically
generating protocols that satisfy specified requirements. We constructed a
verifier in this study, but would like to link it to these studies in the
future.

## References

  * [1] Martín Abadi and Véronique Cortier.  Deciding knowledge in security protocols under equational theories.  Theoretical Computer Science, 367(1-2):2–32, 2006.
  * [2] Roberto M Amadio, Denis Lugiez, and Vincent Vanackere.  On the symbolic reduction of processes with cryptographic functions.  Theoretical Computer Science, 290(1):695–740, 2003.
  * [3] David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, and Benedikt Schmidt.  Tamarin prover, 2020.  https://tamarin-prover.github.io/. Accessed: 2020-12-16.
  * [4] David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, and Vincent Stettler.  A formal analysis of 5g authentication.  In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 1383–1396, 2018.
  * [5] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi.  Verified models and reference implementations for the tls 1.3 standard candidate.  In 2017 IEEE Symposium on Security and Privacy (SP), pages 483–502. IEEE, 2017.
  * [6] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi.  Verified models and reference implementations for the TLS 1.3 standard candidate.  In IEEE Symposium on Security and Privacy (S&P’17), pages 483–503, San Jose, CA, May 2017. IEEE.  Distinguished paper award.
  * [7] Karthikeyan Bhargavan, Vincent Cheval, and Christopher Wood.  A symbolic analysis of privacy for tls 1.3 with encrypted client hello.  In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pages 365–379, 2022.
  * [8] Bruno Blanchet.  Automatic verification of security protocols in the symbolic model: The verifier proverif.  In Foundations of security analysis and design VII, pages 54–87. Springer, 2013.
  * [9] Bruno Blanchet.  Composition theorems for cryptoverif and application to tls 1.3.  In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 16–30. IEEE, 2018.
  * [10] Bruno Blanchet.  Proverif: Cryptographic protocol verifier in the formal model, 2021.  https://prosecco.gforge.inria.fr/personal/bblanche/proverif/. Accessed: 2021-2-5.
  * [11] Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre.  Proverif 2.04: Automatic cryptographic protocol verifier, user manual and tutorial, 2021.
  * [12] Colin Boyd, Anish Mathuria, and Douglas Stebila.  Protocols for authentication and key establishment Second Edition.  Springer, 2019.
  * [13] Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al.  Language models are few-shot learners.  Advances in neural information processing systems, 33:1877–1901, 2020.
  * [14] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina.  Deepsec: Deciding equivalence properties in security protocols theory and practice.  In 2018 IEEE Symposium on Security and Privacy (SP), pages 529–546, 2018.
  * [15] Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune.  Decidability of trace equivalence for protocols with nonces.  In 2015 IEEE 28th Computer Security Foundations Symposium, pages 170–184. IEEE, 2015.
  * [16] Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer.  Computing knowledge in security protocols under convergent equational theories.  In International Conference on Automated Deduction, pages 355–370. Springer, 2009.
  * [17] Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer.  Computing knowledge in security protocols under convergent equational theories.  Journal of Automated Reasoning, 48(2):219–262, 2012.
  * [18] Hubert Comon and Véronique Cortier.  Tree automata with one memory set constraints and cryptographic protocols.  Theoretical Computer Science, 331(1):143–214, 2005.
  * [19] Bruno Conchinha, David Basin, and Carlos Caleiro.  Efficient decision procedures for message deducibility and static equivalence.  In International Workshop on Formal Aspects in Security and Trust, pages 34–49. Springer, 2010.
  * [20] Cas Cremers.  The scyther tool: Verification, falsification, and analysis of security protocols.  In International conference on computer aided verification, pages 414–418. Springer, 2008.
  * [21] Cas Cremers.  The scyther tool, 2021.  https://people.cispa.io/cas.cremers/scyther/. Accessed: 2021-2-5.
  * [22] Cas Cremers and Martin Dehnel-Wild.  Component-based formal analysis of 5g-aka: Channel assumptions and session confusion.  2019\.
  * [23] Cas Cremers and Martin Dehnel-Wild.  Component-based formal analysis of 5g-aka: Channel assumptions and session confusion.  In Network and Distributed Systems Security (NDSS) Symposium 2019, February 2019.
  * [24] Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe.  A comprehensive symbolic analysis of tls 1.3.  In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1773–1788, 2017.
  * [25] Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe.  Automated analysis and verification of tls 1.3: 0-rtt, resumption and delayed authentication.  In 2016 IEEE Symposium on Security and Privacy (SP), pages 470–485. IEEE, 2016.
  * [26] Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan, Jianyang Pan, and Jean Karim Zinzindohoue.  Implementing and proving the tls 1.3 record layer.  In 2017 IEEE Symposium on Security and Privacy (SP), pages 463–482. IEEE, 2017.
  * [27] Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou.  A security model and fully verified implementation for the ietf quic record layer.  In 2021 IEEE Symposium on Security and Privacy (SP), pages 1162–1178. IEEE, 2021.
  * [28] Danny Dolev and Andrew Yao.  On the security of public key protocols.  IEEE Transactions on information theory, 29(2):198–208, 1983.
  * [29] Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov.  Multiset rewriting and the complexity of bounded security protocols.  Journal of Computer Security, 12(2):247–311, 2004.
  * [30] Ian Goodfellow, Yoshua Bengio, and Aaron Courville.  Deep Learning.  MIT Press, 2016.  http://www.deeplearningbook.org.
  * [31] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun.  Deep residual learning for image recognition.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 770–778, 2016.
  * [32] Jonathan Ho, Ajay Jain, and Pieter Abbeel.  Denoising diffusion probabilistic models.  Advances in Neural Information Processing Systems, 33:6840–6851, 2020.
  * [33] Sepp Hochreiter and JÃ¼rgen Schmidhuber.  Long Short-Term Memory.  Neural Computation, 9(8):1735–1780, 11 1997.
  * [34] Nadim Kobeissi.  Verifpal, 2021.  https://verifpal.com/. Accessed: 2021-2-5.
  * [35] Nadim Kobeissi, Georgio Nicolas, and Mukesh Tiwari.  Verifpal: Cryptographic protocol analysis for the real world.  In Proceedings of the 2020 ACM SIGSAC Conference on Cloud Computing Security Workshop, pages 159–159, 2020.
  * [36] Zhiyao Liang and Rakesh M Verma.  Improving techniques for proving undecidability of checking cryptographic protocols.  In 2008 Third International Conference on Availability, Reliability and Security, pages 1067–1074, 2008.
  * [37] Zhuo Ma, Yang Liu, Zhuzhu Wang, Haoran Ge, and Meng Zhao.  A machine learning-based scheme for the security analysis of authentication and key agreement protocols.  Neural Computing and Applications, 32(22):16819–16831, 2020.
  * [38] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin.  The tamarin prover for the symbolic analysis of security protocols.  In International Conference on Computer Aided Verification, pages 696–701. Springer, 2013.
  * [39] Eric Rescorla.  The transport layer security (tls) protocol version 1.3, rfc 8446, 2018\.  https://www.rfc-editor.org/info/rfc8446.
  * [40] Michaël Rusinowitch and Mathieu Turuani.  Protocol insecurity with a finite number of sessions and composed keys is np-complete.  Theoretical Computer Science, 299(1-3):451–475, 2003.
  * [41] International Standard.  Iso: Information technology - security techniques - key management - part 3: Mechanisms using asymmetric techniques iso/iec 11770-3, 2015.  3rd edition.
  * [42] Kai Sheng Tai, Richard Socher, and Christopher D. Manning.  Improved semantic representations from tree-structured long short-term memory networks.  In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 1: Long Papers), pages 1556–1566, Beijing, China, July 2015. Association for Computational Linguistics.
  * [43] Ferucio Laurentiu Tiplea, Constantin Enea, and Catalin V Bîrjoveanu.  Decidability and complexity results for security protocols.  VISSAS, 1:185–211, 2005.
  * [44] Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd, Steve Schneider, Helen Treharne, and Stephan Wesemeyer.  Formal analysis of v2x revocation protocols.  In International Workshop on Security and Trust Management, pages 147–163. Springer, 2017.
  * [45] Behnam Zahednejad, Lishan Ke, and Jing Li.  A novel machine learning-based approach for security analysis of authentication and key agreement protocols.  Security and Communication Networks, 2020, 2020.
  * [46] Jingjing Zhang, Qiang Wang, Lin Yang, and Tao Feng.  Formal verification of 5g-eap-tls authentication protocol.  In 2019 IEEE Fourth International Conference on Data Science in Cyberspace (DSC), pages 503–509, 2019.
  * [47] Jingjing Zhang, Lin Yang, Weipeng Cao, and Qiang Wang.  Formal analysis of 5g eap-tls authentication protocol using proverif.  IEEE Access, 8:23674–23688, 2020.
  * [48] Jingjing Zhang, Lin Yang, Xianming Gao, Gaigai Tang, Jiyong Zhang, and Qiang Wang.  Formal analysis of quic handshake protocol using proverif.  In 2020 7th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2020 6th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom), pages 132–138, 2020.