JAIST Repository
https://dspace.jaist.ac.jp/

Title

Proceedings of the 2nd International Workshop on
Formal Analysis and Verification of Post-Quantum
Cryptographic Protocols (FAVPQC), 2023

Author(s)Escobar, Santiago; Otmani, Ayoub; Akleylek, Sedat;
Ogata, Kazuhiro

CitationIssue Date

2024-02-26

Type

Conference Paper

Text version

publisher

URL

http://hdl.handle.net/10119/18811

RightsCopyright (c) 2024 JAIST Press

Description

The 2nd International Workshop on Formal
Analysis and Verification of Post-Quantum
Cryptographic Protocols (FAVPQC), 2023, Brisbane,
Australia, November 21, 2023

Japan Advanced Institute of Science and Technology

Proceedings of the 2nd International Workshop on
Formal Analysis and Verification of Post-Quantum
Cryptographic Protocols (FAVPQC), 2023

Santiago Escobar1 , Ayoub Otmani2 , Sedat Akleylek3,4 and Kazuhiro Ogata5

ISBN: 978-4-903092-62-1

Preface

Post-quantum cryptographic protocols refer to those replacements of classical cryptographic protocols as a precaution against future attacks from quantum computers. This has been motivatedby the fact that the public-key cryptosystems used today will be no longer secure under largescale quantum computers, which are promisingly becoming available in the near future becauseof the huge research and development investment. Significant efforts have been spent to standardize post-quantum cryptographic primitives and protocols, especially after the Post-quantum
Cryptography Standardization Project started by NIST (https://csrc.nist.gov/projects/postquantum-cryptography). Therefore, security analysis/verification of those post-quantum cryptographic protocols is an important factor in the construction of final secure cryptosystems.
FAVPQC is organized as an event for researchers all over the world to report and discuss research
related to the above-mentioned issue.
Following the previously successful FAVPQC 2022, in 2023, the second workshop has been held
in Brisbane, Australia. The workshop is a satellite event of the 24th International Conference on
Formal Engineering Methods (ICFEM 2023). There were six papers submitted to the workshop
and at least three reviewers who were PC members were assigned to each paper. Through thestandard peer-review process, all six papers were accepted for presentation at the workshop.
Five papers were presented physically at the venue, while one paper was presented online. The
six papers are included in this volume. Note that any PC members (including PC co-chairs) who
are co-authors of a paper was never involved in the peer-review process of the paper.

Program Committee
Sedat Akleylek, Ondokuz Mayis University, Turkey & University of Tartu, Estonia (co-chair)
Christophe Chareton, LORIA-CELLO, France
Canh Minh Do, Japan Advanced Institute of Science and Technology, Japan
Santiago Escobar, Universitat Politecnica de Valencia, Spain (co-chair)
Daniel Gaina, Kyushu University, Japan
Catherine Meadows, Naval Research Laboratory, USA
Paolo Modesti, Teesside University, UK
Masaki Nakamura, Toyama Prefectural University, Japan
Kazuhiro Ogata, Japan Advanced Institute of Science and Technology, Japan (co-chair)
Ayoub Otmani, University of Rouen Normandie, France (co-chair)
Adrian Riesco, Universidad Complutense de Madrid, Spain
Min Zhang, East China Normal University, China

Organization Committee
Sedat Akleylek, Ondokuz Mayis University, Turkey & University of Tartu, Estonia
Santiago Escobar, Polytechnic University of Valencia, Spain
Kazuhiro Ogata, Japan Advanced Institute of Science and Technology, Japan
Ayoub Otmani, University of Rouen Normandie, France

Publicity Committee
Duong Dinh Tran, Japan Advanced Institute of Science and Technology, Japan (chair)

Editors' affiliations and emails
1

Polytechnic University of Valencia, Spain
University of Rouen Normandie, France
3
Ondokuz Mayis University, Turkey
4
University of Tartu, Estonia
5Japan Advanced Institute of Science and Technology, Japan2$ sescobar@upv.es (S. Escobar);ayoub.otmani@univ-rouen.fr (A. Otmani);
sedat.akleylek@bil.omu.edu.tr (S. Akleylek);ogata@jaist.ac.jp (K. Ogata)Table of Contents
Formal specification of the post‐quantum signature scheme FALCON in Maude ………………………… 1
Víctor García, Santiago Escobar and Kazuhiro Ogata
A formal analysis of OpenPGP's post‐quantum public‐key algorithm extension ………………………… 17
Duong Dinh Tran, Kazuhiro Ogata and Santiago Escobar
Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic ……………….. 36
Canh Minh Do, Tsubasa Takagi and Kazuhiro Ogata
Symbolic Model Checking Quantum Circuits With Density Operators in Maude ……………………….. 52
Canh Minh Do and Kazuhiro Ogata
Reachability Analysis of the Equivalence of Two Terms in Free Orthomodular Lattices ……………. 67
Tsubasa Takagi, Canh Minh Do and Kazuhiro Ogata
Theoretical Foundation for Equivalence Checking of Quantum Circuits ……………………………………. 83
Canh Minh Do and Kazuhiro Ogata

Formal specification of the post-quantum signaturescheme FALCON in Maude
Víctor García1,∗ , Santiago Escobar1 and Kazuhiro Ogata2
1
2

Universitat Politècnica de València (UPV), Camí de Vera, s/n, 46022 València, Valencia, Spain
Japan Advanced Institute of Science and Technology (JAIST), Ishikawa 923–1292, Japan

Abstract
Cryptography is an important piece in any communication system. Digital signatures are a part ofcryptography that ensures the authenticity and integrity of digital assets, vital properties for any securecommunication. Due to fast advances in post-quantum technologies, the National Institute of Standards
and Technologies started the Post-Quantum Cryptography project to standardise new algorithms andprotocols that are secure against quantum attackers. One of the finalists is the signature scheme FALCON.
We present the first formal specification, in the high-performance language Maude, of FALCON. For thispurpose, we use an existing framework, originally aimed to formally specify and analyse post quantum
key encapsulation mechanism. With the infrastructure provided by the framework, we encode a symbolicmodel of the signature scheme’s behaviour and simulate an execution trace.

Keywords
Formal specification, Post-Quantum, Signature scheme, FALCON, Maude

1. Introduction
Security is a basic requirement in any information system today, where cryptography has animportant role in fulfilling such needs. A building block of cryptography is a digital signature,a cryptography element that provides authentication and integrity protection to the system
where it is enforced. The security of the most used digital signature schemes, e.g. Rivest-ShamirAdleman (RSA) [1] and Elliptic Curve Digital Signature Algorithm (ECDSA) [2], is based on thehardness of solving computational problems hard to solve for classic computers, such as theprime factorization and discrete logarithm problems. Some algorithms could provide solutions
to these hard computational problems. One example is Shor’s prime factorization algorithm [3]when operating on computers with quantum computing capabilities.
With the race for quantum supremacy at full throttle there is a need for new secure schemes
and protocols that are quantum-resistant. The National Institute of Standards and Technology(NIST) launched the Post-Quantum Cryptography (PQC) project to encourage the development
FAVPQC 2023: 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic
Protocols, November 21, 2023, Brisbane, Australia∗
Corresponding author.
Envelope-Open vicgarval@upv.es (V. García); sescobar@upv.es (S. Escobar); ogata@jaist.ac.jp (K. Ogata)
GLOBE https://v1ct0r-byte.github.io/ (V. García); http://personales.upv.es/sanesro/ (S. Escobar);
http://www.jaist.ac.jp/~ogata/ (K. Ogata)
Orcid 0000-0003-0681-1130 (V. García); 0000-0002-3550-4781 (S. Escobar); 0000-0002-4441-3259 (K. Ogata)1

of new protocols resilient to adversaries with access to quantum computing power. So far, at thetime of writing this paper, there have been 4 rounds, where different Public-key Encryption andKey-establishment Algorithms (KEMs) and Digital Signature Algorithms (DSAs) were submitted
for standardization. The first selection of finalists took place in round 3, where CRYSTALS-Kyber
was the only selected candidate to represent the KEMs section. Moreover, CRYSTALS-Dilithium,
FALCON and SPHINCS+ were the finalists for DSAs. From the three finalists in the DSAs
section we focus on FALCON [4].
In this paper, we present the first steps towards modelling signature schemes by reusing
and adapting a framework previously developed for Key Encapsulation Mechanisms in [5].
Specifically, we show how the framework is adapted to signature schemes and how FALCON
is described in this new framework, obtaining an executable symbolic model that simulates
execution traces. All the specifications presented in this paper can be found in the GitHub
repository at: https://github.com/v1ct0r-byte/PQC-in-Maude/tree/PQ-SIG.
Outline: The rest of the paper is structured as follows. Section 2 lists a series of formal
analysis tools/techniques over post-quantum protocols. Section 3 explains basic concepts on
Maude, the framework we work on and the basic idea of signature schemes. Section 4 presents
the signature scheme detailing the steps in each algorithm. Section 5 settles assumptions forour symbolic model and displays the Maude specification in greater detail, focusing on thespecification of FALCON. Section 6 gives some concluding remarks and future work.

2. Related Work
Advances in protocol security analysis have been made in the field of cryptography. One
interesting idea is the one proposed at [6], where the author explains several examples offormal specification of protocols and introduces and explains the symbolic and computationalmodel analysis approaches. In [7], the authors explore the current literature and papers on
both symbolic and computational analysis of protocols. In this survey, they analyze the resultsby combining both types of analysis. This proposal was initially made by [8] to close the gap
between both lines of protocol verification.
Among the various symbolic protocol analysis tools available, we have Maude-NPA [9, 10],related to the programming language Maude [11, 12, 13]. Maude-NPA has a theoretical basis on
rewriting logic, unification and narrowing and performs a backwards search from a final attack
state to determine whether or not it is reachable from an initial state. Some symbolic tools, suchas ProVerif [14, 15], are based on an abstract representation of a protocol using Horn clauses.
The verification of security properties is done by reasoning on these representative clauses.
Other symbolic tools, such as Tamarin [16, 17], are based on constraint solving to perform an
exhaustive, symbolic search for execution traces. Furthermore, other symbolic tools such as
Scyther [18] or CPSA [19] attempt to enumerate all the essential parts of the different possible
executions of a protocol. Also, AKISS [20] or the DEEPSEC prover [21] are other tools mostly
used to decide equivalence properties.
Some related work can be found for the symbolic security analysis of protocols with quantum
features. For example, the authors of [22] build a model of IKEv2 on a classical setting and2then perform some analysis on it for seven properties, all of it using the Tamarin prover. With
this first symbolic analysis, they prove their model to be correct and corroborate previous
results by other authors. Later, they extended the model with the improvements included in
the latest extension of IKEv2 in order to include a quantum-resistant key exchange. With thisextension, they perform a new analysis, where all properties hold, verifying the security of the
new extension.
Another paper performing symbolic analysis of post-quantum protocols is [23]. The authors
use the recently published tool SAPIC+ to analyze the Ephemeral Diffie Hellman Over COSE(EDHOC) protocol, on its 12th draft version. With SAPIC+ they can automatically transformtheir model to a suitable one in Tamarin, ProVerif or DEEPSEC respective syntax. This allows
the authors to take advantage of the strength of each tool to perform analysis over their modular
composed model of the protocol. With the analysis, they discover several flaws and report themto the team of EDHOC. The authors proposed some fixes, validated them and the proposal was
accepted into the 14th draft version of the protocol.
In [24] a variant for a handshake protocol from the WireGuard VPN protocol with postquantum capabilities is presented. They perform such adaptation by replacing the previous
Diffie-Hellman-based handshake with key-encapsulation mechanisms. The authors verify
the security of their proposal with symbolic and computational proofs. On the one hand,the symbolic proofs verify more security properties than the computational proofs and arecomputer-verified. On the other hand, computational proofs give stronger security guarantees
as the proof makes less idealizing assumptions.
The closest works to our contributions in this paper are [25, 26, 27, 28, 5]. [25] provides afirst approximation on the symbolic specification of post-quantum protocols in Maude-NPA.
The authors decided to specify the Post-Quantum TLS protocol primitives and execution trace.
This type of work is interesting and necessary to us because it demonstrates the capabilityof Maude-NPA, and Maude, to verify more advanced schemes automatically. In the extended
version, [26], the authors report some of the experimental results of formal verification/analysis
over Transport Layer Security using a parallel version of Maude-NPA. [27, 28] present the firstsymbolic security analyses of a collection of post-quantum protocols. These analyses served as
guidelines for the developments presented in [5]. The main differences of our paper with [5]are: (i) we focus on signature schemes, (ii) the three main algorithms are modified to represent
the new steps and (iii) communication now takes place in only one way due to the nature ofdigital signature protocols.
Finally, regarding the post-quantum signature scheme FALCON, as far as the authors know
there are no formal specifications or analyses in the literature.

3. Preliminaries
The section briefly introduces the language used to specify our model, Maude. Moreover, ahigh-level view of the framework used to specify the signature schemes is explained. Finally,an explanation of the nature and general behaviour of signature schemes is given.

33.1. Maude
Maude [12, 11] is a high-level programming language and system implementing rewriting
logic [29]. Rewriting logic is ideally suited to specify and execute computational systems in a
simple and natural way. Some examples are the works in Petri nets [30], process calculus [31],object-based systems [32], asynchronous hardware [33], a mobile ad hoc network protocol [34],cloud-based storage systems [35], web browsers [36], programming languages with threads[37], distributed control systems [38] and models of mammalian cell pathways [39, 40].
Rewriting logic has a sub-logic called membership equational logic. This sub-logic defines
a system’s deterministic parts using functional modules. In contrast, Maude system modules
represent concurrent systems as conditional rewrite theories that model a nondeterministic
system which may never terminate and where the notion of a computed value may be meaningless. In this concurrent system, the membership equational sub-theory defines the statesof such a system as the elements of an algebraic data type, such as terms in an equivalenceclass associated with cryptography properties. We can call this aspect the static part of thespecification. Instead, its dynamics, i.e., how states evolve, are described by the transition rules,
which specify the possible local concurrent transitions of the system.
In the case of analysis, Maude provides a series of tools to analyze specified models. The mostbasic form of system analysis is illustrated by the search command in Maude. The command
performs reachability analysis from an initial state to a target state, searching for states that
violate the invariant. If the invariant fails to hold, it will do so for some finite sequence oftransitions from the initial state, which will be uncovered by the search command above since
all reachable states are explored in a breadth-first manner. If the invariant does hold, we may belucky and have a finite state system, in which case the search command will report failure tofind a violation of the invariant. However, the search will never terminate if an infinite numberof states are reachable from the initial state. Moreover, under the assumption that the set ofstates reachable from an initial state is finite, Maude also supports explicit-state model checking
verification of any properties in linear-time temporal logic (LTL) through its LTL model checker.

3.2. Framework
Our work is developed on the framework proposed from [5]. The framework’s purpose is toease the specification of Key Encapsulation Mechanism (KEMs) in a modular way, splitting thedifferent components into modules. Moreover, with the specifications at hand, the framework
allows the user to run analyses such as invariant analysis or model checking of properties. In [5],the authors present three case studies where Kyber, Classic McEliece and BIKE are modelled andanalysed. These KEMs were candidates of the same round but under the Public-key Encryption
and Key-establishment Algorithm section.
A general picture of the framework is given in Figure 1. There are different modules in
the framework, depicted by the colours of the box, and inclusion relations between modules
are represented by arrows. Functional modules are in blue, and system modules are in red.
The data structures and main algorithms (KeyGen, Enc and Dec) are represented in functional
modules through symbols and equations, e.g. DATA-TYPES module specifies the different datatypes and their properties the scheme handles. Functional module MODEL-CONFIGURATION

4

serves as a basis for the system module, defining the structure upon which the behaviourof the scheme will be specified later. The general configuration handles participants in the
protocol, a network for message passing between the participants, and lists of contact symbols
to be used as keys and values in the symbolic computations. Finally, everything blends in thesystem module KEM . There, the communication actions of honest participants and intruders are
represented by transition rules between states of the general configuration. Thanks to the dataand cryptography properties defined through an equational theory in the functional modules,
symbolic simulations of the protocol can be performed.
KEM

KEM-KEYGEN

KEM-ENC

KEM-DEC

MODEL-CONFIGURATION

KEM-HASH-OPERATIONSDATA-TYPES

Figure 1: Overview of the framework, extracted from [5], used to specify and analyze post-quantum
key encapsulation mechanisms in a modular way.

3.3. Signature schemes
A signature scheme is a mathematical scheme that uses asymmetric cryptography to verify theauthenticity of digital assets, e.g. messages or documents. The asymmetric cryptography takes
place in the form of a pair of keys, one public and one private. As an overview, the private key
is used to sign the asset. Meanwhile, the public key, known by the other participant, is required
to verify the validity of the generated signature. Signature schemes provide a mechanism forparticipants to verify that a message comes from someone they know, given that they know the
public key of the sender.
Let’s see an example of a general flow of a signature scheme. Figure 2 depicts a network
diagram between two participants, Alice and Bob. The participants perform a series of actions
depending on their role in the signature scheme. Let us suppose that Alice initiates the signatureprocess since she wants to send a message, our digital asset, to Bob. To achieve this, Alice firstneeds to generate a pair of keys, a publicly known key and a secret key. After generating the5

6The algorithm to sign some digital assets, Sign, needs the digital asset in question and theprivate key. Note that, in principle, the algorithm would also receive a certain bound 𝛽, but
we simplified the specification based on the assumptions given in Section 5.1. First, a random
value 𝑟 is uniformly sampled, to which the message to sign is concatenated and given to a hashoperation to produce a value 𝑐. This hash value 𝑐 is used along the components of the secret key
to compute a pair of values 𝑠1 and 𝑠2 . Finally, 𝑠2 is compressed to serve as a component of thesignature along with the random value 𝑟. Thus, the signature 𝑠𝑖𝑔 = (𝑟, 𝑠) is the pair of values of
the uniformly sampled 𝑟 and the compressed value 𝑠2 .
The verification algorithm, Verify, uses the sent asset along with its signature, together withthe public key of the sender. Similar to the signing algorithm, a bound 𝛽 is needed, but we omit
it due to the assumptions given in Section 5.1. The verification procedure is as follows. The
value 𝑐 is recomputed using the received message 𝑚 with the second component of the signature,i.e. the salt 𝑟. Then, values 𝑠1 and 𝑠2 are recomputed based on the recomputed value 𝑐. The
value for 𝑠2 is obtained through the decompression of the compressed value in 𝑠. Meanwhile, 𝑠1
depends on the recomputed values of 𝑐 and 𝑠2 , plus the public key, to be recomputed using theformula in step 3. If the recomputed values 𝑠1 and 𝑠2 match the original ones then the signature
is proven to be valid for the received message 𝑚. Otherwise, the signature is rejected and thevalidity of the message can not be proven valid.

pk(m, sig)

Figure 3: Falcon internal algorithms adapted from [4].

7

5. Formal specification with Maude
This section takes a closer look at the formal specification built in Maude. First, a series ofassumptions over the model are made so we can abstract from computational requirements andfocus on the symbolic behaviour, easing the specification. Then we explain how we used theexisting framework to define the different rules, and how the equational theory represents thecryptography properties making the specification executable.

5.1. Assumptions
When symbolically modelling a protocol one can abstract himself from computational aspects
to make the specifications simpler and easier to understand. Such abstractions come at a cost,
making the model less representative of what really happens in the real world, but facilitating thereasoning of the intended behaviour. The assumptions we make for our symbolic specification
over the computational model are:• Any generated polynomials f , g , F and G always satisfy the equation 𝑓 𝐺 − 𝑔𝐹 = 𝑞 mod 𝜙.
This helps to encapsulate on the respective symbolic values any polynomial that will
satisfy the equation.
• The signature and verification algorithms operate always in the bound given by theirparameter 𝛽, thus it is not deemed necessary in the specification of these algorithms.
The assumption allows us to avoid specifying the parameter in algorithms for signature
generation and validation, easing the procedure. The main loss would be the symbolicmodel’s fidelity over an actual implementation, but this can apply to most kinds ofassumptions given their nature.
• The correctness of the encodings s1 and s2 in signature and validation algorithms. In
other words, signature validation of a well-constructed signature for a valid message does
not fail. This assumption allows us to focus on one of the outcomes of the validation
algorithm, i.e. the case in which the signature is proven valid, skipping what would
happen if the signature is rejected.
• Modulus operation over q is equal to modulus operation over (q, 𝜙) . This is one of themost important assumptions we have made, since it will allow us to model the relation
𝑠1 + 𝑠2 ℎ = 𝑐 mod (𝜙, 𝑞) to later obtain 𝑠1 as the equivalent equality 𝑐 − 𝑠2 ℎ mod 𝑞 = 𝑠1 .

5.2. Code specification
The framework from [5] serves as a perfect frame for specifying signature schemes. The maindifferences fall in (i) the participants’ behaviour, since now messages go only one way throughthe communication channel, and (ii) the three main algorithms and their related modules. In
the case of the communication, the rules used to send and receive messages are similar inboth KEMs and DSAs. However, the main algorithms in digital signature schemes differ incontent and application from those of KEMs, thus their modules hold new declarations to use
in the redefined rules. We now dive into the details of each of the main algorithms of FALCON
specified in Maude. Having in mind Figure 3 will help in the explanations.

85.2.1. KeyGen
Similar to KEMs, signature schemes require a key generation algorithm to provide a pair ofkeys. We have defined in module FALCON-KEYGEN , partially shown in Figure 4, the necessary
symbolic values and operations for this algorithm. Specifically, we have defined operator
constants phi and q to represent any possible value of 𝜙 and 𝑞 respectively. The generatorof polynomials 𝑁 𝑇 𝑅𝑈 𝐺𝑒𝑛 is declared and defined through the equation to return a list ofpolynomials 𝑓 , 𝑔, 𝐹 and 𝐺, which are symbolic representations of any possible combination ofthem when receiving the constants phi and q as parameters. Furthermore, operations regarding
Fast Fourier Transformation (FFT), the product between matrices and ffLDL have also been
defined.
fmod FALCON-KEYGEN is...
--- Sample values for KeyGeneration
op phi : -> Polynomial .
op q : -> Nat .
--- Sampler of values f, g, F and G
op NTRUGen : Polynomial Nat -> List{Data} .
ops f g F G : -> Polynomial .
eq NTRUGen(phi, q) = (f g F G) .
--- Matrix of a set of polynomials (this is to construct B)
op mat : List{Data} -> Matrix .
--- Fast Fourier Transformation
op FFT : Matrix -> Polynomial .
op FFT : Polynomial -> Polynomial .
--- Matrix productop _x_ : Polynomial Polynomial -> Matrix .
--- Fast Fourier LDL
op ffLDL : Matrix -> Polynomial .
endfm

Figure 4: Functional module to declare and define values and operations to perform the key generationin FALCON.

The rule for key generation requires two samples from different groups of samples available
as Figure 5 shows in the first line. Specifically, sample values for 𝜙 and 𝑞 from the pools phis andqs are taken. These values serve as the basics for the construction of the public and secret keys.
The conditions of the conditional rule KeyGen serve as representations for some of the internal
steps in the algorithm. The first step is the generation of a list of polynomials L through function
NTRUGen on the sampled values SAM1 and SAM2 . Then, we collapse some of the specification

9

steps in the definition of the secret key SK . The secret key is defined in this second step as apair of elements. The first element of the pair is the result of applying FFT over the resulting
matrix from the elements of L , i.e. f, g, F and G . The second element of the pair is the productbetween ffLDL over the first element of the pair with that same element. Finally, the public key
is defined as the product of the second element of L and the inverse of the first element of L ,modulus the sampled value for 𝑞.
crl [KeyGen] :{phis(SAM1, CONT1), qs(SAM2, CONT2), CONT3}< (ID1[emptyK]peer(ID2)) PS >net(MSGS)=>{phis(CONT1), qs(CONT2), CONT3}< (ID1[publicKey(ID1,PK) ; secretKey(ID1,SK)]qI(ID1,SAM2), phiI(ID1,SAM1), peer(ID2)) PS >net(MSGS)
if L := NTRUGen(SAM1,SAM2) /\SK := ([FFT(mat(L)),ffLDL(FFT(mat(L)) x FFT(mat(L)))]) /\PK := (elem(2,L) p* inv(elem(1,L))) mod SAM2 /\ID1 =/= ID2 .

Figure 5: Conditional rule for the specification of a participant applying the KeyGen algorithm.

5.2.2. Sign
Signature schemes require operations to sign the digital asset, in this case, a message. To thisend, we defined a functional module named FALCON-SIGN , depicted in Figure 6. Similar tomodule FALCON-KEYGEN , the module stores the declarations of sample values necessary forthe signature, as well as operations. Constant values are declared to represent the salt 𝑟 andmessage 𝑚. Furthermore, operators s1 and s2 symbolically represent any value for 𝑠1 and 𝑠2
respectively. Regarding operations, the sampling procedure ffSampling and the inverse Fast
Fourier Transformation invFFT are declared, plus the second one is also defined to return thepair of values s1 and s2 . Finally, an equation representing the property 𝑠1 + 𝑠2ℎ = 𝑐 mod 𝑞
is given. This will prove to be very useful when trying to validate the signature in the Verify
algorithm.
Figure 7 depicts the rule that models the behaviour of a participant applying the Sign algorithm.
The initial requirements for the rule to apply over a participant are: (i) there is some message
to be created, (ii) there is a sample value for r available and (iii) the participant has a secretkey and a value q obtained from the key generation algorithm. Then, the conditions of therule specify how the components are defined following the specification of FALCON. The firststep is to create a hash value c from the message STR and the salt r . In the next two steps, apreimage of c is stored in t and is given as a parameter to ffSampling along the secret key.
The result is then put in a formula, following the pattern on the right-hand side of the equation
for invFFT in Figure 6. This allows the final step to return the pair of short polynomials s1 and10

fmod FALCON-SIGN is...
--- Sample values for r
op r : -> Nat .
--- Sample values for messages
op m : -> String .
--- Fast Fourier Sampling
op ffSampling : Polynomial Polynomial -> Polynomial .
--- Constant values to represent an instance of s_1 and s_2
ops s1 s2 : -> Polynomial .
--- Inverse Fast Fourier Transformation
op invFFT : Polynomial -> Pair .
eq invFFT((P1:Polynomial p- P2:Polynomial) p* FFT(M1:Matrix)) = ([s1,s2]) .
--- Equation specifiyng equality "s1 + s2h = c mod (q)"eq (P1:Polynomial p- (s2 p* P2:Polynomial)) mod N:Nat = s1 .
endfm

Figure 6: Functional module to declare and define values and operations to sign a message in FALCON.

s2 . Finally, a signature associated with STR is placed in the contents of the participant. Thissignature is composed of the sampled random salt r and the compressed value of s2. Take notethat the second component is compressed with a value called SBYTELEN . This symbolic constantis defined to represent the value of the byte length of s .
crl [Sign] :{ms(str(STR), CONT1), rs(SAM1, CONT2), CONT3}< (ID1[secretKey(ID1,SK) ; KS1]qI(ID1,Q), CONT4) PS >net(MSGS)=>{ms(CONT1), rs(CONT2), CONT3}< (ID1[KS1]sig(STR,SAM1,Compress(second(Ss),SBYTELEN)),
mI(ID1,STR), qI(ID1,Q), CONT4) PS >net(MSGS)
if c := HashToPoint(SAM1 || STR, Q, n) /\t := [FFT(c), FFT(0)] p* inv(first(SK)) /\z := ffSampling(t, second(SK)) /\s := (t p- z) p* first(SK) /\Ss := invFFT(s) .

Figure 7: Conditional rule for the specification of a participant applying the Sign algorithm.

115.2.3. Verify
The last algorithm in the scheme, Verify, is depicted with the conditional rule of the same namein Figure 8. The participant must be peers with another one and have received both a public key
and a message along with its corresponding signature from that peer. Now, similar to the Signingalgorithm a hash value c of the message is computed. As the condition shows, the random
value R is obtained from the first component of the signature pair. Then, the recomputationof values s2 and s1 takes place. On the one hand, obtaining the value of s2 is straightforward
since P = Compress(s2, SBYTELEN) . Through the equation Decompress(Compress(S,N),N)= S , where S is some polynomial value and N is some numeric value, we obtain s2. On the other
hand, the value of s1 requires an equational theory based on a relation between values. The
specific relation is given by the equality 𝑠1 + 𝑠2 ℎ = 𝑐 mod (𝜙, 𝑞) available in Algorithm 10 in [4],which we translated into the equivalent equation 𝑐 − 𝑠2 ℎ mod (𝜙, 𝑞) = 𝑠1 by leaving 𝑠1 on theright side alone. This equation makes explicit the relation between the hash 𝑐, the public key ℎand the pair of values 𝑠1 and 𝑠2 . The last condition models the check that the computed values
must be equal to those used during the signing, thus verifying the signature of the message.
crl [Verify] :{CONT1}< (ID1[publicKey(ID2, p mod Q) ; KS1]
mI(ID2,STR), sig(STR,R,P), peer(ID2), CONT2) PS >net(MSGS)=>{CONT1}< (ID1[KS1]mI(ID2,STR), peer(none), CONT2) PS >net(MSGS)
if c := HashToPoint(R || STR, Q, n) /\S2 := Decompress(P, SBYTELEN) /\h := p mod Q /\S1 := (c p- (S2 p* h)) mod Q /\(S1 == s1) /\ (S2 == s2) .

Figure 8: Conditional rule for the specification of a participant applying the Verify algorithm.

5.2.4. Execution
To prove termination of our formal model we run the rewrite command to see if the initial state ends in a state where two honest participants, Alice and Bob, apply the specified
rules. Figure 9 shows the result of applying the said command over initial state init1 ,which is defined as phis(phi), qs(q), ms(str(m)), rs(r)< (Alice[emptyK]peer(Bob))(Eve[emptyK]peer(none)) (Bob[emptyK]peer(Alice)) >net(emptyM) , where from left toright it defines a configuration with: (1) a set of samples, each with one element available, (2)a set of participants with no keys and two of them set to begin the protocol between them,and (3) an empty network of messages, i.e. there is no previous history of message exchanges.
When applying the command we get a new configuration where Alice and Bob finished thecommunication between them, thus they are no longer peers and Bob has the message Alice12

wanted to send him. With it we have proven termination, a liveness property, of the model. We
do not prove any other properties, and leave them for future work.

Figure 9: Execution of the rewrite command over an initial state init1 to check if the symbolic
specification represents an execution of the signature scheme FALCON.

6. Conclusion and future work
We provide a first approach on the formal specification of post-quantum signature schemes.
Specifically we adapted the framework from [5] to serve as a tool for the specification of
signature schemes. The post-quantum signature scheme FALCON served as our case study
to show the feasibility of the Maude language to represent the behaviour of post-quantum
signature schemes along with their cryptography properties.
This work serves as a first step towards the formal verification of signature schemes. Thus, as
future work we plan to use explicit state model checking for the verification of invariants and
LTL Model Checking to check if any interesting property holds in the specified symbolic model.

References[1] R. L. Rivest, A. Shamir, L. Adleman, A method for obtaining digital signatures and publickey cryptosystems, Communications of the ACM 21 (1978) 120–126.
[2] W. J. Caelli, E. P. Dawson, S. A. Rea, Pki, elliptic curve cryptography, and digital signatures,
Computers & Security 18 (1999) 47–66.
[3] P. W. Shor, Polynomial-time algorithms for prime factorization and discrete logarithms on
a quantum computer, SIAM review 41 (1999) 303–332.

13

[4] P.-A. Fouque, J. Hoffstein, P. Kirchner, V. Lyubashevsky, T. Pornin, T. Prest, T. Ricosset,
G. Seiler, W. Whyte, Z. Zhang, Falcon: Fast-fourier lattice-based compact signatures overntru (2020).
[5] V. García, S. Escobar, K. Ogata, S. Akleylek, A. Otmani, Modelling and verification of
post-quantum key encapsulation mechanisms using maude, PeerJ Computer Science 9(2023) e1547.
[6] B. Blanchet, Security protocol verification: Symbolic and computational models, in:International Conference on Principles of Security and Trust, Springer, 2012, pp. 3–29.
[7] V. Cortier, S. Kremer, B. Warinschi, A survey of symbolic methods in computational
analysis of cryptographic systems, Journal of Automated Reasoning 46 (2011) 225–259.
[8] M. Abadi, P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), Journal of cryptology 15 (2002) 103–127.
[9] S. Escobar, C. Meadows, J. Meseguer, Maude-NPA: Cryptographic protocol analysis modulo
equational properties, in: Foundations of Security Analysis and Design V, Springer, 2009,
pp. 1–50.
[10] S. Escobar, C. Meadows, J. Meseguer, A rewriting-based inference system for the nrl
protocol analyzer and its meta-logical properties, Theoretical Computer Science 367 (2006)
162–202.
[11] M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, R. Rubio,
C. Talcott, Maude Manual (version 3.3.1), Technical Report, SRI International, 2023. URL:
http://maude.cs.illinois.edu.
[12] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. M. Oliet, J. Meseguer, C. Talcott, All About Maude- A High-Performance Logical Framework: How to Specify, Program, and Verify Systems
in Rewriting Logic, Lecture Notes in Computer Science, Springer, 2007. URL: http://dx.doi.
org/http://dx.doi.org/10.1007/978-3-540-71999-1. doi:10.1007/978- 3- 540- 71999- 1 .
[13] F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, R. Rubio, C. Talcott, Programming and symbolic computation in maude, Journal of Logical and Algebraic Methods in
Programming 110 (2020) 100497.
[14] B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre, Proverif 2.00: automatic cryptographic
protocol verifier, user manual and tutorial, Version from (2018) 05–16.
[15] B. Blanchet, V. Cheval, V. Cortier, Proverif with lemmas, induction, fast subsumption, andmuch more, in: 2022 IEEE Symposium on Security and Privacy (SP), IEEE, 2022, pp. 69–86.
[16] S. Meier, B. Schmidt, C. Cremers, D. Basin, The tamarin prover for the symbolic analysis of
security protocols, in: International conference on computer aided verification, Springer,
2013, pp. 696–701.
[17] D. Basin, C. Cremers, J. Dreier, R. Sasse, Tamarin: verification of large-scale, real-world,
cryptographic protocols, IEEE Security & Privacy 20 (2022) 24–32.
[18] C. J. Cremers, The scyther tool: Verification, falsification, and analysis of security protocols,
in: International conference on computer aided verification, Springer, 2008, pp. 414–418.
[19] J. Ramsdell, J. Guttman, CPSA4: A cryptographic protocol shapes analyzer,
https://github.com/mitre/cpsaexp, 2018.
[20] I. Gazeau, S. Kremer, Automated analysis of equivalence properties for security protocols
using else branches, in: Computer Security–ESORICS 2017: 22nd European Symposium
on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings,

14

Part II 22, Springer, 2017, pp. 1–20.
[21] V. Cheval, S. Kremer, I. Rakotonirina, The DEEPSEC prover, in: International Conference
on Computer Aided Verification, Springer, 2018, pp. 28–36.
[22] S.-L. Gazdag, S. Grundner-Culemann, T. Guggemos, T. Heider, D. Loebenberger, A formal
analysis of IKEv2’s post-quantum extension, in: Annual Computer Security Applications
Conference, 2021, pp. 91–105.
[23] C. Jacomme, E. Klein, S. Kremer, M. Racouchot, A comprehensive, formal and automatedanalysis of the edhoc protocol, in: USENIX Security’23-32nd USENIX Security Symposium,
2023.
[24] A. Hülsing, K.-C. Ning, P. Schwabe, F. Weber, P. R. Zimmermann, Post-quantum wireguard,
in: 2021 IEEE Symposium on Security and Privacy (SP), IEEE, 2021, pp. 304–321.
[25] D. D. Tran, C. M. Do, S. Escobar, K. Ogata, Hybrid post-quantum tls formal specification inmaude-npa-toward its security analysis?, Proceedings http://ceur-ws.org ISSN 1613 (2022)
0073.
[26] D. D. Tran, C. M. Do, S. Escobar, K. Ogata, Hybrid post-quantum transport layer security
formal analysis in maude-npa and its parallel version, PeerJ Computer Science 9 (2023)
e1556.
[27] D. D. Tran, K. Ogata, S. Escobar, S. Akleylek, A. Otmani, Formal specification and model
checking of lattice-based key encapsulation mechanisms in Maude, in: Rewriting Logic
and its Applications 14th International Workshop, WRLA 2022, 2022, p. 26.
[28] D. D. Tran, K. Ogata, S. Escobar, S. Akleylek, A. Otmani, Formal specification and model
checking of saber lattice-based key encapsulation mechanism in Maude, in: Proceedings ofthe 34th International Conference on Software Engineering and Knowledge Engineering,2022.
[29] J. Meseguer, Conditional rewriting logic as a united model of concurrency, Theor. Comput.
Sci. 96 (1992) 73–155. URL: https://doi.org/10.1016/0304-3975(92)90182-F. doi:10.1016/
0304- 3975(92)90182- F .
[30] M.-O. Stehr, J. Meseguer, P. C. Ölveczky, Rewriting logic as a unifying framework for petri
nets, in: Unifying Petri Nets, Springer, 2001, pp. 250–303.
[31] N. Martí-Oliet, J. A. Verdejo-López, Implementing CCS in Maude, in: Actas de las VIII
Jornadas de Concurrencia: Cuenca, 14 a 16 de junio de 2000, Universidad de Castilla-La
Mancha, 2000, pp. 81–96.
[32] J. Meseguer, A logical theory of concurrent objects and its realization in the Maude
language, in: G. Agha, P. Wegner, A. Yonezawa (Eds.), Research Directions in Concurrent
Object-Oriented Programming, MIT Press, 1993, pp. 314–390.
[33] M. Katelman, S. Keller, J. Meseguer, Rewriting semantics of production rule sets, Journalof Logic and Algebraic Programming 81 (2012) 929–956.
[34] S. Liu, P. C. Ölveczky, J. Meseguer, Modeling and analyzing mobile ad hoc networks in
Real-Time Maude, Journal of Logical and Algebraic Methods in Programming (2015).
[35] R. Bobba, J. Grov, I. Gupta, S. Liu, J. Meseguer, P. Ölveczky, S. Skeirik, Design, Formal
Modeling, and Validation of Cloud Storage Systems using Maude, in: R. H. Campbell, C. A.
Kamhoua, K. A. Kwiat (Eds.), Assured Cloud Computing, J. Wiley, 2018, pp. 10–48. URL:
http://hdl.handle.net/2142/96274.
[36] S. Chen, J. Meseguer, R. Sasse, H. J. Wang, Y.-M. Wang, A systematic approach to uncover15

security flaws in gui logic, in: 2007 IEEE Symposium on Security and Privacy (SP’07),
IEEE, 2007, pp. 71–85.
[37] J. Meseguer, G. Roșu, The rewriting logic semantics project, Theoretical Computer Science
373 (2007) 213–237.
[38] K. Bae, J. Meseguer, P. C. Ölveczky, Formal patterns for multirate distributed real-timesystems, Science of Computer Programming 91 (2014) 3–44.
[39] S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer, K. Sonmez, Pathway logic:
Symbolic analysis of biological signaling, in: Biocomputing 2002, World Scientific, 2001,
pp. 400–412.
[40] C. Talcott, S. Eker, M. Knapp, P. Lincoln, K. Laderoute, Pathway logic modeling of proteinfunctional domains in signal transduction, in: Biocomputing 2004, World Scientific, 2003,
pp. 568–580.

16

A formal analysis of OpenPGP’s post-quantum
public-key algorithm extension
Duong Dinh Tran1,* , Kazuhiro Ogata1 and Santiago Escobar2
1
2

Japan Advanced Institute of Science and Technology, Ishikawa 923-1292, JapanVRAIN, Universitat Politècnica de València, Valencia, Spain

Abstract

OpenPGP is an open standard widely used for encrypting and decrypting communication data. Because
the security of the current public-key algorithms is dangered by the rapid advancement of quantum
computers, a post-quantum extension of the OpenPGP protocol has been proposed in which traditional public-key primitives based on elliptic curve cryptography (ECC) are used in combination with
CRYSTALS-Kyber and CRYSTALS-Dilithium, two presumed quantum-resistant schemes. This paper
presents a formal analysis of the OpenPGP’s post-quantum extension with Maude, a formal specification
language and a high-performance tool. We model the protocol in Maude as a state machine with the presence of two honest participants together with an active attacker who can intercept network connections
and specifically, break the ECC-based public-key algorithms. The security properties under analysis are(1) secrecy of messages and (2) authenticity of messages. By using the Maude search functionality, we
verify that the protocol enjoys (1) and (2) up to depths 13 and 11, respectively.

Keywords

OpenPGP, post-quantum, formal analysis, security verification

1. Introduction
OpenPGP [1, 2] is an open standard of the Pretty Good Privacy (PGP) security program, apopular system used for encrypting and decrypting communications, preventing unwanted
individuals from eavesdropping. The most widely used application of the OpenPGP protocol is
to allow individuals to exchange emails securely by encrypting and decrypting their contents.
Besides, OpenPGP also supports protecting private texts, files, and even whole disk partitions.
OpenPGP supports many public-key encryption and digital signature algorithms. Initially, the
RSA algorithm was used as the public-key encryption scheme. To protect a message, the sender
encrypts it with a random session key that is then encrypted by the receiver’s RSA public key.
Only the recipient can decrypt the session key by using the RSA private key and uses it to
decrypt the encrypted message. Over time, to meet the security requirement, the RSA key
size was increased, which made it lose efficiency. Elliptic Curve Cryptography (ECC), on theother hand, can provide the same security level as RSA with a smaller key size. The OpenPGP
standard was then extended to support signing and key exchange based on ECC by RFC 6637 [3]FAVPQC 2023: International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols,November 21, 2023, Brisbane, Australia.
*
Corresponding author.
$ duongtd@jaist.ac.jp (D. D. Tran); ogata@jaist.ac.jp (K. Ogata); sescobar@upv.es (S. Escobar)17

in 2012. Instead of using the recipient’s RSA public key and private key to encrypt and decrypt
the session key, the sender and recipient use a shared secret established by the Elliptic Curve
Diffie-Hellman (ECDH) method to symmetrically encrypt the session key.
The security of the currently used public-key algorithms, including RSA, ECDH, and ECCbased digital signatures, is threatened by the rapid advancement of quantum computers recently.
On a sufficiently large quantum computer, Shor’s algorithm [4] allows attackers to break thosepublic-key algorithms by efficiently computing the private key from the public key. Facingthat threat, in 2017, The National Institute of Standards and Technology (NIST) started the
Post-Quantum Cryptography Standardization Project [5], which aims to standardize a newclass of public-key algorithms that are resistant to quantum computers as measures before
practical quantum computers become operational. A post-quantum extension for the OpenPGP
protocol [6] has been proposed and standardized by an Internet Engineering Task Force (IETF)
working group. In this extension, a traditional ECC-based public-key encryption scheme isused in combination with CRYSTALS-Kyber [7, 8], a Key Encapsulation Mechanism (KEM),
and an ECC-based digital signature is used in combination with CRYSTALS-Dilithium [9].
CRYSTALS-Kyber and CRYSTALS-Dilithium base their security on the hardness of the learningwith errors problem, which is presumed to be hard even with quantum computers. They are twoof the first group of winners in the standardization project as NIST announced in July 20221 .
Let us shortly refer to them as Kyber and Dilithium. The OpenPGP’s post-quantum extension isreferred to as PQ OpenPGP in this paper.
In this paper, we present a formal analysis of PQ OpenPGP. We use Maude [10], a formal
specification language and a high-performance tool to model the protocol as a state machine.
We employ the equipped invariant model checker in Maude (the search command) to checktwo properties: (1) secrecy of messages and (2) authenticity of messages. The former guarantees
that messages are securely exchanged, that is, no one other than the sender and the recipient
can learn the message content. The latter states that if Bob successfully decrypts an encrypted
message apparently sent from Alice and verifies the signature, obtaining a raw message 𝑀 , thenAlice indeed sent 𝑀 . To model the presence of an attacker, we rely on the standard Dolev-Yao
model [11]. There exists a generic attacker who can control all connections in the network.
Particularly, the attacker can intercept any message sent in the network to collect informationfrom such a message, use all cryptographic primitives to manipulate the available information,and pretend some individual to send a faking message to another individual. Besides, our
specification also allows the attacker to break the security of the ECDH method and the ECCbased digital signature schemes, that is, the attacker can derive the associated private key froma given public key.
The Maude specification of the protocol is publicly available on the webpage2 . The remainderof this paper is organized as follows. Some closely related work is mentioned in Section 2. Next,
in Section 3, we briefly introduce some preliminaries, which are necessary for the rest of thepaper. OpenPGP and its post-quantum extension are described in Section 4. Then, Section 5
and Section 6 present how to model the protocol in Maude and the formal analysis. Finally,
Section 7 summarizes our study.
12

https://csrc.nist.gov/Projects/post-quantum-cryptography/selected-algorithms-2022
https://github.com/duongtd23/pq-openpgp-analysis

18

2. Related work
There are several case studies on applications of formal methods to security analysis of postquantum cryptographic protocols. S. Gazdag et al. [12] have conducted a security analysis
of a post-quantum version of the Internet Key Exchange version 2 (IKEv2). IKEv2 is used to
set up a security association (SA) in the Internet Protocol Security (IPsec) protocol [13], themost popular technology for setting up Virtual Private Networks (VPNs). They showed thatin a quantum setting, i.e., an attacker has access to quantum computers, the original IKEv2 isinsecure, which is similar to what we showed that Eve can learn the ECDH shared secret. They
analyzed an IKEv2’s post-quantum extension proposed in [14, 15], showing that the improved
protocol enjoys all desired security properties. The formal method tool Tamarin [16] was used
for the verification, where Tamarin is well known as one of the most useful tools for formal
analysis of cryptographic protocols. The Tamarin specification of the protocol is essentially astate machine in which each state is an AC-collection of facts and transitions between states,
which model the protocol execution, the behavior of honest participants, and capabilities of theattacker, are specified by Tamarin rules. Tamarin facts and rules are closely similar to observable
components (i.e, name-value pairs) and Maude rewrite rules, respectively. To check a property,
the tool performs an exhaustive, symbolic search based on constraint solving until either asatisfying trace is found or no more rewrite rules can be applied. Because symbolic search is
executed, Tamarin can give security proof with respect to an unbounded number of sessions
and protocol participants. Meanwhile, with our analysis reported in this paper, the number ofparticipants must be fixed.
A. Hülsing et al. [17] have proposed a WireGuard’s post-quantum extension and presented aformal verification of the desired security properties inherited from WireGuard [18], a VPN
protocol focusing on simplicity, fast speed, and high performance. The tool Tamarin [16] wasalso used for the formal verification. They modeled the primitives, messages, etc., used in
the protocol as function symbols and terms, which is similar to our approach with Maude. In
addition, the paper also presented a computational security proof, which gave stronger security
guarantees than the symbolic proof with Tamarin since probability and complexity are taken
into account and fewer idealizing assumptions are made. However, more security propertiesare verified in the verification with Tamarin, and more importantly, it is computer-verified.
There are some existing case studies on analyzing cryptographic protocols and primitives
also by using Maude [19, 20]. In this paper, to verify the security properties, we use only theMaude search command (or invariant model checker). Whereas, liveness and fairness properties
were taken into account in the analysis experiments reported in [20]. They employed the LTL
model checker in Maude. On the other hand, they modeled the protocol under analysis at ahigher level than us, that is, some more simplifications are made in their model.
The Amazon Web Services has proposed a quantum-resistant version of the Transport Layer
Security 1.2 protocol [21], called the Hybrid Post-Quantum TLS [22], and its formal analysis has
been studied in [23]. The analysis was conducted by using Maude-NPA [24] and Par-MaudeNPA [25], a parallel version of Maude-NPA. Maude-NPA is a cryptographic protocol analysis
tool implemented in Maude, based on narrowing & rewriting logic [26]. They used strands [27]
to model the execution of the Hybrid Post-Quantum TLS protocol as well as the capabilities ofa Dolev-Yao attacker. Two properties are verified: (1) secrecy property of the post-quantum

19

key encapsulation mechanism’s shared secret, and (2) authentication property. To check each
property, a Maude-NPA attack state is defined, representing the insecure state that violates
the property. For the analysis, different from Maude’s forward search, Maude-NPA performs abackward search from the attack state to check whether it is reachable from an initial state. The
backward reachability analysis is symbolic, and hence, Maude-NPA can provide security proof
with respect to an unbounded number of sessions and participants, which is an advantage over
our analysis approach with Maude. Because of the very large state space generated, similar to
our results reported in this paper, they can only guarantee that the protocol enjoys (1) and (2)up to depths 12 and 18, respectively, after about 72 days.

3. Preliminaries
This section gives the definition of key encapsulation mechanisms followed by a brief descriptionof the Maude language.

Key Encapsulation Mechanism
According to the NIST standardization project, key exchange algorithms are formulated as Key
Encapsulation Mechanisms (KEMs). The following is the definition of KEMs.
Definition 1. A key encapsulation mechanism is a tuple of algorithms (KeyGen, Encaps, Decaps)
along with a finite key space 𝒦:• KeyGen() → (𝑝𝑘, 𝑠𝑘): A probabilistic key generation algorithm that outputs a public key
𝑝𝑘 and a private key 𝑠𝑘.
• Encaps(𝑝𝑘) → (𝑐, 𝑘): A probabilistic encapsulation algorithm that takes as input a public
key 𝑝𝑘, and outputs a ciphertext (or encapsulation) 𝑐 and a shared secret 𝑘 ∈ 𝒦.
• Decaps(𝑐, 𝑠𝑘) → 𝑘: A deterministic decapsulation algorithm that takes as inputs a ciphertext 𝑐 and a private key 𝑠𝑘, and outputs a shared secret 𝑘 ∈ 𝒦.

Maude
Maude is a declarative language and high-performance tool that focuses on simplicity, expressiveness, and performance to support the formal specification and analysis of concurrent
programs/systems in rewriting logic. In Maude, the most basic building block is modules. There
are two kinds of modules in Maude: functional modules and system modules. A functional
modules is in the form of fmod ℳ is (Σ , E ) endfm, where ℳ is the module name, Σ is anorder-sorted signature and E is an equation set. Σ may contain declarations of sorts (or types),subsorts, operators (or function symbols), and variables. A system module is in the form ofmod ℛ is (Σ , E , R) endm, where R is a set of rewrite rules. Using rewrite rules, we can specify
state transitions of a state machine. A rewrite rule starts with the keyword rl, followed by alabel enclosed with square brackets and a colon, two patterns connected with =>, and ends witha full stop. A conditional one starts with the keyword crl and has a condition following the
keyword if before a full stop. The following is a form of a conditional rewrite rule:20

crl [𝑙𝑏] : 𝑙 => 𝑟 if . . . /\ 𝑐𝑖 /\ . . . .

where 𝑙𝑏 is a label and 𝑐𝑖 is part of the condition, which may be an equation 𝑙𝑐𝑖 = 𝑟𝑐𝑖 . The
negation of 𝑙𝑐𝑖 = 𝑟𝑐𝑖 could be written as (𝑙𝑐𝑖 =/= 𝑟𝑐𝑖 ) = true, where = true could be omitted.
If the condition . . . /\ 𝑐𝑖 /\ . . . holds under some substitution 𝜎, 𝜎(𝑙) can be replaced with𝜎(𝑟).
Maude provides the search command that can find a state reachable from 𝑡 such that the state
matches 𝑝 and satisfies condition(s) 𝑐:
search [n,m] in MOD :𝑡 =>* 𝑝 such that 𝑐 .

where MOD is the name of the module specifying the state machine, and n and m are optional
arguments stating a bound on the number of desired solutions and the maximum depth of
the search, respectively. n typically is 1 and 𝑡 typically represents an initial state of the statemachine.

4. OpenPGP’s post-quantum extension
We describe the OpenPGP protocol followed by its post-quantum extension.

OpenPGP and ECC in OpenPGP
The process that 𝐴 (the sender) sends a message 𝑀 to 𝐵 (the recipient) is shown in Figure 1,
which consists of the following sequence of steps:
1. The sender hashes the message (using the hash function H), and then signs the digest
with his/her private key (𝑠𝑘𝐴 ).
2. The sender randomly selects a key value 𝑘, which is served as a session key to encrypt themessage. Note that this session key is used for this message only, i.e., different messages
use different session keys. For the analysis, we suppose that the session key is uniqueand non-guessable.
3. The sender asymmetrically encrypts (aenc) the session key with the recipient’s publickey (𝑝𝑘𝐵 ), obtaining 𝐶1 .
4. The sender concatenates the message’s signature and the message, and symmetricallyencrypts (senc) it under the session key 𝑘, obtaining 𝐶2 (|| denotes the concatenation).
The concatenation of 𝐶1 and 𝐶2 are outputted as the result.
The process shown in Figure 1 provides confidentiality and integrity to the message being
sent. Depending on the sender’s desire, it may not be desirable to have both security services.
For instance, when integrity is not desirable, the sender will omit the signing part and proceed
to encrypt the message only. In this study, however, we always consider both confidentiality
and integrity to be desirable.
Figure 2 depicts how the recipient decrypts the received ciphertext and validates it, which
consists of the following step sequence:

21

𝑀

H

𝑆𝑖𝑔𝑛 || 𝑀

||

sign

senc

𝐶2

||

𝐶1 || 𝐶2

𝐶1
𝑠𝑘𝐴

aenc

𝑘

𝑝𝑘𝐵

Figure 1: OpenPGP: Sending a message 𝑀

𝐶1 || 𝐶2

adec

𝑘

sdec

𝑆𝑖𝑔𝑛 || 𝑀verifyH

𝑝𝑘𝐴

𝑠𝑘𝐵
Figure 2: OpenPGP: Receiving an encrypted message
Sender private key𝑣

Recipient public key
𝑅

Shared secret𝑆
Derived key
𝑍 = KDF(𝑆)

Session key𝑘Encrypted session key
ECC𝐶 = senc(𝑍, 𝑘)
Output𝐶1 = 𝑉 || ECC𝐶
Figure 3: Session key encryption with ECDH

1. The recipient decrypts the first part of the ciphertext (𝐶1 ) with his/her private key (𝑠𝑘𝐵 )to recover the session key 𝑘.
2. The recipient uses the session key to decrypt the second part of the ciphertext (𝐶2 ),obtaining a message and a signature.
3. The recipient hashes the message and uses the sender public key (𝑝𝑘𝐴 ) to validate theintegrity of the message received.
When the ECDH key exchange method is used, instead of using the recipient’s public key
and private key to encrypt and decrypt the session key as shown in Figure 1 and Figure 2, aso-called derived key is computed from the shared secret and that derived key is used to encrypt22

ECC𝑠𝑘𝐴
𝑀

H

ECC-sign||

𝑆𝑖𝑔𝑛 || 𝑀

Dilithium-sign
DIL𝑠𝑘𝐴
Figure 4: Composite ECC-based signature scheme and CRYSTALS-Dilithium

the session key. The precise step sequence to encrypt the session key with ECDH is given in
Figure 3:
1. The sender first generates an ECDH ephemeral private/public key pair {𝑣, 𝑉 }.
2. The ECDH shared secret 𝑆 is computed from 𝑣 and the recipient public key 𝑅.
3. The sender then uses the key derivation function (KDF) to compute the derived key 𝑍
from the shared secret.
4. The session key 𝑘 is encrypted under the derived key.
5. Finally, the sender concatenates his/her ephemeral public key and the encrypted session
key, outputting the result.
Upon receiving the message, the recipient computes the shared secret from his/her ECDH
private key (the associated private key of 𝑅) and the sender public key 𝑉 . The recipient thenderives 𝑍, uses it to decrypt the session key, and uses the session key to decrypt the message aswell as validate the signature.

OpenPGP’s post-quantum extension
PQ OpenPGP makes use of two pairs of combinations: (1) an ECC-based signature algorithm incombination with CRYSTALS-Dilithium, and (2) ECDH in combination with CRYSTALS-Kyber.
Figure 4 illustrates the composite ECC-based and Dilithium signature schemes. Given a message
𝑀 , the sender hashes it, and signs the message digest with both ECC-based’s and Dilithium’s
sign functions. Note that ECC𝑠𝑘𝐴 and DIL𝑠𝑘𝐴 denote the ECC-based and Dilithium signingprivate key of the sender, respectively. When decrypting the message, the recipient must
validate both signatures.
The Internet-Draft [6] also defines another option in which SPHINCS+ [28] is used as astandalone public-key signature scheme. That option, however, is omitted in this paper.
Figure 5 depicts the composite algorithm with ECDH and Kyber to encrypt a session key 𝑘,which consists of the following sequence of steps:

23

ECDH private key
ECDH𝑣

ECDH public key
ECDH𝑅

Kyber public key
KBR𝑝𝑘
Kyber ciphertext & shared secret(KBR𝐶 , KBR𝑆 ) ← Encaps(KBR𝑝𝑘 )ECDH shared secret
ECDH𝑆

Key-Encryption-Key
𝐾𝐸𝐾 = KeyCombine(ECDH𝑆 , ECDH𝑉 , KBR𝑆 , KBR𝐶 )Session key𝑘Encrypted session key
𝐾𝐶 = senc(𝐾𝐸𝐾, 𝑘)
Output𝐶1 = ECDH𝑉 || KBR𝐶 || 𝐾𝐶
Figure 5: Composite ECDH and CRYSTALS-Kyber

1. The sender first generates an ECDH ephemeral private/public key pair
{ECDH𝑣 , ECDH𝑉 }.
2. The ECDH shared secret ECDH𝑆 is computed from the sender’s private key and therecipient’s public key ECDH𝑅 .
3. Taking the Kyber public key of the recipient as input, the sender performs Kyber Encaps
to generate a ciphertext KBR𝐶 and a shared secret KBR𝑆 . Note that because Encaps
is probabilistic, each time it is invoked, different ciphertext and shared secret will be
generated.
4. The sender then uses a so-called function KeyCombine to compute the so-called KeyEncryption-Key 𝐾𝐸𝐾 from the two shared secrets, the sender’s ECDH public key, andthe Kyber ciphertext.
5. The session key 𝑘 is encrypted under the Key-Encryption-Key.
6. Finally, the sender concatenates his/her ECDH public key, the Kyber ciphertext, and theencrypted session key, outputting the result.
Upon receiving the message, the recipient computes: (1) the ECDH shared secret from his/her
private key (the associated private key of 𝑅) and the sender public key 𝑉 ; and (2) the Kyber
shared secret by performing Decaps, taking his/her private key (the associated private key of
KBR𝑝𝑘 ) and the received Kyber ciphertext as inputs. The recipient then derives Key-EncryptionKey, uses it to decrypt the session key, and uses the session key to decrypt the message as wellas validate the two signatures.
For the analysis, we suppose that the binding between a public key and its owner identifier isalways correctly done. It means that the attacker is unable to claim their public key is a public

24

key of some honest participant. To achieve this purpose, different methods are used together
in OpenPGP, such as, public-key fingerprints, certificates, and web of trust. Web of trust is adecentralized trust model, in contrast to the centralized trust model that relies on a certificate
authority, allowing anyone to sign a partner public key to certify that that public key truly
belongs to that person. Everyone can choose their trusted introducers, from which they trust
all certificates signed by such introducers. In fact, however, no completely satisfactory solution(including the web of trust model) is known to the issue of binding between a public key and its
owner.

5. Modeling the protocol
This section presents how to model PQ OpenPGP in Maude [10], a formal specification language
and a high-performance tool that can be used to analyze a wide range of systems/protocols.

5.1. Modeling ECDH and CRYSTALS-Kyber
ECDH is modeled in the following Maude functional module:
fmod ECDH issorts EdPubKey EdPriKey EdShareS .
derivation of the associated public key from a private key

op pk: EdPriKey-> EdPubKey .

computation of the shared secret from a received public key and a private key

op ss: EdPubKey EdPriKey-> EdShareS .

constructor of a shared secret is a private key pairop | : EdPriKey EdPriKeyvars SK SK2 : EdPriKey .

-> EdShareS [comm] .
declarations of variables

eq ss(pk(SK), SK2) = SK | SK2 .

an equation

endfm

This module first introduces three sorts (or types) EdPubKey, EdPriKey, and EdShareS representing
ECDH public keys, private keys, and shared secrets, respectively. We then declare threeoperators (or function symbols), where the comments followed bygive their corresponding
explanations for what they stand for. For instance, the first operator takes a private key as input
and returns its associated public key as output. The equational attribute comm attached to thelast operator denotes that it is commutative, namely, (𝑠𝑘1 | 𝑠𝑘2 ) and (𝑠𝑘2 | 𝑠𝑘1 ) are identicalwith all private keys 𝑠𝑘1 and 𝑠𝑘2 . The equation defines the semantic of the last operator.
We model Kyber based on the general definition of KEMs, i.e., Definition 1. Another module
is introduced, which contains the following declarations and definitions:sorts KbPubKey KbPriKey KbShareS KbCipher .
KeyGen is a probabilistic algorithm ,so keygen takes a private key as input and returns the public key

op keygen: KbPriKey-> KbPubKey .

similarly , Encaps is probabilistic , so an argument of KbPriKey is added

op encapsC : KbPubKey KbPriKey -> KbCipher .
op encapsK : KbPubKey KbPriKey -> KbShareS .

Encaps: returns ciphertext

op decaps

Decaps: KbCipher KbPriKey -> KbShareS .

25

Encaps: returns shared secretconstructor of a shared secret is a private key pairop&

: KbPriKey KbPriKey -> KbShareS .

vars SK SK2 : KbPriKey .
eq encapsK(keygen(SK), SK2) = (SK & SK2) .
eq decaps(encapsC(keygen(SK), SK2), SK) = (SK & SK2) .

We introduce four sorts KbPubKey, KbPriKey, KbShareS, and KbCipher, representing public keys,
private keys, shared secrets, and ciphertexts (or encapsulations), respectively. As indicatedin Definition 1, KeyGen and Encaps are two probabilistic algorithms. Thus, to specify them as
deterministic procedures in Maude, an argument of the sort KbPriKey is added as the input
argument. With Encaps, we introduce two separate operators encapsC and encapsK, respectively
returning the ciphertext and the shared secret. The first equation defines the semantic of theoperator &. Given a ciphertext and a private key, the second equation states that Decaps properly
outputs the shared secret only if the given ciphertext encapsulates the public key that is theassociated public key of the given private key.

5.2. Modeling cryptographic primitives
We define the generic sort Data as the supersort of all sorts mentioned before, such as EdPubKey
and KbPubKey. || is the concatenation operator, which forms terms of the sort DataL.
sorts Data DataL .
subsorts EdPubKey EdPriKey KbPubKey KbPriKey ... < Data .
subsort Data < DataL .
op nilDL :-> DataL [ctor] .
op||: DataL DataL -> DataL [assoc ctor id: nilDL] .

some other sorts in ...

concatenation

nilDL is the identity element of ||, thanks to the Maude attribute id:. assoc states that || isassociative. ctor states that nilDL and || are constructors of the sort DataL.
Several operators are introduced to model cryptographic primitives. For instance, the operators modeling the hash function, the sign and verify functions of ECC-based digital signatureschemes are as follows:op hop ecSign: DataL: EsPriKey Data-> Data .
-> Data .

ECC based signature: sign-> Bool .

ECC based signature: verify

hash function

sign digest

op ecVerify : EsPubKey Data Data

where EsPriKey and EsPubKey are two sorts of the signing private keys and the verifying publickeys. Given a digest, a verifying public key, and a signature, the following two equations definethat ecVerify returns valid only if the signature is signed with the associated private key of thegiven public key (with the attached attribute owise, the second equation will not be applied
unless the first equation cannot be applied):
eq ecVerify(pkes(SKES), ecSign(SKES,D), D) = true .
eq ecVerify(PKES,
SIGN,D) = false [owise] .

26

5.3. Modeling the protocol execution
We suppose that there exists two honest users together with a dishonest user (the intruder)participating in the protocol. PQ OpenPGP is modeled as a state machine, where each state isin the form of a braced associative-commutative collection (AC-collection) of name-value pairs,
which are called observable components in Maude.
We use the following observable components:• (ecdh[𝑎]: < pk(𝑠𝑘𝑒𝑑) ; 𝑠𝑘𝑒𝑑 >): User 𝑎 has an ECDH public/private key pair pk(𝑠𝑘𝑒𝑑) and𝑠𝑘𝑒𝑑, where < · ; · > is defined as a pair of keys. Recall that the operator pk takes a private
key as input and returns its associated public key as output. In fact, a user may have morethan one ECDH public/private key pair, but for the sake of simplicity, in this analysis, we
restrict each user to only one ECDH public/private key pair.
• (ecsig[𝑎]: < pkes(𝑠𝑘𝑒𝑠) ; 𝑠𝑘𝑒𝑠 >): User 𝑎 has an ECC-based signature scheme’s public/private key pair pkes(𝑠𝑘𝑒𝑠) and 𝑠𝑘𝑒𝑠, where pk(𝑠𝑘𝑒𝑠) denotes the associated public key of𝑠𝑘𝑒𝑠.
• (kyber[𝑎]: < keygen(𝑠𝑘𝑘𝑏) ; 𝑠𝑘𝑘𝑏 >): User 𝑎 has a Kyber public/private key pairkeygen(𝑠𝑘𝑘𝑏) and 𝑠𝑘𝑘𝑏.
• (dilit[𝑎]: < pkdi(𝑠𝑘𝑑𝑖) ; 𝑠𝑘𝑑𝑖 >): User 𝑎 has a Dilithium signature public/private key pairpkdi(𝑠𝑘𝑑𝑖) and 𝑠𝑘𝑑𝑖, where pkdi(𝑠𝑘𝑑𝑖) is the associated public key of 𝑠𝑘𝑒𝑠.
• (rd-sesskey: 𝑘𝑠): 𝑘𝑠 is a space-separated list of available session keys to be used by any
user. That is, whenever a user needs to randomly generate a session key to encrypt a raw
message, the head value of 𝑘𝑠 will be used. Note that we define 𝑘𝑠 as a list instead of a
set to reduce the number of states generated in the checking experiments later on.
• (e-knl: 𝑑𝑠): The intruder’s knowledge is 𝑑𝑠, which is a set of Data’s terms separated by ;.
𝑑𝑠 includes all information that is available to the intruder, such as those grasped frommessages exchanged between other users, and those synthesized by using cryptographic
primitives.
• (nw: 𝑒𝑚𝑠): The network, i.e., the collection of messages exchanged, is 𝑒𝑚𝑠. Each encrypted
message is in the form of msg(𝑎, 𝑏, 𝑐𝑖𝑝ℎ𝑒𝑟), where 𝑎, 𝑏, and 𝑐𝑖𝑝ℎ𝑒𝑟 respectively are thesender, the recipient, and the message content.
• (ms: 𝑚𝑠): 𝑚𝑠 is a space-separated list of raw messages to be sent by users.
• (rd-ecdh: 𝑠𝑘𝑒𝑑𝑠): 𝑠𝑘𝑒𝑑𝑠 is a list of available values to be used as ECDH ephemeral private
keys. That is, whenever a user queries a new ECDH ephemeral private key, the headvalue of 𝑠𝑘𝑒𝑑𝑠 will be used.
• (rd-kyber: 𝑠𝑘𝑘𝑏𝑠): 𝑠𝑘𝑘𝑏𝑠 is a list of available values to be used as Kyber ephemeral privatekeys.
• (used-kyber[𝑎]: 𝑠𝑘𝑘𝑏𝑠): 𝑠𝑘𝑘𝑏𝑠 is a set of Kyber ephemeral private keys that was used byuser 𝑎 and was erased from 𝑎’s memory.

27

The initial state is defined as follows:
eq init ={(ecsig[a]: (< pkes(skes1) ; skes1 >))(dilit[a]: (< pkdi(skdi1) ; skdi1 >))(ecdh[a] : (< pk(sked1) ; sked1 >))(ecdh[b] : (< pk(sked2) ; sked2 >))(kyber[b]: (< keygen(skkb1) ; skkb1 >)) (kyber[a]: (< keygen(skkb2) ; skkb2 >))(ecsig[eve]: (< pkes(skes3) ; skes3 >)) (dilit[eve]: (< pkdi(skdi3) ; skdi3 >))(ecdh[eve] : (< pk(sked3) ; sked3 >))(rd-sesskey: (k1 k2))

(kyber[eve]: (< keygen(skkb3) ; skkb3 >))(rd-ecdh: sked4) (rd-kyber: skkb4)(e-knl: (pkes(skes1) ; pkdi(skdi1) ; pk(sked1) ; pk(sked2) ;keygen(skkb1) ; pkes(skes3) ; skes3 ; pkdi(skdi3) ; skdi3 ;pk(sked3) ; sked3 ; keygen(skkb3) ; skkb3))(nw: empty)(ms: (m1 m2))

(used-kyber[b]: empty) (used-kyber[a]: empty)} .
a and b are the two honest users, while eve is the dishonest one. We suppose that b always be

the recipient, while a always be the sender, and so two key pairs of ECC-based and Dilithium
signatures are given to a. Initially, the intruder’s knowledge includes their own keys and allother participants’ public keys.
Encryption and sending a message is modeled by the following rewrite rule:crl [send] :{(ms: (M MS)) (rd-sesskey: (K KS))(ecsig[A]: (< PKES ; SKES > , SKS))(dilit[A]: (< PKDI ; SKDI > , SKS2))(ecdh[B] : (< PKED ; SKED > , SKS3)) (ecdh[A] : (< PKED2 ; SKED2 > , SKS4))(kyber[B]: (< PKKB ; SKKB > , SKS5)) (kyber[A] : (< PKKB2 ; SKKB2 > , SKS6))(nw: NW) (e-knl: DS) (used-kyber[A]: SKS7) OCs}=> {(ms: MS)(rd-sesskey: KS)(ecsig[A]: (< PKES ; SKES > , SKS)) (dilit[A]: (< PKDI ; SKDI > , SKS2))(ecdh[B] : (< PKED ; SKED > , SKS3)) (ecdh[A] : (SKS4))(kyber[B]: (< PKKB ; SKKB > , SKS5)) (kyber[A] : (SKS6))(nw: (msg(A,B, PKED2 || KBC || KC || C2) NW))
(e-knl: (DS ; PKED2 ; KBC ; KC ; C2))
(used-kyber[A]: (SKS7 , < PKKB2 ; SKKB2 >)) OCs}
if H:= h(M) /\SIGN := ecSign(SKES,H) /\ SIGN2 := diSign(SKDI,H) /\EDSS := ss(PKED,SKED2) /\ KBSS := encapsK(PKKB,SKKB2) /\KBC := encapsC(PKKB,SKKB2) /\KEK := kcombine(EDSS,PKED2,KBSS,KBC) /\KC:= senc(KEK, K) /\C2:= senc(K, SIGN || SIGN2 || M) .
M is the raw message being sent. Sender A first hashes M, obtaining H, and then signs H with his

own ECC-based signature’s and Dilithium’s private keys, obtaining SIGN and SIGN2, respectively.
PKED and PKKB are the ECDH’s and Kyber’s public keys of recipient B, while SKED2 and SKKB2 are
the ECDH’s and Kyber’s ephemeral private keys of A. From these keys, A computes the twoshared secrets EDSS and KBSS as well as the Kyber ciphertext KBC. The key-encryption-key KEK
is then computed by the function kCombine (KeyCombine in Figure 5). A selects session key K,
encrypts it with the key-encryption-key, obtaining KC, and encrypts SIGN || SIGN2 || M with28

K, obtaining C2. The encrypted message msg(A,B, PKED2 || KBC || KC || C2) is put into the

network in the successor state, namely, A sent that message to B. At the same time, the intruder
learns the message content (the message content is put into e-knl), A erases his ECDH’s andKyber’s ephemeral key pairs just used, and the Kyber’s ephemeral private key is put into A’s setof Kyber’s ephemeral private keys used.
We suppose that the sender always deletes ECDH’s and Kyber’s ephemeral keys after sendinga message. In contrast, the recipient is not forced to do so. Typically, users are required toperiodically update the ephemeral keys. We defined two other rewrite rules modeling theprocess by which users generate new ephemeral key pairs.

5.4. Modeling the intruder
The intruder is given a capability of intercepting any message sent in the network to learn
information carried in that message. This capability has been illustrated through the rewrite
rule [send] previously presented. In addition, the intruder can (1) generate random session
keys and raw messages to be sent, and (2) apply any cryptographic primitive function to derive
new information from the information is available to them. Several rewrite rules are defined tomodel (2), some among them are as follows:
hash anythingrl [hash] :{(e-knl: (M ; DS)) OCs} => {(e-knl: (M ; DS ; h(M))) OCs} .
sign anything , SKES is any ECC based signature scheme ’s private keyrl [sign] :{(e-knl: (SKES ; h(D) ; DS)) OCs}=> {(e-knl: (SKES ; h(D) ; DS ; ecSign(SKES,h(D)))) OCs} .
compute keys and encapsulation by Encaps
PKKB and SKKB are variables of Kyber public and private keys

crl [encaps] :{(e-knl: (PKKB ; SKKB ; DS)) OCs}=> {(e-knl: (PKKB ; SKKB ; DS ; encapsC(PKKB, SKKB) ; encapsK(PKKB, SKKB))) OCs}
if PKKB =/= keygen(SKKB) .

With the rewrite rule [hash], the intruder is restricted to hash only raw messages instead of any
terms of sort Data. Even though this restricts the intruder capabilities to some extent, it helps toreduce the number of states generated in the analysis later on. Recall that because we define 𝑑𝑠
in (e-knl: 𝑑𝑠) as a set, there is no duplication in 𝑑𝑠. As a result, it cannot be the case that an
infinite number of different states are produced by applying the rule [hash] infinite times withthe same message M.
We assume practical quantum computers are available to the intruder, from which they canbreak the security of ECDH and ECC-based signature schemes. If a public key of those two
schemes is given to Eve, Eve can derive its associated private key. This capability is specified by
the following two rewrite rules:
breaking ECDH , Eve can derive private keys from public keysrl [break-ecdh] :{(e-knl: (pk(SKED) ; DS)) OCs}=> {(e-knl: (pk(SKED) ; DS ; SKED)) OCs} .

breaking ECC based signature schemes29rl [break-ecc-sign] :{(e-knl: (pkes(SKES) ; DS)) OCs} => {(e-knl: (pkes(SKES) ; DS ; SKES)) OCs} .

6. Formal analysis
We first check that the formal specification allows two users to successfully send an encrypted
message and decrypt it. To this end, we define a Maude search command finding a statereachable from init such that an encrypted message sent from A to B exists in the network andB successfully decrypts and validates the message. Executing that search command, Maude
almost immediately found such a state at the first depth, that is, only one rewrite rule (send) is
applied, changing the state from init to the state found.

6.1. Secrecy of messages
All messages should be securely sent, that is, no one other than the sender and the recipient
can learn the message content. This property can be called the secrecy of messages. To checkthis property, we define the following search command:search [1,10] in PQOPENPGP : init =>*{(ecsig[A]: (< PKES ; SKES > , SKS))(dilit[A]: (< PKDI ; SKDI > , SKS2))(ecdh[B] : (< PKED ; SKED > , SKS3)) (kyber[B]: (< PKKB ; SKKB > , SKS5))(nw: (msg(A,B, PKED2 || KBC || KC || C2) NW))
(e-knl: (M ; DS)) OCs}
such that(A =/= eve and B =/= eve)/\

EDSS := ss(PKED2, SKED)/\ KBSS := decaps(KBC, SKKB) /\KEK := kcombine(EDSS, PKED2, KBSS, KBC) /\K:= sdec(KEK, KC) /\SIGN || SIGN2 || M := sdec(K, C2) /\ecVerify(PKES, SIGN,h(M)) /\

diVerify(PKDI, SIGN2, h(M)) .

The command tries to find a state with bounded depth 10 in which there exists an encrypted
message sent from A to B in the network, B successfully decrypts the raw message M and verifies
the composite signatures, and M exists in Eve’s knowledge. The procedure for the recipient B
to decrypt and validate the message is as follows. B first computes (1) the ECDH shared secret
EDSS from the received public key and her own private key; and (2) the Kyber shared secret
KBSS by the function Decaps with the received encapsulation and her own private key. B thencomputes the key-encryption-key KEK and uses it to decrypt the session key K. B uses the session
key to decrypt the encrypted message, obtaining a raw message M and two signatures. Finally, B
verifies the two signatures.
Maude did not find such a state after about 1 minute and 39 seconds, meaning that the protocol
enjoys the property up to depth 10. The experiment was conducted on a computing server thatcarries 192 GB of memory and a 2.8 GHz microprocessor with 8 cores. The experimental results
are reported in Table 1 and will be discussed in detail below.

30

Property

Depth

ResultTime (h:m:s)

No. States

Secrecy of messages

8
9
10
11
12
13

∅
∅
∅
∅
∅
∅

0:00:6.7
0:00:22.2
0:01:39
0:08:31
0:42:34
5:08:16

46317
98943
206972430750903344
1929731

Authenticity of messages

8
9
10
11

∅
∅
∅
∅

0:06:40
0:23:39
1:26:30
6:54:14

46317
98943
206972430750

Table 1
Experimental results. ∅ means that Maude did not find solution(s) for the given search command.

6.2. Learning ECDH shared secrets
We define another command to show that Eve can learn the ECDH shared secret after a message
is exchanged between two users. This search command is identical to the previous command
used to check the secrecy property of messages sent except that the observable component
e-knl is now changed to the following:(e-knl: (EDSS ; DS))

Recall that EDSS is the ECDH shared secret. Maude found a state after about 6 milliseconds. The
found state is at depth 3 after the three following rewrite rules are applied:
1. rule [send]: a encrypts and sends a message to b.
2. rule [break-ecdh]: eve derives the ECDH ephemeral private key of a from the public key.
3. rule [ss]: eve computes the ECDH shared secret from a’s private key just obtained andb’s public key.

6.3. Authenticity of messages
This property states that if Bob successfully decrypts an encrypted message apparently sent from
Alice and successfully verifies the composite signatures with Alice’s verifying keys, obtaining
a raw message 𝑀 , then Alice indeed sent 𝑀 to Bob. To check the property, we define thefollowing search command:search [1,10] in PQOPENPGP : init =>*{(ecsig[A]: (< PKES ; SKES > , SKS))(dilit[A]: (< PKDI ; SKDI > , SKS2))(ecdh[B] : (< PKED ; SKED > , SKS3)) (kyber[B]: (< PKKB ; SKKB > , SKS5))(e-knl: (PKED2 ; KBC ; KC ; C2 ; DS)) (nw: NW)(used-kyber[A]: (< PKKB2 ; SKKB2 > , SKS6)) OCs}
such that(A =/= eve and B =/= eve)/\

31

EDSS := ss(PKED2, SKED)/\KBSS := decaps(KBC, SKKB) /\KEK:= kcombine(EDSS, PKED2, KBSS, KBC) /\K:= sdec(KEK, KC) /\SIGN || SIGN2 || M := sdec(K, C2) /\ecVerify(PKES, SIGN,h(M)) /\

diVerify(PKDI, SIGN2, h(M)) /\not(msg(A,B, PKED2 || KBC || KC || C2) \in NW) /\KBC == encapsC(PKKB, SKKB2) .

The command tries to find a state with bounded depth 10 such that:(1) Eve knows four pieces of data PKED2, KBC, KC, and C2 (Eve can use these pieces of data
forming a message, and pretend A to send the message to B);(2) from those four pieces of data, B successfully decrypts a raw message M and verifies thesignatures with A’s verifying keys;(3) A did not send those four pieces of data to B, namely, such a message does not exist in the
network.
If such a state exists, it is possible to happen a case in which B receives a valid message apparently
sent from A, but the message is actually forged by Eve. Maude did not find such a state after about
1 hour and 26 minutes. The search command bounds KBC to be the ciphertext encapsulating anephemeral private key of A, meaning that the ciphertext was really created by A. As mentioned
before, we suppose that the binding between a public key (or KEM ciphertext) and its real owneris always correctly done.
Table 1 shows the experimental results of (1) the secrecy of messages from depth 8 to depth 13
and (2) the authenticity of messages from depth 8 to depth 11. Those results confirm that PQ
OpenPGP enjoys (1) and (2) up to depths 13 and 11, respectively. With the same depth, checking(1) is significantly faster than checking (2), which is mostly because, in each state, there is ahuge number of substitutions for the following pattern in the search command of (2):(e-knl: (PKED2 ; KBC ; KC ; C2 ; DS))
KC and C2 are variables of the sort Data, and so they can be substituted by any terms of Data or

its subsorts. Besides, ; is AC, making the number of substitution solutions increase.

7. Concluding remarks
Using the Maude tool, we have presented a formal analysis of the OpenPGP’s post-quantum
extension. The protocol is modeled as a state machine with three participants, one of whom
is an active attacker. The experimental results have confirmed that the protocol enjoys two
properties: secrecy of messages and authenticity of messages up to some specific depths. Even
though we limit the number of protocol participants to three, the number of the state space
generated is really huge (nearly 1 million states at depth 12), which makes us unable to proceedwith the experiments at deeper depths due to time limitations. State explosion, however, is notdedicated to Maude only, but rather the burdensome issue of all analysis/verification approaches
based on model checking.

32

Interactive theorem proving, the complementary approach to model checking, is one possible
way to escape from the state explosion issue. Protocol analysis/verification based on interactive
theorem proving makes it feasible to deal with an infinite state space. In particular, with cryptographic protocols, we can do formal verification with an unbounded number of participants andsession executions. However, this comes at a cost: human creativity is required. Verification byusing the tool IPSG [29] to produce the so-called proof scores [30] is a promising way that weplan to apply the method to the OpenPGP’s post-quantum extension.

References[1] P. Wouters, D. Huigens, J. Winter, N. Yutaka, OpenPGP, Internet-Draft draft-ietf-openpgpcrypto-refresh-10, Internet Engineering Task Force, 2023. URL: https://datatracker.ietf.org/
doc/draft-ietf-openpgp-crypto-refresh/10/, work in Progress.
[2] H. Finney, L. Donnerhacke, J. Callas, R. L. Thayer, D. Shaw, OpenPGP Message Format,
RFC 4880, 2007. doi:10.17487/RFC4880.
[3] A. Jivsov, Elliptic Curve Cryptography (ECC) in OpenPGP, RFC 6637, 2012. doi:10.17487/
RFC6637.
[4] P. Shor, Algorithms for quantum computation: discrete logarithms and factoring, in:Proceedings 35th Annual Symposium on Foundations of Computer Science, 1994, pp.
124–134. doi:10.1109/SFCS.1994.365700.
[5] National Institute of Standards and Technology (NIST), Post-quantum cryptography, NIST,
2017. URL: https://csrc.nist.gov/projects/post-quantum-cryptography.
[6] S. Kousidis, F. Strenzke, A. Wussler, Post-Quantum Cryptography in OpenPGP, InternetDraft draft-wussler-openpgp-pqc-02, Internet Engineering Task Force, 2023. URL: https://datatracker.ietf.org/doc/draft-wussler-openpgp-pqc/02/, work in Progress.
[7] J. W. Bos, L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, J. M. Schanck, P. Schwabe,
G. Seiler, D. Stehlé, CRYSTALS-Kyber: A CCA-secure module-lattice-based KEM, in:2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, London, United
Kingdom, April 24-26, 2018, IEEE, 2018, pp. 353–367. doi:10.1109/EuroSP.2018.00032.
[8] R. Avanzi, J. Bos, L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, J. M. Schanck,
P. Schwabe, G. Seiler, D. Stehlé, CRYSTALS-Kyber: Algorithm Specifications And Supporting Documentation (version 3.02), 2021. URL: https://pq-crystals.org/kyber/data/
kyber-specification-round3-20210804.pdf.
[9] L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, P. Schwabe, G. Seiler, D. Stehlé, CRYSTALSDilithium – Algorithm Specifications and Supporting Documentation (Version 3.1), 2021.
URL: https://pq-crystals.org/dilithium/data/dilithium-specification-round3-20210208.pdf.
[10] F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, R. Rubio, C. L. Talcott, Programming and symbolic computation in maude, J. Log. Algebraic Methods Program. 110 (2020).
doi:10.1016/j.jlamp.2019.100497.
[11] D. Dolev, A. C. Yao, On the security of public key protocols, IEEE Trans. Inf. Theory 29(1983) 198–207.
[12] S. Gazdag, S. Grundner-Culemann, T. Guggemos, T. Heider, D. Loebenberger, A formal
analysis of IKEv2’s post-quantum extension, in: ACSAC ’21: Annual Computer Security

33

Applications Conference, Virtual Event, USA, December 6 - 10, 2021, ACM, 2021, pp.
91–105. doi:10.1145/3485832.3485885.
[13] S. Frankel, S. Krishnan, IP Security (IPsec) and Internet Key Exchange (IKE) Document
Roadmap, RFC 6071, 2011. doi:10.17487/RFC6071.
[14] V. Smyslov, Intermediate Exchange in the Internet Key Exchange Protocol Version 2(IKEv2), RFC 9242, 2022. doi:10.17487/RFC9242.
[15] C. Tjhai, M. Tomlinson, G. Bartlett, S. Fluhrer, D. V. Geest, O. Garcia-Morchon, V. Smyslov,
Multiple Key Exchanges in the Internet Key Exchange Protocol Version 2 (IKEv2), RFC
9370, 2023. doi:10.17487/RFC9370.
[16] D. A. Basin, C. Cremers, J. Dreier, R. Sasse, Symbolically analyzing security protocols
using TAMARIN, ACM SIGLOG News 4 (2017) 19–30. doi:10.1145/3157831.3157835.
[17] A. Hülsing, K. Ning, P. Schwabe, F. Weber, P. R. Zimmermann, Post-quantum wireguard, in:2021 IEEE Symposium on Security and Privacy, 2021, pp. 304–321. doi:10.1109/SP40001.
2021.00030.
[18] J. A. Donenfeld, Wireguard: Next generation kernel network tunnel, in: 24th Annual
Network and Distributed System Security Symposium, NDSS 2017, 2017. https://www.
wireguard.com/papers/wireguard.pdf.
[19] D. D. Tran, K. Ogata, S. Escobar, S. Akleylek, A. Otmani, Kyber, Saber, and SK-MLWR
Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude, IET Information Security 2023 (2023) 9399887. doi:10.1049/2023/9399887.
[20] V. García, S. Escobar, K. Ogata, S. Akleylek, A. Otmani, Modelling and verification of
post-quantum key encapsulation mechanisms using maude, PeerJ Comput. Sci. 9 (2023)
e1547. doi:10.7717/PEERJ-CS.1547.
[21] E. Rescorla, T. Dierks, The Transport Layer Security (TLS) Protocol Version 1.2, RFC 5246,
2008. doi:10.17487/RFC5246.
[22] M. Campagna, E. Crockett, Hybrid Post-Quantum Key Encapsulation Methods (PQ KEM)
for Transport Layer Security 1.2 (TLS), RFC, RFC Editor, 2021. URL: https://datatracker.ietf.
org/doc/html/draft-campagna-tls-bike-sike-hybrid.
[23] D. D. Tran, C. M. Do, S. Escobar, K. Ogata, Hybrid Post-Quantum Transport Layer Security
formal analysis in Maude-NPA and its parallel version, PeerJ Comput. Sci. (2023). To
appear.
[24] S. Escobar, C. Meadows, J. Meseguer, A Rewriting-Based Inference System for the NRL
Protocol Analyzer and Its Meta-Logical Properties, Theor. Comput. Sci. 367 (2006) 162–202.
doi:10.1016/j.tcs.2006.08.035.
[25] C. M. Do, A. Riesco, S. Escobar, K. Ogata, Parallel Maude-NPA for cryptographic protocol
analysis, in: K. Bae (Ed.), Rewriting Logic and Its Applications - 14th International
Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022, Revised Selected
Papers, volume 13252 of Lecture Notes in Computer Science, Springer, 2022, pp. 253–273.
doi:10.1007/978-3-031-12441-9 13.
[26] S. Escobar, J. Meseguer, P. Thati, Narrowing and rewriting logic: from foundations toapplications, in: F. J. López-Fraguas (Ed.), Proceedings of the 15th Workshop on Functionaland (Constraint) Logic Programming, WFLP 2006, Madrid, Spain, November 16-17, 2006,
volume 177 of Electronic Notes in Theoretical Computer Science, Elsevier, 2006, pp. 5–33.
doi:10.1016/j.entcs.2007.01.004.

34

[27] F. J. Thayer, J. C. Herzog, J. D. Guttman, Strand spaces: Why is a security protocolcorrect?, in: Security and Privacy - 1998 IEEE Symposium on Security and Privacy,
Oakland, CA, USA, May 3-6, 1998, Proceedings, IEEE Computer Society, 1998, pp. 160–171.
doi:10.1109/SECPRI.1998.674832.
[28] J.-P. Aumasson, D. J. Bernstein, W. Beullens, C. Dobraunig, M. Eichlseder, S. Fluhrer, S.L. Gazdag, A. Hülsing, P. Kampanakis, S. Kölbl, T. Lange, M. M. Lauridsen, F. Mendel,
R. Niederhagen, C. Rechberger, J. Rijneveld, P. Schwabe, B. Westerbaan, SPHINCS+ –Submission to the 3rd round of the NIST post-quantum project. v3.1, 2022. URL: https://sphincs.org/data/sphincs+-r3.1-specification.pdf.
[29] D. D. Tran, K. Ogata, Formal verification of TLS 1.2 by automatically generating proof
scores, Computers & Security 123 (2022) 102909. doi:https://doi.org/10.1016/j.cose.
2022.102909.
[30] K. Ogata, K. Futatsugi, Proof scores in the OTS/CafeOBJ method, in: Formal Methods
for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference,
FMOODS 2003, Paris, France, volume 2884 of Lecture Notes in Computer Science, Springer,
2003, pp. 170–184. doi:10.1007/978-3-540-39958-2\ 12.

35

Automated Quantum Program Verification in
Probabilistic Dynamic Quantum Logic
Canh Minh Do1,* , Tsubasa Takagi2 and Kazuhiro Ogata1
1
2

Japan Advanced Institute of Science and Technology, 1-8 Asahidai, Nomi, JapanTokyo Institute of Technology, 2-12-1 Ookayama, Meguro-ku, Tokyo, Japan

Abstract

We proposed an automated approach to verifying quantum programs based on Basic Dynamic Quantum
Logic (BDQL), a simplified version of Dynamic Quantum Logic, and developed a support tool in Maude, aspecification/programming language based on rewriting logic, to automate the verification process. This
paper extends BDQL to Probabilistic Dynamic Quantum Logic (PDQL) to verify probabilistic quantum
programs by introducing a probabilistic operator in the formulas of PDQL. We also extend the support toolfor BDQL to make a new support tool for PDQL to automatically verify both qualitative and quantitative
properties for quantum programs with PDQL. As case studies, we use our support tool to verify several
quantum programs: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement
Swapping, Quantum Gate Teleportation, Quantum Relay Scheme, Bidirectional Quantum Teleportation,
Two-qubit Quantum Teleportation, and Quantum Network Coding, where the probability is intentionallyexpressed in the formalizations of quantum programs, demonstrating the expressiveness of PDQL.

Keywords

Probabilistic Dynamic Quantum Logic, Quantum Programs, Quantum Protocols, Dirac notation, Maude

1. Introduction
Quantum computing holds the potential to revolutionize various fields by harnessing theprinciples of quantum mechanics to perform computations that are currently infeasible forclassical computers. For example, in the field of cryptography, the arrival of future quantum
computers has the potential to break widely used public-key cryptography methods, such as
Rivest–Shamir–Adleman (RSA) and Elliptic-curve Cryptography (ECC), by effectively factoring large numbers or solving the discrete logarithm problem using Shor’s fast algorithm [1].
Quantum computing uses different principles of quantum mechanics, such as superposition,
entanglement, and measurement, which are completely different from classical computing. As
a result, it is challenging to accurately design and implement quantum algorithms, programs,
and protocols. Therefore, it is crucial to ensure the correctness of quantum systems throughverification.

The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, November 11, 2023, Brisbane, Australia*
Corresponding author.
$ canhdo@jaist.ac.jp (C. M. Do); takagi.t.ah@m.titech.ac.jp (T. Takagi); ogata@jaist.ac.jp (K. Ogata) 0000-0002-1601-4584 (C. M. Do); 0000-0001-9890-1015 (T. Takagi); 0000-0002-4441-3259 (K. Ogata)

36

Dynamic Logic [2] has been playing a significant role in the formal verification of classical systems for some decades. To handle quantum effects, Dynamic Quantum Logic [3], thequantum counterpart of Dynamic Logic, has been developed. However, we lack an automatedapproach to verifying quantum programs using Dynamic Quantum Logic. Our research groupdevised an automated approach to verifying quantum programs using Basic Dynamic Quantum
Logic (BDQL) [4], a simplified version of Dynamic Quantum Logic, and developed a support
tool in Maude [5], a specification/programming language based on rewriting logic [5], to automate the verification process by incorporating symbolic reasoning for quantum computationin [6]. This paper extends BDQL to Probabilistic Dynamic Quantum Logic (PDQL) to verify
probabilistic quantum programs by introducing a probabilistic operator in the formulas of
PDQL. We also extend the support tool for BDQL to make a new support tool for PDQL toautomatically verify both qualitative and quantitative properties for quantum programs with
PDQL. As case studies, we use our support tool to verify several quantum programs: Superdense Coding [7], Quantum Teleportation [8], Quantum Secret Sharing [9], Entanglement
Swapping [10], Quantum Relay Scheme [11], Bidirectional Quantum Teleportation [12], Quantum Gate Teleportation [13], Two-qubit Quantum Teleportation [14], and Quantum Network
Coding [15], where the probability is intentionally expressed in the formalizations of quantum
programs, demonstrates the expressiveness of PDQL. The support tool and case studies are
publicly available at https://github.com/canhminhdo/DQL.
The rest of the paper is organized as follows: Section 2 describes Basic Dynamic Quantum
Logic (BDQL); Section 3 presents Probabilistic Dynamic Quantum Logic (PDQL); Section 5
demonstrates the application of PDQL for probabilistic quantum program verification; Section 5
describes the implementation of PDQL; Section 6 exhibits the experimental results with our
support tool for several quantum programs; Section 7 presents some existing work; and Section 8
concludes the paper with some pieces of future work.

2. Basic Dynamic Quantum Logic
This section formulates Basic Dynamic Quantum Logic (BDQL) [4]. Let 𝐿0 be a set of atomic
formulas and Π0 be a set of atomic programs. The set 𝐿 of all formulas in BDQL and the set Πof all star-free regular programs are generated by simultaneous induction as follows:
𝐿 ∋ 𝐴 :: = 𝑝 | ¬𝐴 | 𝐴 ∧ 𝐴 | [𝑎]𝐴,Π ∋ 𝑎 :: = skip | abort | 𝜋 | 𝑎 ; 𝑎 | 𝑎 ∪ 𝑎 | 𝐴?,
where 𝑝 ∈ 𝐿0 and 𝜋 ∈ Π0 . The symbols skip and abort are called constant programs. The
operators ;, ∪, and ? are called sequential composition, non-deterministic choice, and test,
respectively.
The syntax of BDQL is exactly the same as that of Propositional Dynamic Logic (PDL) [2]
without the Kleene star operator * . It is not strange that two different logics have the same
syntax. For example, Classical Logic and Intuitionistic Logic have the same syntax but are
distinguished by their semantics (or their sets of provable formulas). Similarly, the semantics
of BDQL and that of the star-free fragment of PDL are different. This paper considers only
star-free regular programs, leaving the addition of * to the logic in a future paper.

37

We define the semantics of BDQL using frames and models as usual. This kind of semantics
is called Kripke (or relational) semantics.
• A quantum dynamic frame is a pair 𝐹 = (ℋ, 𝑣) that consists of a Hilbert space ℋ anda function 𝑣 from Π0 to the set 𝒰(ℋ) of all unitary operators on ℋ. The function 𝑣 iscalled an interpretation for atomic programs.
• A quantum dynamic model is a triple 𝑀 = (ℋ, 𝑣, 𝑉 ) that consists of a quantum dynamic
frame (ℋ, 𝑣) and a function 𝑉 from 𝐿0 to the set 𝒞(ℋ) of all closed subspaces of ℋ. The
function 𝑉 is called an interpretation for atomic formulas.
The definition of quantum dynamic models states that atomic formulas are interpreted asa closed subspace of a Hilbert space. This interpretation is known as the algebraic semantics
for Quantum Logic [16]. The set 𝒞(ℋ) is called a Hilbert lattice [17] because it forms a latticewith meet 𝑋 ∩ 𝑌 and join 𝑋 ⊔ 𝑌 = (𝑋 ⊥ ∩ 𝑌 ⊥ )⊥ for any 𝑋, 𝑌 ∈ 𝒞(ℋ), where ⊥ denotes theorthogonal complement. Note that 𝑋 ⊔ 𝑌 ⊇ 𝑋 ∪ 𝑌 and 𝑋 ∪ 𝑌 ∈/ 𝒞(ℋ) in general.
Remark 2.1. Usually, Kripke frames are defined as a pair (tuple) that consists of a non-empty
set 𝑆 and relation(s) 𝑅 on 𝑆. On the other hand, the quantum dynamic frames defined above
have no relation(s). However, the relations can be recovered immediately using 𝑣. That is, thefamily {𝑅𝜋 : 𝜋 ∈ Π0 } of relations on ℋ is constructed by
𝑅𝜋 = {(𝑠, 𝑡) : (𝑣(𝜋))(𝑠) = 𝑡}
for each 𝜋 ∈ Π0 . For this reason, we use the word “frame” for quantum dynamic frames.
The interpretation 𝑣 is defined for atomic programs, and 𝑉 is defined for atomic formulas. These interpretations are extended to that for star-free regular programs and formulas,respectively. For any quantum dynamic model 𝑀 , the function [[ ]]𝑀 : 𝐿 → 𝒞(ℋ) and family{𝑅𝑎𝑀 : 𝑎 ∈ Π} of relations on ℋ are defined by simultaneous induction as follows:
1. [[𝑝]]𝑀 = 𝑉 (𝑝);2. [[¬𝐴]]𝑀 is the orthogonal complement of [[𝐴]]𝑀 ;3. [[𝐴 ∧ 𝐵]]𝑀 = [[𝐴]]𝑀 ∩ [[𝐵]]𝑀 ;4. [[[𝑎]𝐴]]𝑀 = {𝑠 ∈ ℋ : (𝑠, 𝑡) ∈ 𝑅𝑎𝑀 implies 𝑡 ∈ [[𝐴]]𝑀 for any 𝑡 ∈ ℋ};
𝑀
5. 𝑅skip= {(𝑠, 𝑡) : 𝑠 = 𝑡};
𝑀
6. 𝑅abort= ∅;7. 𝑅𝜋𝑀 = {(𝑠, 𝑡) : (𝑣(𝜋))(𝑠) = 𝑡};
𝑀 = {(𝑠, 𝑡) : (𝑠, 𝑢) ∈ 𝑅𝑀 and (𝑢, 𝑡) ∈ 𝑅𝑀 for some 𝑢 ∈ ℋ};
8. 𝑅𝑎;𝑏𝑎𝑏
𝑀 = 𝑅𝑀 ∪ 𝑅𝑀 ;9. 𝑅𝑎∪𝑏𝑎𝑏
𝑀 = {(𝑠, 𝑡) : 𝑃
𝑀
10. 𝑅𝐴?
[[𝐴]]𝑀 (𝑠) = 𝑡}, where 𝑃[[𝐴]]𝑀 stands for the projection onto [[𝐴]] .

Theorem 2.1. [[ ]]𝑀 is well-defined. That is, [[𝐴]]𝑀 ∈ 𝒞(ℋ) for each 𝐴 ∈ 𝐿.
Proof. See our proof in [4].

38The function [[ ]]𝑀 and family {𝑅𝑎𝑀 : 𝑎 ∈ Π} are uniquely determined if 𝑀 is given. Recall
that 𝑣(𝜋) is a function. On the other hand, 𝑅𝑎𝑀 is a relation and may not be a function due to ∪.
Now we can understand the meaning of each program: skip does nothing, abort forces
to halt without executing subsequent programs, ; is the composition operator, ∪ is the nondeterministic choice operator, and ? is the quantum test operator and is used to represent a
result of projective measurement (see Section 4.1).
Henceforth, we write (𝑀, 𝑠) |= 𝐴 for the condition 𝑠 ∈ [[𝐴]]𝑀 as usual. That is, (𝑀, 𝑠) |= 𝐴
if and only if 𝑃[[𝐴]]𝑀 (𝑠) = 𝑠. A formula 𝐴 is said to be satisfiable (resp. valid) if (𝑀, 𝑠) |= 𝐴 forsome (resp. any) 𝑀 and 𝑠 ∈ ℋ.
Remark 2.2. In most modal logics, a contradiction 𝐴 ∧ ¬𝐴 is not satisfiable. In other words,
not (𝑀, 𝑠) |= 𝐴 ∧ ¬𝐴 for any 𝑠. On the other hand, 𝐴 ∧ ¬𝐴 is satisfiable in BDQL because(𝑀, 0) |= 𝐴 ∧ ¬𝐴, where 0 stands for the origin (zero vector) of ℋ. LQP [18] chooses different
semantics from that in this paper to avoid this. That is, 0 (or the corresponding subspace {0})is not a state in the semantics of LQP. Unlike LQP, we allow 0 to be a state; otherwise, ourdefinition is ill-defined (Theorem 2.1 does not hold).
The following theorem gives the theoretical background for rewriting the statement of theform (𝑀, 𝑠) |= 𝐴 in our implementation explained in Section 4 of our previous work [4].
Theorem 2.2. The following holds for any 𝑀 and 𝑠 ∈ ℋ.
1. (𝑀, 𝑠) |= 𝐴 ∧ 𝐵, if and only if (𝑀, 𝑠) |= 𝐴 and (𝑀, 𝑠) |= 𝐵.
2. (𝑀, 𝑠) |= [skip]𝐴 if and only if (𝑀, 𝑠) |= 𝐴.
3. (𝑀, 𝑠) |= [abort]𝐴.
4. (𝑀, 𝑠) |= [𝜋]𝐴 if and only if (𝑀, (𝑣(𝜋))(𝑠)) |= 𝐴.
5. (𝑀, 𝑠) |= [𝑎 ; 𝑏]𝐴 if and only if (𝑀, 𝑠) |= [𝑎][𝑏]𝐴.
6. (𝑀, 𝑠) |= [𝑎 ∪ 𝑏]𝐴 if and only if (𝑀, 𝑠) |= [𝑎]𝐴 ∧ [𝑏]𝐴.
7. (𝑀, 𝑠) |= [𝐴?]𝐵 if and only if (𝑀, 𝑃[[𝐴]]𝑀 (𝑠)) |= 𝐵.
Proof. Straightforward.

3. Probabilistic Dynamic Quantum Logic
In general, the outcome of a projective measurement is not determined in advance because
there is a probability associated with each outcome. To capture this probabilistic ingredient,
we employ a probabilistic operator P≥𝑟 from [3] to formulate Probabilistic Dynamic Quantum
Logic (PDQL) as follows:
𝐿 ∋ 𝐴 :: = 𝑝 | ¬𝐴 | 𝐴 ∧ 𝐴 | [𝑎]𝐴 | P≥𝑟 𝐴,
Π ∋ 𝑎 :: = skip | abort | 𝜋 | 𝑎 ; 𝑎 | 𝑎 ∪ 𝑎 | 𝐴?,
where 𝑟 denotes a rational number in the closed interval [0, 1]. The expression P≥𝑟 𝐴 meansthat a projective measurement of 𝐴 on the current state of a quantum system will succeed withprobability ≥ 𝑟.

39

We can also use the probabilistic formula inside the dynamic modality for quantum tests asfollows:[𝐴?≥𝑟 ]𝐵 ≜ P≥𝑟 𝐴 ∧ [𝐴?]𝐵,
This means that if the quantum test 𝐴? (or the projective measurement of 𝐴) succeeds withprobability ≥ 𝑟, then 𝐵 will be the case after the successful execution of the quantum test.
Similarly, we can define other probabilistic operators P>𝑟 , P≤𝑟 , P<𝑟 , P=𝑟 , and P̸=𝑟 . Regarding the binary projective measurement of 𝐴, we have the following axioms:P≥𝑟 𝐴 → P≤𝑟 ¬𝐴,

P>𝑟 𝐴 → P<𝑟 ¬𝐴,

P≤𝑟 𝐴 → P≥(1−𝑟) ¬𝐴,

P<𝑟 𝐴 → P>𝑟 ¬𝐴,

P=𝑟 𝐴 → P=(1−𝑟) 𝐴,P̸=𝑟 𝐴 → P̸=(1−𝑟) .

Notice that these axioms only hold for the binary projective measurement of 𝐴.
The function [[ ]]𝑀 : 𝐿 → 𝒞(ℋ) is extended to handle the probabilistic operator P≥𝑟 using
the Born rule as follows:⟨ ⃒⟩⃒𝑠 ∈ [[P≥𝑟 𝐴]]𝑀 if and only if 𝑠⃒𝑃[[𝐴]]𝑀 (𝑠) ≥ 𝑟,
where 𝑃[[𝐴]]𝑀 (𝑠) is the projection of the current state 𝑠 on the closed linear subspace spanned by[[𝐴]]𝑀 , and ⟨𝑠|𝑠′ ⟩ is the inner product of two vectors representing two states 𝑠 and 𝑠′ , respectively.
Therefore, we write (𝑀, 𝑠) |= P≥𝑟 𝐴 if and only if 𝑠 ∈ [[P≥𝑟 𝐴]]𝑀 as usual.
The following theorem gives the theoretical background for rewriting the statement involving
the probabilistic operator for quantum tests.
Theorem 3.1. The following holds for any 𝑀 , 𝑠 ∈ ℋ, and 𝑟 ∈ [0, 1].
1. (𝑀, 𝑠) |= [𝐴?≥𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P≥𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
2. (𝑀, 𝑠) |= [𝐴?>𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P>𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
3. (𝑀, 𝑠) |= [𝐴?≤𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P≤𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
4. (𝑀, 𝑠) |= [𝐴?<𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P<𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
5. (𝑀, 𝑠) |= [𝐴?=𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P=𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
6. (𝑀, 𝑠) |= [𝐴?̸=𝑟 ]𝐵, if and only if (𝑀, 𝑠) |= P̸=𝑟 𝐴 and (𝑀, 𝑠) |= [𝐴?]𝐵.
Proof. Straightforward.

4. Application to Probabilistic Quantum Program Verification
This section describes the behavior and desired properties of some specific quantum programsin the language of PDQL. These properties can be verified automatically using our support tool
as shown in Sections 5 and 6.

40

4.1. Basic Notions
In the beginning, we briefly review quantum computation and fix our notation. We assume thereaders have basic knowledge of linear algebra.
Generally speaking, quantum systems are formulated as complex Hilbert spaces. However, forquantum computation, it is enough to consider specific Hilbert spaces called qubit systems. An𝑛𝑛-qubit system is the complex 2𝑛 -space C2 , where C stands for the complex plane. Pure states𝑛𝑛in the 𝑛-qubit system C2 are unit vectors in C2 . The orthogonal basis called computational
basis in the one-qubit system C2 is a set {|0⟩ , |1⟩} that consists of the column vectors |0⟩ =(1, 0)𝑇 and |1⟩ = (0,√1)𝑇 , where 𝑇 denotes the transpose
operator. The linear combinations√|+⟩ = (|0⟩ + |1⟩)/ 2 and |−⟩ = (|0⟩ − |1⟩)/ 2 of |0⟩ and |1⟩ are also pure states. In
general, |𝜓⟩ = 𝑐0 |0⟩ + 𝑐1 |1⟩ represents a pure state in the one-qubit system C2 provided that|𝑐0 |2 + |𝑐1 |2 = 1. This notation of vectors is called bra-ket notation (also called Dirac notation).
|𝜓⟩ is called a ket vector. The bra vector ⟨𝜓| is defined as a row vector whose elements arecomplex conjugates of the elements of the corresponding ket vector |𝜓⟩. In the two-qubit system
C4 , there are pure states that cannot be represented in the form |𝜓1 ⟩ ⊗ |𝜓2 ⟩ and are called
entangled states, where ⊗ denotes the tensor product (more precisely, the Kronecker √product).
For example, the EPR state (Einstein-Podolsky-Rosen state) |EPR⟩ = (|00⟩ + |11⟩)/ 2 is anentangled state, where |00⟩ = |0⟩ ⊗ |0⟩ and |11⟩ = |1⟩ ⊗ |1⟩.
Quantum computation is represented by unitary operators (also called quantum gates). There
are various quantum gates. For example, the Hadamard gate 𝐻 and Pauli gates 𝑋, 𝑌 , and 𝑍
are typical quantum gates on the one-qubit system C2 and are defined as follows:
)︃
)︃
)︃
)︃
(︃
(︃
(︃
(︃
0 1
0 −𝑖
1 0
1 1 1
, 𝑋=
, 𝑌 =
, 𝑍=
.
𝐻=√
2 1 −11 0
𝑖 0
0 −1
Two typical quantum gates on the two-qubit system C4 are the controlled-X gate (also called
the controlled NOT gate) CX and the swap gate SWAP are defined by
CX = |0⟩⟨0| ⊗ 𝐼 + |1⟩⟨1| ⊗ 𝑋,
SWAP = CX(𝐼 ⊗ |0⟩⟨0| + 𝑋 ⊗ |1⟩⟨1|)CX,
where 𝐼 denotes the identity matrix of size 2 × 2. Measurement is a completely different processfrom applying quantum gates. Here we roughly explain specific projective measurements.
For the general definition of projective measurement, see [19]. Observe that 𝑃0 = |0⟩⟨0| and𝑃1 = |1⟩⟨1| are projections, respectively. After executing the measurement {𝑃0 , 𝑃1 }, a current
state |𝜓⟩ = 𝑐0 |0⟩ + 𝑐1 |1⟩ is transitioned into 𝑃0 |𝜓⟩ /|𝑐0 | = 𝑐0 |0⟩ /|𝑐0 | with probability |𝑐0 |2
and into 𝑃1 |𝜓⟩ /|𝑐1 | = 𝑐1 |1⟩ /|𝑐1 | with probability |𝑐1 |2 .

4.2. Standard Interpretation
To describe the quantum programs discussed in this paper, we fix
Π0 = {H(𝑖), X(𝑖), Y(𝑖), Z(𝑖), CX(𝑖, 𝑗), SWAP(𝑖, 𝑗) : 𝑖, 𝑗 ∈ N, 𝑖 ̸= 𝑗},
𝐿0 = {𝑝(𝑖, |𝜓⟩), 𝑝(𝑖, 𝑖 + 1, |Ψ⟩) : 𝑖 ∈ N, |𝜓⟩ ∈ C2 , |Ψ⟩ ∈ C4 },41

where N stands for the set of all natural numbers (including 0). Because now atomic programs
and atomic formulas are restricted, we only need to consider specific interpretations called thestandard interpretations 𝑣¯ and 𝑉 instead of 𝑣 and 𝑉 , respectively. The standard interpretations
are defined below.
𝑛𝑛
A function 𝑣¯ : Π0 → 𝒰(C2 ) is called the standard interpretation on C2 for atomic programsif𝑣¯(H(𝑖)) = 𝐼 ⊗𝑖 ⊗ 𝐻 ⊗ 𝐼 ⊗𝑛−𝑖−1 ,𝑣¯(X(𝑖)) = 𝐼 ⊗𝑖 ⊗ 𝑋 ⊗ 𝐼 ⊗𝑛−𝑖−1 ,𝑣¯(Y(𝑖)) = 𝐼 ⊗𝑖 ⊗ 𝑌 ⊗ 𝐼 ⊗𝑛−𝑖−1 ,𝑣¯(Z(𝑖)) = 𝐼 ⊗𝑖 ⊗ 𝑍 ⊗ 𝐼 ⊗𝑛−𝑖−1 ,𝑣¯(CX(𝑖, 𝑗)) = 𝐼 ⊗𝑖 ⊗ |0⟩⟨0| ⊗ 𝐼 ⊗𝑛−𝑖−1 + (𝐼 ⊗𝑖 ⊗ |1⟩⟨1| ⊗ 𝐼 ⊗𝑛−𝑖−1 )(𝐼 ⊗𝑗 ⊗ 𝑋 ⊗ 𝐼 ⊗𝑛−𝑗−1 ),𝑣¯(SWAP(𝑖, 𝑗)) = 𝑣¯(CX(𝑖, 𝑗) ; CX(𝑗, 𝑖) ; CX(𝑖, 𝑗)),
where

𝑖

𝐼

⊗𝑖

⏞
⏟
= 𝐼 ⊗ ··· ⊗ 𝐼 .

That is, under the standard interpretation, H(𝑖), X(𝑖), Y(𝑖), Z(𝑖) execute the corresponding
quantum gate on the 𝑖-th qubit, CX(𝑖, 𝑗) executes the Pauli gate 𝑋 on the target qubit (𝑗-thqubit) depending on the state of the control qubit (𝑖-th qubit), and SWAP(𝑖, 𝑗) swaps the 𝑖-thand 𝑗-th qubits.
𝑛
A functionato is called the standard interpretation on C2 for atomic formulas if
𝑖

𝑛−𝑖−1

2𝑖

2𝑛−𝑖−2𝑉 (𝑝(𝑖, |𝜓⟩)) = C2 ⊗ span{|𝜓⟩} ⊗ C2
𝑉 (𝑝(𝑖, 𝑖 + 1, |Ψ⟩)) = C ⊗ span{|Ψ⟩} ⊗ C,,

where span{|𝜓⟩} (resp. span{|Ψ⟩}) stands for the subspace spanned by {|𝜓⟩} (resp. {|Ψ⟩}).
𝑛
In what follows, we write 𝑀 𝑛 for (C2 , 𝑣¯, 𝑉 ), where the index 𝑛 represents the numberof qubits. In addition, we use the following abbreviation to conventionally describe quantum
programs for quantum tests with probability in PDQL:
if P≥𝑟 𝐴 then 𝑎 else 𝑏 fi = (𝐴?≥𝑟 ; 𝑎) ∪ (¬𝐴?≤(1−𝑟) ; 𝑏).
This program means the selection depends on the outcomes of projective measurement withrespect to the probabilities. That is, execute 𝑎 or 𝑏 depending on the result of the measurement{𝑃[[𝐴]]𝑀 , 𝑃[[¬𝐴]]𝑀 } with respect to P≥𝑟 𝐴 and P≤(1−𝑟) ¬𝐴.

4.3. Case Studies
In the sequel, we use PDQL to verify some case studies involving probability, which intentionallyis added to the formalizations of quantum programs to demonstrate the expressiveness of
PDQL. For the sake of brevity, this section only describes some quantum programs, including
Quantum Relay Scheme [11], Bidirectional Quantum Teleportation [12], Two-qubit Quantum
Teleportation [14], and Quantum Network Coding [15]. Meanwhile, other quantum programs,
including Superdense Coding [7], Quantum Teleportation [8], Quantum Secret Sharing [9],Entanglement Swapping [10], and Quantum Gate Teleportation [13], can be derived in a similar
way. The reader interested in them is referred to our previous work [4] for their description
without probability.

42

Alice: |𝜓⟩
Alice: |0⟩

𝐻
𝐻Charlie: |0⟩Charlie: |0⟩

𝑋

𝑍

𝐻

𝐻

Bob: |0⟩

𝑋

𝑍

|𝜓⟩

Figure 1: Quantum Relay Scheme

Quantum Relay Scheme
Quantum Relay Scheme [11] allows us to teleport a quantum state from one quantum device
to another wirelessly even though these two devices do not share EPR pairs mutually, which
differs from Quantum Teleportation [8]. The quantum circuit of Quantum Relay Scheme isdepicted in Figure 1. The program of Quantum Relay Scheme with probability intentionallyadded is described as follows:
relay = H(1) ; CX(1, 2) ; H(3) ; CX(3, 4) ; CX(0, 1) ; H(0); if 𝑝(1, |0⟩)≥1/2 then skip else X(2) fi; if 𝑝(0, |0⟩)≥1/2 then skip else Z(2) fi; CX(2, 3) ; H(2); if 𝑝(3, |0⟩)≥1/2 then skip else X(4) fi; if 𝑝(2, |0⟩)≥1/2 then skip else Z(4) fi.
The desired property of Quantum Relay Scheme is that “a pure state |𝜓⟩ is correctly teleported.”
In PDQL, this property is expressed as follows:(𝑀 5 , |𝜓⟩ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩) |= [relay]𝑝(4, |𝜓⟩).

Bidirectional Quantum Teleportation
Bidirectional Quantum Teleportation [12] is based on EPR pairs and entanglement swapping
to allow two users to simultaneously transmit an unknown single qubit to each other. The
quantum circuit of Bidirectional Quantum Teleportation is depicted in Figure 2. The programof Bidirectional Quantum Teleportation with probability intentionally added is described asfollows:biTeleport = H(2) ; CX(2, 3) ; H(4) ; CX(4, 5) ; CX(0, 2) ; CX(1, 5) ; H(0) ; H(1); if 𝑝(2, |0⟩)≥1/2 then skip else X(3) fi; if 𝑝(0, |0⟩)≥1/2 then skip else Z(3) fi; if 𝑝(5, |0⟩)≥1/2 then skip else X(4) fi

43Alice: |𝜓⟩𝐻

Bob: |𝜓 ′ ⟩𝐻

Alice: |0⟩𝐻

Bob: |0⟩
Alice: |0⟩

𝑋
𝐻

|𝜓⟩

𝑍
𝑋

𝑍

|𝜓 ′ ⟩

Bob: |0⟩
Figure 2: Bidirectional Quantum Teleportation
𝐻
Alice: |Ψ⟩𝐻
Alice: |0⟩

𝐻

Alice: |0⟩𝐻

Bob: |0⟩𝑋

Bob: |0⟩

𝑋

𝑍

|Ψ⟩

𝑍

Figure 3: Two-qubit Quantum Teleportation; if 𝑝(1, |0⟩)≥1/2 then skip else Z(4) fi.
The desired property of Bidirectional Quantum Teleportation is that “two pure states |𝜓⟩and |𝜓 ′ ⟩ owned by two users are correctly teleported to each other.” In PDQL, this property isexpressed as follows:
⃒ ⟩︀
⃒ ⟩︀
(𝑀 6 , |𝜓⟩ ⊗ ⃒𝜓 ′ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩) |= [biTeleport]𝑝(3, |𝜓⟩) ∧ 𝑝(4, ⃒𝜓 ′ ).

Two-qubit Quantum Teleportation
Two-qubit Quantum Teleportation [14] allows us to teleport an arbitrary two-qubit pure states|Ψ⟩ = 𝑐00 |00⟩+𝑐01 |01⟩+𝑐10 |10⟩+𝑐11 |11⟩ from one source to another, where |𝑐00 |2 +|𝑐01 |2 +|𝑐10 |2 + |𝑐11 |2 = 1. The quantum circuit of Two-qubit Quantum Teleportation is depicted in
Figure 3. The program of Two-qubit Quantum Teleportation with probability intentionallyadded is described as follows:
twoTeleport = H(2) ; H(3) ; CX(2, 4) ; CX(3, 5) ; CX(0, 2) ; CX(1, 3) ; H(0) ; H(1); if 𝑝(3, |0⟩)≥1/2 then skip else X(5) fi; if 𝑝(2, |0⟩)≥1/2 then skip else X(4) fi; if 𝑝(1, |0⟩)≥1/2 then skip else Z(5) fi

44

; if 𝑝(0, |0⟩)≥1/2 then skip else Z(4) fi.
The desired property of Two-qubit Quantum Teleportation is that “arbitrary two-qubit purestates |Ψ⟩ is correctly teleported.” In PDQL, this property is expressed as follows:(𝑀 6 , |Ψ⟩ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩ ⊗ |0⟩) |= [twoTeleport]𝑝(4, 5, |Ψ⟩).

Quantum Network Coding
Quantum Network Coding [15] enables the simultaneous generation of EPR pairs by using only
local operations and classical communication (LOCC) and the sharing of EPR pairs between
adjacent quantum repeaters. Simultaneous quantum communication can be achieved by using
Teleportation with these EPR states. This facilitates the transmission of quantum informationon complex networks at higher rates than straightforward routing strategies, such as the simple
entanglement swapping strategy. For the sake of simplicity, we do not depict the quantum
circuit of Quantum Network Coding here, while the reader is referred to their original paper [15].
The protocol introduces two new techniques called “Connection” and “Removal” to manipulateentangled states and systematize the methods of encoding, which are described as follows:con(𝑁 1, (𝑁 2 → 𝑁 3)) = CX(𝑁 1, 𝑁 2)
; if 𝑝(𝑁 2, |0⟩)≥1/2 then skip else X(𝑁 3) fi.
fanout(𝑁 1, (𝑁 2 → 𝑁 3), (𝑁 4 → 𝑁 5)) = con(𝑁 1, (𝑁 2 → 𝑁 3)) ; con(𝑁 1, (𝑁 4 → 𝑁 5)).
add(𝑁 1, 𝑁 2, (𝑁 3 → 𝑁 4)) = CX(𝑁 1, 𝑁 3) ; CX(𝑁 2, 𝑁 3)
; if 𝑝(𝑁 3, |0⟩)≥1/2 then skip else X(𝑁 4) fi.
rem(𝑁 1 → 𝑁 2) = H(𝑁 1); if 𝑝(𝑁 1, |0⟩)≥1/2 then skip else Z(𝑁 2) fi.
remadd(𝑁 3 → (𝑁 1, 𝑁 2)) = H(𝑁 3); if 𝑝(𝑁 3, |0⟩)≥1/2 then skip
else Z(𝑁 1) ; Z(𝑁 2) fi .
where 𝑁 1, 𝑁 2, 𝑁 3, and 𝑁 4 are natural numbers in the range [0, 9]. Then, the program of
Quantum Network Coding with probability intentionally added is described via con, fanout,add, rem, and remadd as follows:
networkcoding = H(0) ; CX(0, 1) ; H(2) ; CX(2, 3); H(4) ; CX(4, 5) ; H(6) ; CX(6, 7); H(8) ; CX(8, 9) ; H(10) ; CX(10, 11); H(12) ; CX(12, 13); con(0, (2 → 3) ; con(4, (6 → 7)) ; add(3, 7, (8 → 9)); fanout(9, (10 → 11), (12 → 13)) ; CX(13, 5) ; CX(11, 1); rem(11 → 9) ; rem(13 → 9) ; remadd(9 → (3, 7))45

; rem(3 → 0) ; rem(7 → 4)
; SWAP(2, 4) ; SWAP(0, 4).
The desired property of Quantum Network Coding is that “the two EPR states (in this case
|EPR⟩) are simultaneously generated.” In PDQL, this property is expressed as follows:(𝑀 14 , |0⟩⊗14 ) |= [networkcoding]𝑝(1, 2, |EPR⟩) ∧ 𝑝(4, 5, |EPR⟩).

5. Implementation of Probabilistic Dynamic Quantum Logic
This section describes the implementation of PDQL in Maude [5], a specification/programming
language based on rewriting logic [20]. Hence, the notations used in this section follow the
Maude syntax.

5.1. Syntax of Probabilistic Dynamic Quantum Logic
Recalling the syntax of Basic Dynamic Quantum Logic (BDQL) in our previous work [4], we
defined two sorts AtomicProg and Prog for atomic programs Π0 and star-free regular programs
Π, respectively, where AtomicProg is a subsort of Prog. Additionally, we defined several
operators for atomic programs: I(_), H(_), X(_), Y(_), and Z(_). These operators take anatural number as input, denoting the index of a qubit of a pure state on which the quantum
gates 𝐼, 𝐻, 𝑋, 𝑌 , and 𝑍, will be applied, respectively. Furthermore, CX(_,_) and SWAP(_,_)
operators take two natural numbers as inputs, denoting the indices of two qubits of a pure stateon which CX and SWAP gates will be applied. We also defined abort, skip, _;_ , _U_, and_? operators to construct star-free regular programs in BDQL, as specified in Section 2.
We defined two sorts AtomicFormula and Formula for atomic formulas 𝐿0 and generalformulas 𝐿 in BDQL, respectively, where AtomicFormula is a subsort of Formula. Additionally, we defined several operators for constructing formulas in BDQL: P(_,_) and P(_,_,_)
operators are atomic formulas representing projections of the forms 𝑝(𝑖, |𝜓⟩) and 𝑝(𝑖, 𝑗, |Ψ⟩), respectively; and the neg_, _/\_, and [_]_ operators to construct formulas in BDQL, as specified
in Section 2. Moreover, the if_then_else_fi command in Section 4.2 was also implemented
for convenient use.
Regarding the syntax of Probabilistic Dynamic Quantum Logic (PDQL), we extend the syntax
of BDQL by introducing the probabilistic operator as follows:
op _with prob >=_: Formula Scalar -> Formula [ctor] .

op _with prob >_: Formula Scalar -> Formula [ctor] .

op _with prob <=_: Formula Scalar -> Formula [ctor] .

op _with prob <_: Formula Scalar -> Formula [ctor] .

op _with prob ==_: Formula Scalar -> Formula [ctor] .

op _with prob =/=_ : Formula Scalar -> Formula [ctor] .

where the five operators above explicitly denote the probabilistic operators P≥𝑟 𝐴, P>𝑟 𝐴,
P≤𝑟 𝐴, P<𝑟 𝐴, P=𝑟 𝐴, P̸=𝑟 𝐴, respectively, and 𝑟 is a rational number ∈ [0, 1]. However, we
define 𝑟 as belonging to a sort of Scalar in our formalization because we also want to reason on
symbolic complex constants included in the value of probability.

46

5.2. Semantics of Probabilistic Dynamic Quantum Logic
We extend the semantics of BDQL to describe the semantics of PDQL by introducing thefollowing equations, which strictly follow Theorem 3.1. For the sake of simplicity, we only
describe equations used for _with prob >=_ operator representing the probabilistic operatorP≥𝑟 𝐴, while other operators are similar.
We define some Maude variables before use as follows: Q is a Maude variable of quantum
states, Phi is a Maude variable of formulas, Prob is a Maude variable of scalars, M is a Maude
variable of matrices, and N, N1, and N2 is Maude variables of natural numbers.
We first handle the probabilistic operator in a formula as follows:
ceq Q |= P(N, M) with prob >= Prob = emptyJS if (Q).Prob(N, M) .>= Prob .
ceq Q |= P(N1, N2, M) with prob >= Prob = emptyJS if (Q).Prob(N1, N2, M) .>= Prob.

where emptyJS denote success in checking and .>= operator denotes “greater than or equalto” when comparing two complex numbers.
We then handle the probabilistic operator in the dynamic modality as follows:
ceq Q |= [(P(N, M) with prob >= Prob)?] Phi = Q |= [P(N, M)?] Phi
if (Q).Prob(N, M) .>= Prob .

With respect to the equations specified in our support tool, (𝑀, 𝑠) |= 𝐴 if s |= A is simplified
to emptyJS. Otherwise, (𝑀, 𝑠) ̸|= 𝐴 if s |= A is not simplified to emptyJS.

6. Experimental Results
In this section, we illustrate the application of our support tool for verifying Quantum Relay
Scheme in Maude, using it as an example. Similar procedures can be done for verifying otherquantum programs, which are publicly available at https://github.com/canhminhdo/DQL. Following that, we summarize the experimental results for several quantum programs employed inour experiments, including Superdense Coding [7], Quantum Teleportation [8], Quantum Secret
Sharing [9], Entanglement Swapping [10], Quantum Relay Scheme [11], Bidirectional Quantum
Teleportation [12], Two-qubit Quantum Teleportation [14], Quantum Gate Teleportation [13],and Quantum Network Coding [15].
Assuming that RELAY-SCHEME represents the specification of Quantum Relay Scheme,
initQState represents for the initial state for RELAY-SCHEME, and qubitAt denotes thefunction to retrieve a single qubit at a specific index. We can verify the correctness of Quantum
Relay Scheme using our support tool by executing the following reduce command in Maude:
red in RELAY-SCHEME : initQState |= [H(1) ; CX(1, 2) ; H(3) ; CX(3, 4) ; CX(0, 1) ; H(0) ;if P(1, |0>) with prob >= 1/2 then skip else X(2) fi ;if P(0, |0>) with prob >= 1/2

then skip else Z(2) fi ;CX(2, 3) ; H(2) ;if P(3, |0>) with prob >= 1/2

then skip else X(4) fi ;if P(2, |0>) with prob >= 1/2

then skip else Z(4) fi] P(4, qubitAt(initQState, 0)) .

47

Table 1
Experimental results with our support tool for several quantum programs in PDQL
Protocol

QubitsRewrite Steps

Verification Time

Superdense Coding

2

2,451

1ms

Quantum Teleportation

3

9,034

4ms

Quantum Secret Sharing

439,041

18ms

Entanglement Swapping

4

14,2726ms

Quantum Relay Scheme

544,93926ms

Bidirectional Quantum Teleportation

6

47,71727ms

Two-qubit Quantum Teleportation

6660,313

238ms

Quantum Gate Teleportation

6

667,806

250ms

Quantum Network Coding

14

11,568,281

4,811ms

The reduce command automatically performs an equational simplification process based on
the equations defined in our tool. Within just a few moments, the command returns an emptyJS
result. Consequently, this confirms the correctness of Quantum Relay Scheme with probability
intentionally added by using our support tool, the implementation of PDQL in Maude. The
property being verified informally says that the first qubit of the initial quantum state at index
0 is correctly teleported to the fifth qubit at index 4 in the final quantum state.
We conducted experiments on an iMac equipped with a 4 GHz microprocessor with eightcores and 32 GB memory of RAM. Table 1 presents the experimental results. We have successfully confirmed the correctness of Superdense Coding [7], Quantum Teleportation [8], Quantum
Secret Sharing [9], Entanglement Swapping [10], Quantum Relay Scheme [11], Bidirectional
Quantum Teleportation [12], Quantum Gate Teleportation [13], Two-qubit Quantum Teleportation [14], and Quantum Network Coding [15] in accordance with the specified properties
outlined in Section 4. Comparing to our previous work [4], we extend our case studies by adding
additional quantum programs to be verified with and without the probability. For all case studies
from two to 14 qubits, we can quickly verify their correctness within just a few moments using
our support tool despite the considerable number of rewrite steps involved. These results would
have been extremely challenging to obtain without the assistance of computer programs likeour support tool, especially in the case of Quantum Network Coding. This shows the usefulnessof our automated approach for verifying quantum programs in PDQL, employing the symbolic
approach for quantum computation from [6].

48

7. Related Work
Quantum Hoare Logic (QHL), as introduced by M. Ying in his work [21], was conceived with theaim of serving as a quantum counterpart to Hoare Logic. When examining the logical aspects,
BDQL, in contrast to QHL, possesses the capability to express more foundational elements
within quantum programs. Specifically, QHL faces limitations when dealing with the if · · · fi
statement, which represents non-deterministic measurements, as it cannot be further divided.
In contrast, BDQL can explicitly express its non-deterministic characteristic by employing the
choice operator ∪. Additionally, it’s worth noting that QHL lacks the inclusion of a test operator
in its syntax and does not support probability in its formulas.
In our paper, we used Maude as our implementation language. In contrast, the work by [22]utilized PRISM, a probabilistic symbolic model checker, to verify quantum protocols. Unlike ourapproach, [22] requires the task of enumerating states and precomputing state transitions, which
are then encoded into a specification in PRISM. Conversely, our method doesn’t necessitate thisstate enumeration and precomputing state transitions because we formalize both the quantum
computation and the semantics of PDQL using equations. The verification problem is carriedout automatically through an equational simplification process within Maude. Moreover, they
only support a small number of qubits, saying less than five qubits. As demonstrated, we canverify Quantum Network Coding with 14 qubits within a few moments, demonstrating thescalability of our approach.

8. Conclusion
We have extended Basic Dynamic Quantum Logic (BDQL) to Probabilistic Dynamic Quantum
Logic (PDQL) to verify probabilistic quantum programs by introducing the probabilistic operatorP≥𝑟 and some others in the formulas of PDQL. We have also developed a support tool in Maude
to automate the entire verification process. Several quantum programs have been verified
automatically using the support tool, demonstrating the usefulness of PDQL and our support
tool. As one piece of our future work, we would like to conduct more case studies where theprobabilistic properties are realistically expressed, such as Quantum Search Algorithm andQuantum Leader Election Protocol.

Acknowledgments
The research was supported by JAIST Research Grant for Fundamental Research. The researchof the first author was supported by JSPS KAKENHI Grant Number JP23K19959. The researchof the first and the third authors was supported by JST SICORP Grant Number JPMJSC20C2.
The research of the second author was supported by Grant-in-Aid for JSPS Research Fellow
Grant Number JP22KJ1483.

49

References[1] P. Shor, Algorithms for quantum computation: discrete logarithms and factoring, in:Proceedings 35th Annual Symposium on Foundations of Computer Science, 1994, pp.
124–134. doi:10.1109/SFCS.1994.365700.
[2] D. Harel, D. Kozen, J. Tiuryn, Dynamic Logic, MIT Press, 2000.
[3] A. Baltag, S. Smets, Reasoning about quantum information: An overview of quantum
dynamic logic, Applied Sciences 12 (2022). URL: https://www.mdpi.com/2076-3417/12/9/
4458. doi:10.3390/app12094458.
[4] T. Takagi, C. M. Do, K. Ogata, Automated quantum program verification in a dynamic
quantum logic (to appear), in: DaLí: Dynamic Logic – New trends and applications, 2023.
[5] M. Clavel, et al., All About Maude, volume 4350 of Lecture Notes in Computer Science,
Springer, 2007. doi:10.1007/978-3-540-71999-1.
[6] C. M. Do, K. Ogata, Symbolic model checking quantum circuits in maude, in: The 35th
International Conference on Software Engineering and Knowledge Engineering, SEKE
2023, 2023, pp. 103–108. doi:10.18293/SEKE2023-014.
[7] C. H. Bennett, S. J. Wiesner, Communication via one- and two-particle operators on
Einstein-Podolsky-Rosen states, Phys. Rev. Lett. 69 (1992) 2881–2884. doi:10.1103/
PhysRevLett.69.2881.
[8] C. H. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres, W. K. Wootters, Teleporting an
unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels, Phys.
Rev. Lett. 70 (1993) 1895–1899. doi:10.1103/PhysRevLett.70.1895.
[9] M. Hillery, V. Bužek, A. Berthiaume, Quantum secret sharing, Phys. Rev. A 59 (1999)
1829–1834. doi:10.1103/PhysRevA.59.1829.
[10] M. Żukowski, A. Zeilinger, M. A. Horne, A. K. Ekert, “Event-ready-detectors” Bell experiment via entanglement swapping, Phys. Rev. Lett. 71 (1993) 4287–4290. doi:10.1103/
PhysRevLett.71.4287.
[11] S.-T. Cheng, C.-Y. Wang, M.-H. Tao, Quantum communication for wireless wide-area
networks, IEEE Journal on Selected Areas in Communications 23 (2005) 1424–1432.
doi:10.1109/JSAC.2005.851157.
[12] S. Hassanpour, M. Houshmand, Bidirectional quantum teleportation and secure directcommunication via entanglement swapping, 2014. doi:10.48550/arXiv.1411.0206.
arXiv:1411.0206.
[13] D. Gottesman, I. L. Chuang, Demonstrating the viability of universal quantum computation
using teleportation and single-qubit operations, Nature 402 (1999) 390–393. doi:10.1038/
46503.
[14] G. Rigolin, Quantum teleportation of an arbitrary two-qubit state and its relation tomultipartite entanglement, Phys. Rev. A 71 (2005) 032303. URL: https://link.aps.org/doi/10.
1103/PhysRevA.71.032303. doi:10.1103/PhysRevA.71.032303.
[15] T. Satoh, F. L. Gall, H. Imai, Quantum network coding for quantum repeaters, PhysicalReview A 86 (2012). doi:10.1103/physreva.86.032331.
[16] G. Birkhoff, J. von Neumann, The logic of quantum mechanics, Annals of mathematics 57(1936) 823–843. doi:10.2307/1968621.
[17] M. Rédei, Quantum logic in algebraic approach, volume 91 of Fundamental Theories of50

Physics, Springer, 1998. doi:10.1007/978-94-015-9026-6.
[18] A. Baltag, S. Smets, LQP: the dynamic logic of quantum information, Mathematicalstructures in computer science 16 (2006) 491–525. doi:10.1017/S0960129506005299.
[19] M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information: 10th
Anniversary Edition, Cambridge University Press, 2011.
[20] J. Meseguer, Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming 81 (2012) 721–781. doi:10.1016/j.jlap.2012.06.003.
[21] M. Ying, Floyd–hoare logic for quantum programs, ACM Transactions on Programming
Languages and Systems (TOPLAS) 33 (2012) 1–49. doi:10.1145/2049706.2049708.
[22] S. Gay, R. Nagarajan, N. Papanikolaou, Probabilistic model–checking of quantum protocols,arXiv preprint quant-ph/0504007 (2005). doi:10.48550/arXiv.quant-ph/0504007.

51

Symbolic Model Checking Quantum Circuits With
Density Operators in Maude
Canh Minh Do* , Kazuhiro Ogata
Japan Advanced Institute of Science and Technology, 1-8 Asahidai, Nomi, Japan

Abstract

We proposed a symbolic approach to model checking quantum circuits using a set of laws from quantum
mechanics and basic matrix operations with Dirac notation and used Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach. However,it only supports the formalization of pure states but not mixed states of quantum systems. This paper
extends our current symbolic approach to deal with mixed states of quantum systems by using density
operators for their representations. Once a quantum circuit is formalized by our proposed way with an
initial state and a desired property expressed in Linear Temporal Logic (LTL), we use a built-in Maude
LTL model checker to verify whether the quantum circuit enjoys the desired property from the initialstate automatically. As case studies, we successfully verify several quantum communication protocols:
Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, and Entanglement Swapping.

Keywords

Mixed States, Density Operators, Quantum circuits, Dirac notation, Symbolic Model Checking, Maude

1. Introduction
Quantum computing represents a new frontier in computation, offering the potential to solve
hard problems, which were previously considered intractable for the current computing technologies. For example, Shore’s fast algorithm [1] can break the security of modern cryptographic
systems relying on discrete logarithms and factoring in the future once practical quantum computers are available. To design and implement such quantum algorithms, quantum circuits
are often used as a model of quantum computation. Unlike classical circuits, quantum circuits
manipulate qubits using quantum operations (e.g., quantum gates). Because quantum computation is counter-intuitive and distinct from classical computing due to different principles, suchas superposition, entanglement, and measurement, it is challenging to design and implement
quantum algorithms (or quantum circuits) accurately. Therefore, it is crucial to verify thatquantum circuits enjoy some desired properties in preparing for the quantum era.
Our research group proposed a symbolic approach [2] to model checking quantum circuits
using a set of laws from quantum mechanics and basic matrix operations with Dirac notation [3]and used Maude [4], a high-level specification/programming language based on rewriting
The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, November 11, 2023, Brisbane, Australia*
Corresponding author.
$ canhdo@jaist.ac.jp (C. M. Do); ogata@jaist.ac.jp (K. Ogata) 0000-0002-1601-4584 (C. M. Do); 0000-0002-4441-3259 (K. Ogata)52

logic [5], to implement our symbolic approach. However, it only supports the formalization ofpure states but not mixed states of quantum systems. In many practical situations, a quantum
system is not a single, well-defined state but a statistical mixture of multiple pure states. Therefore, it requires the formalization of mixed states to describe the probabilities associated witheach pure state. This paper extends our current symbolic approach [2] to deal with mixed statesof quantum systems by using density operators for their representations. Once a quantum
circuit is formalized by our proposed way with an initial state and a desired property expressedin Linear Temporal Logic (LTL), we use the built-in Maude LTL model checker to automatically verify whether the quantum circuit enjoys the desired property from the initial state. Ascase studies, we successfully verify several quantum communication protocols: Superdense
Coding [6], Quantum Teleportation [7], Quantum Secret Sharing [8], and Entanglement Swapping [9]. This demonstrates the usefulness of our symbolic model checking quantum circuitswith density operators in Maude. The support tool and case studies are publicly available athttps://github.com/canhminhdo/QTC-Maude under the mixed-states folder.
The rest of the paper is organized as follows: Sect. 2 provides basic quantum mechanics,
symbolic reasoning for quantum computation based on Dirac notation, and Kripke structure;
Sect. 3 describes the formalization of qubits, quantum gates, and quantum circuits; Sect. 4
demonstrates how to use our approach to model checking for Quantum Teleportation; Sect. 5shows the experimental results with our support tool; Sect. 6 presents some existing work; andSect. 7 concludes the paper with some pieces of future work.

2. Preliminaries
Firstly, we describe some basic notations from quantum mechanics based on linear algebra(refer to [10] for more details). Secondly, we describe symbolic reasoning [2, 11] to reason
about quantum computation based on Dirac notation. Lastly, we describe Kripke structures toformalize quantum systems.

2.1. Basic Quantum Mechanics
In classical computing, the fundamental unit of information is a bit whose value is either 0
or 1. In quantum computing, the counterpart is a quantum bit or qubit, which has two basis
states, conventionally written in Dirac notation [3] as(︃ |0⟩)︃ and(︃|1⟩,)︃corresponding to one-bit
10classical values, whose values are two column vectors
and, respectively. In quantum
0
1
theory, a general state of a quantum system is a superposition or linear combination of basis
states. A single qubit has state |𝜓⟩ = 𝛼 |0⟩ + 𝛽 |1⟩, where 𝛼 and 𝛽 are complex numbers
such that|𝛼|2 + |𝛽|2 = 1. States can be represented by column complex vectors as follows:
(︃ )︃
𝛼
|𝜓⟩ =
= 𝛼 |0⟩ + 𝛽 |1⟩, where {|0⟩ , |1⟩} forms an orthonormal basis of the 2D complex𝛽vector space. Formally, a quantum state is a unit vector in a Hilbert space ℋ, which is equippedwith an inner product satisfying some axioms.

53

The basis {|0⟩ , |1⟩} is called as the standard basis. Besides, we have some other bases ofinterest, such as diagonal (or dual, or Hadamard) basis consisting of the following vectors:|+⟩ = √12 (|0⟩ + |1⟩) and |−⟩ = √12 (|0⟩ − |1⟩)
The evolution of a closed quantum system can be performed by a unitary transformation.
If the state of a qubit is represented by a column vector, then a unitary transformation 𝑈 can† = 𝑈 −1 , where
be represented by a complex-value matrix such that 𝑈 𝑈 † = 𝑈 † 𝑈 = 𝐼 or 𝑈∑︀†
𝑈 is the conjugate transpose of 𝑈 . The trace of 𝑈 is defined as 𝑡𝑟(𝑈 ) = 𝑖 ⟨𝜑𝑖 |𝑈 |𝜑𝑖 ⟩ forsome given orthonormal basis {|𝜑𝑖 ⟩} of ℋ. 𝑈 acts on the Hilbert space ℋ transforming a state|𝜓⟩ to a state |𝜓 ′ ⟩ by a matrix multiplication such that |𝜓 ′ ⟩ = 𝑈 |𝜓⟩. There are some common
quantum gates: the Hadamard gate 𝐻, the identity gate 𝐼, the Pauli gates 𝑋, 𝑌 , and 𝑍, and thecontrolled-NOT gate CX . Note that the CX gate performs on two qubits, while the remaining
gates perform on a single qubit. Their matrix representations are as follows:
I2 =

Z =

(︃
)︃
1 0
0 1
(︃
1

0

(︃
,

X =

0 1
1 0

)︃

0 −1

,

)︃

(︃
𝐻 = √12

1

,

1

)︃

1 −1

,

(︃
)︃
0 −𝑖
Y =
,
𝑖 0
⎛
1 0 0
⎜
⎜0 1 0⎜
CX = ⎜⎜0 0 0
⎝
0 0 1

⎞
0
⎟
0⎟
⎟
⎟.
1⎟
⎠
0

where 𝑖 is the imaginary unit. For example, the Hadamard gate on a single qubit performs the
mapping |0⟩ ↦→ √12 (|0⟩ + |1⟩) and |1⟩ ↦→ √12 (|0⟩ − |1⟩). The controlled-NOT gate on pairs ofqubits performs the mapping |00⟩ ↦→ |00⟩ , |01⟩ ↦→ |01⟩ , |10⟩ ↦→ |11⟩ , |11⟩ ↦→ |10⟩, which
can be understood as inverting the second qubit (referred to as the target) if and only if the first
qubit (referred to as the control) is one.
A quantum measurement is described as a collection {𝑀𝑚 } of measurement operators, where
the indicesto the measurement outcomes. It is required that the measurement operators∑︀ 𝑚 refer†satisfy 𝑚 𝑀𝑚 𝑀𝑚 = I ℋ . If the state of a quantum system is |𝜓⟩ before the measurement,
then the probability for the result 𝑚 is as follows:†𝑝(𝑚) = ⟨𝜓| 𝑀𝑚
𝑀𝑚 |𝜓⟩,√𝑚 |𝜓⟩ provided that 𝑝(𝑚) > 0.
and the state of the quantum system after the measurement is 𝑀𝑝(𝑚)For example, if a qubit is in state 𝛼 |0⟩ + 𝛽 |1⟩ and measuring with {𝑀0 , 𝑀1 } operators, wehave the result 0 with probability |𝛼|2 at the post-measurement state |0⟩ and the result 1 withprobability |𝛽|2 at the post-measurement state |1⟩, where 𝑀0 = |0⟩ × ⟨0| and 𝑀1 = |1⟩ × ⟨1|.
For multiple qubits, we use the tensor product of Hilbert spaces. Let ℋ1 and ℋ2 be two
Hilbert spaces. Their tensor product ℋ1 ⊗ ℋ2 is defined as a vector space consisting of linear
combinations of the vectors |𝜓1 𝜓2 ⟩ = |𝜓1 ⟩ |𝜓2 ⟩ = |𝜓1 ⟩⊗|𝜓2 ⟩, where |𝜓1 ⟩ ∈ ℋ1 and |𝜓2 ⟩ ∈ ℋ2 .
Systems of two or more qubits may be in entangled states, meaning that states of qubits are54

correlated and inseparable. Entanglement shows that an entangled state of two qubits cannot
be expressed as a tensor product of single-qubit states. We can use 𝐻 and CX gates to create
entangled states as follows: CX ((𝐻 ⊗ I ) |00⟩) = √12 (|00⟩ + |11⟩).
A pure quantum state can be represented by a ket vector |𝜓⟩, while a mixed state represents
the probabilistic mixtures of pure states and can be described byGiven∑︀ a density operator.
∑︀{(𝑝𝑖 , |𝜓𝑖 ⟩)} be an ensemble of pure states |𝜓𝑖 ⟩, where 𝑝𝑖 ≥ 0 and 𝑖 𝑝𝑖 = 1, 𝜌 = 𝑖 𝑝𝑖 |𝜓𝑖 ⟩⟨𝜓𝑖 |is the density operator representing the mixed state. 𝑈 transforms a mixed state 𝜌 to a mixed
state 𝜌′ by a matrix multiplication such that 𝜌′ = 𝑈 𝜌𝑈 † . For the quantum measurement {𝑀𝑚 }above, if the mixed state of a quantum system is 𝜌 before the measurement, then the probability
for the result 𝑚 is as follows:†𝑝(𝑚) = 𝑡𝑟(𝑀𝑚𝑀𝑚 𝜌),†

𝜌𝑀𝑚
and the mixed state after the measurement is 𝑀𝑚
provided that 𝑝(𝑚) > 0.
𝑝(𝑚)2.2. Symbolic Reasoning
We proposed symbolic reasoning [2, 11] based on Dirac notation with scalars using a set of laws
from quantum mechanics and basic matrix operations for reasoning about quantum computationand developed a support tool in Maude to automate the reasoning. This section briefly describes
terms used in our symbolic reasoning and laws used to reduce terms. The reader is recommended
to refer to [2] for more details.
2.2.1. Terms
Terms are built from scalars and basis vectors with some constructors.
• Scalars are complex numbers. We extend rational numbers supported in Maude to deal
with complex numbers. Some constructors for scalars, such as multiplication, fraction,
addition, conjugation, absolute, power, and square root are formalized, but we do notmention them here to make the paper concise.
• Basis vectors are the standard basis written in Dirac notation as |0⟩ and |1⟩.
• Constructors for matrices consist of scalar multiplication of matrices ·, matrix product ×,matrix addition +, tensor product ⊗, and the conjugate transpose 𝐴† of a matrix 𝐴.
In Dirac notation, ⟨0| is the dual of |0⟩ such that ⟨0|† = |0⟩ and |0⟩† = ⟨0|; similarly for ⟨1|.
The terms |𝑗⟩ × ⟨𝑘| and the inner product of |𝑗⟩ and |𝑘⟩ may be written shortly as |𝑗⟩ ⟨𝑘| and⟨𝑗|𝑘⟩ for any 𝑗, 𝑘 ∈ {0, 1}. By using these notations with the laws below, we can intuitively
explain how quantum operations work.
2.2.2. Laws
Table 1 presents a set of laws derived from the properties of quantum mechanics and basic
matrix operations. Because |0⟩ and |1⟩ can be viewed as 2 × 1 matrices, then the laws actuallydescribe matrix calculations with Dirac notation, zero and identity matrices, and scalars. These55

Table 1
A set of laws used for symbolic reasoning
No.

Law

L1

⟨0|0⟩ = ⟨1|1⟩ = 1, ⟨1|1⟩ = ⟨0|1⟩ = 0

L2
L3
L4
L5
L6
L7
L8
L9
L10
L11
L12
L13
L14
L15
L16
L17
L18
L19
L20

Associativity of ×, +, ⊗ and Commutativity of +0 · 𝐴𝑚×𝑛 = O𝑚×𝑛 , 𝑐 · O = O, 1 · 𝐴 = 𝐴

𝑐 · (𝐴 + 𝐵) = 𝑐 · 𝐴 + 𝑐 · 𝐵

𝑐1 · 𝐴 + 𝑐2 · 𝐴 = (𝑐1 + 𝑐2 ) · 𝐴
𝑐1 · (𝑐2 · 𝐴) = (𝑐1 · 𝑐2 ) · 𝐴(𝑐1 · 𝐴) × (𝑐2 · 𝐵) = (𝑐1 · 𝑐2 ) · (𝐴 × 𝐵)

𝐴 × (𝑐 · 𝐵) = (𝑐 · 𝐴) × 𝐵 = 𝑐 · (𝐴 × 𝐵)

𝐴 ⊗ (𝑐 · 𝐵) = (𝑐 · 𝐴) ⊗ 𝐵 = 𝑐 · (𝐴 ⊗ 𝐵)

O𝑚×𝑛 × 𝐴𝑛×𝑝 = 𝐴𝑚×𝑛 × O𝑛×𝑝 = O𝑚×𝑝
I 𝑚 × 𝐴𝑚×𝑛 = 𝐴𝑚×𝑛 × I 𝑛 = 𝐴𝑚×𝑛
𝐴+O=O+𝐴=O

O𝑚×𝑛 ⊗ 𝐴𝑝×𝑞 = 𝐴𝑝×𝑞 ⊗ O𝑚×𝑛 = O𝑚𝑝×𝑛𝑞
𝐴 × (𝐵 + 𝐶) = 𝐴 × 𝐵 + 𝐴 × 𝐶(𝐴 + 𝐵) × 𝐶 = 𝐴 × 𝐶 + 𝐵 × 𝐶(𝐴 ⊗ 𝐵) × (𝐶 ⊗ 𝐷) = (𝐴 × 𝐶) ⊗ (𝐵 × 𝐷)𝐴 ⊗ (𝐵 + 𝐶) = 𝐴 ⊗ 𝐵 + 𝐴 ⊗ 𝐶(𝐴 + 𝐵) ⊗ 𝐶 = 𝐴 ⊗ 𝐶 + 𝐵 ⊗ 𝐶(𝑐 · 𝐴)† = 𝑐* · 𝐴† , (𝐴 × 𝐵)† = 𝐵 † × 𝐴†

(𝐴 + 𝐵)† = 𝐴† + 𝐵 † , (𝐴 ⊗ 𝐵)† = 𝐴† ⊗ 𝐵 †L21†
𝐼𝑚 † = 𝐼𝑚 , 𝑂𝑚×𝑛
= 𝑂𝑛×𝑚 , (𝐴† )† = 𝐴

L22|0⟩ = ⟨0| , ⟨0| = |0⟩ , |1⟩ = ⟨1| , ⟨1| = |1⟩

†

†

†

†

laws are described by equations in Maude and are used to automatically reduce terms until nomore matrix operation is applicable. Some laws dedicated to simplifying the expressions aboutcomplex numbers are also formalized in Maude by means of equations.

2.3. Kripke Structures
A Kripke structure 𝐾 is ⟨𝑆, 𝐼, 𝑇, 𝐴, 𝐿⟩ [12], where 𝑆 is a set of states, 𝐼 ⊆ 𝑆 is the set of initialstates, 𝑇 ⊆ 𝑆 × 𝑆 is a left-total binary relation over 𝑆, 𝐴 is a set of atomic propositions and
𝐿 is a labeling function whose type is 𝑆 → 2𝐴 . Each element (𝑠, 𝑠′ ) ∈ 𝑇 is called a statetransition from 𝑠 to 𝑠′ and 𝑇 may be called the state transitions (with respect to 𝐾). For a state𝑠 ∈ 𝑆, 𝐿(𝑠) is the set of atomic propositions that hold in 𝑠. A path 𝜋 is an infinite sequence𝑠0 , . . . , 𝑠𝑖 , 𝑠𝑖+1 , . . . such that 𝑠𝑖 ∈ 𝑆 and (𝑠𝑖 , 𝑠𝑖+1 ) ∈ 𝑇 for each 𝑖. We use the following
notations for paths: 𝜋 𝑖 ≜ 𝑠𝑖 , 𝑠𝑖+1 , . . ., 𝜋𝑖 ≜ 𝑠0 , . . . , 𝑠𝑖 , 𝑠𝑖 , 𝑠𝑖 , . . ., 𝜋(𝑖) ≜ 𝑠𝑖 , where ≜ is used as“be defined as.” 𝜋 𝑖 is obtained by deleting the first 𝑖 states 𝑠0 , 𝑠1 , . . . , 𝑠𝑖−1 from 𝜋. 𝜋𝑖 is obtained56

by taking the first 𝑖 + 1 states 𝑠0 , 𝑠1 , . . . , 𝑠𝑖−1 , 𝑠𝑖 and adding 𝑠𝑖 unboundedly many times at theend. 𝜋(𝑖) is the 𝑖th state 𝑠𝑖 . Let 𝒫 be the set of all paths. 𝜋 is called a computation if 𝜋(0) ∈ 𝐼.
Let 𝒞 be the set of all computations.
The syntax of a formula 𝜙 in LTL for 𝐾 is as follows:
𝜙 ::= ⊤ | 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | ○ 𝜙 | 𝜙 𝒰 𝜙where 𝑝 ∈ 𝐴. Let ℱ be the set of all formulas in LTL for 𝐾. An arbitrary path 𝜋 ∈ 𝒫 of 𝐾 andan arbitrary LTL formula 𝜙 ∈ ℱ of 𝐾, 𝐾, 𝜋 |= 𝜙 is inductively defined as follows:• 𝐾, 𝜋 |= ⊤• 𝐾, 𝜋 |= 𝑝 iff 𝑝 ∈ 𝐿(𝜋(0))• 𝐾, 𝜋 |= ¬𝜙1 iff 𝐾, 𝜋 ̸|= 𝜙1• 𝐾, 𝜋 |= 𝜙1 ∧ 𝜙2 iff 𝐾, 𝜋 |= 𝜙1 and 𝐾, 𝜋 |= 𝜙2• 𝐾, 𝜋 |= ○ 𝜙1 iff 𝐾, 𝜋 1 |= 𝜙1• 𝐾, 𝜋 |= 𝜙1 𝒰 𝜙2 iff there exists a natural number 𝑖 such that 𝐾, 𝜋 𝑖 |= 𝜙2 and for all
natural numbers 𝑗 < 𝑖, 𝐾, 𝜋 𝑗 |= 𝜙1
where 𝜙1 and 𝜙2 are LTL formulas. Then, 𝐾 |= 𝜙 iff 𝐾, 𝜋 |= 𝜙 for each computation 𝜋 ∈ 𝒞of 𝐾. ○ and 𝒰 are called the next temporal connective and the until temporal connective,
respectively. We define ♢ 𝜙 ≜ ⊤ 𝒰 𝜙, where ♢ is called the eventual temporal connective. In
this paper, we use LTL formulas to express desired properties under verification for our casestudies.
In this paper, a state is expressed as a braced associative-commutative (AC) collection ofname-value pairs, where a name may have parameters. The order of elements is not relevantin AC collections, such as sets. AC collections are called soups, and name-value pairs arecalled observable components. That is, a state is expressed as a braced soup of observable
components. The juxtaposition operator is used as the constructor of soups. Let 𝑜𝑐1 , 𝑜𝑐2 , 𝑜𝑐3 beobservable components, and then 𝑜𝑐1 𝑜𝑐2 𝑜𝑐3 is the soup of those three observable components.
Since the order is irrelevant because of AC, 𝑜𝑐1 𝑜𝑐2 𝑜𝑐3 is the same as some others, such as
𝑜𝑐3 𝑜𝑐2 𝑜𝑐1 . A state is expressed as {𝑜𝑐1 𝑜𝑐2 𝑜𝑐3 }. In this paper, rewrite rules are used to specify
state transitions. Concretely, we use Maude [4], a programming/specification language basedon rewriting logic. Maude makes it possible to specify complex systems flexibly and is also
equipped with a built-in LTL model checker to conduct model checking experiments.

3. Formal Specification
This section summarizes how we formalize qubits, quantum gates, measurements, and thenquantum circuits in [2] and describes how we extend it to deal with mixed states.

3.1. Formalization of Qubits, Gates, and Measurements
Pure states of qubits are represented in our formalization as the linear combination of tensor
product of the standard basis in Dirac notation with scalars. This representation is also adopted

57

for quantum gates. In our work, we exclusively focus on binary projective measurements
conducted on the standard basis. This implies that our measurement operators consist of twoelements, denoted as 𝑀0 and 𝑀1 . To formalize a mixed state, we prepare an ensemble of purestates and calculate its corresponding density operator as described in Section 2.

3.2. A Formalization of Quantum Circuits
Our approach to formalizing quantum circuits begins by representing them as a sequencecomprising various actions, including quantum gates, measurements, qubit initializations, andother operations, as depicted in Figure 1. Following this, we establish Kripke structures tailoredto quantum circuits to conduct model checking that quantum circuits enjoy desired properties.
3.2.1. Elements of Quantum Circuits
A whole quantum state is formalized as a density operator representing a mixed state. In
our previous work [2], a whole quantum state is formalized as a pure state, which is a linear
combination of the tensor product of basic vectors with Dirac notation and complex numbers.
Classical bits are formalized the same as in our previous work [2]. They are represented as a
mapping from circuit indices to Boolean values. Each entry in this mapping takes the form of(𝑖 ↦→ 𝑏), indicating that the value of the classical bit stored at position 𝑐𝑖 is 𝑏, with 𝑏 taking onvalues of either 0 or 1.
A sequence comprising quantum gates, measurements, and conditional gates in a quantum
circuit is formalized as a list of actions. Each action can take one of the following forms:• I(𝑖) applies the I gate on qubit at index 𝑖,• X(𝑖) applies the X gate on qubit at index 𝑖,• Y(𝑖) applies the Y gate on qubit at index 𝑖,• Z(𝑖) applies the Z gate on qubit at index 𝑖,• H(𝑖) applies the H gate on qubit at index 𝑖,• CX(𝑖, 𝑗 ) applies the CX gate on qubits at indices 𝑖 and 𝑗,• CY(𝑖, 𝑗 ) applies the CY gate on qubits at indices 𝑖 and 𝑗,• CZ(𝑖, 𝑗 ) applies the CZ gate on qubits at indices 𝑖 and 𝑗,• SWAP(𝑖, 𝑗 ) applies the SWAP gate on qubits at indices 𝑖 and 𝑗,• CCX(𝑖, 𝑗, 𝑘 ) applies the CCX gate on qubits at indices 𝑖, 𝑗 and 𝑘,• CCZ(𝑖, 𝑗, 𝑘 ) applies the CCX gate on qubits at indices 𝑖, 𝑗 and 𝑘,• CSWAP(𝑖, 𝑗, 𝑘 ) applies the CSWAP gate on qubits at indices 𝑖, 𝑗 and 𝑘,• M(𝑖) measures 𝑞𝑖 with the standard basis,• c[𝑖] == 𝑏 ? AL checks if the classical bit at 𝑐𝑖 equals 𝑏, then a list AL of actions is
executed.
All actions except the two last actions representing measurements and conditional actions
are called basic actions. In this paper, we support more quantum gates than in our previous
work [2], including S , T , CY , CZ , SWAP, CCY , CCZ , and CSWAP gates.

58

3.2.2. Kripke Structures of Quantum Circuits
Let 𝐾 be the Kripke structure formalizing a quantum circuit. In our formalization, we define
five distinct observable components as follows:• (mState: 𝑚𝑠) denotes the mixed quantum state 𝑚𝑠.
• (#qubits: 𝑛) denotes the number of qubits 𝑛.
• (bits: 𝑏𝑚) denotes the classical bits obtained from measurements and stored in a bit
map 𝑏𝑚.
• (prob: 𝑝) denotes the probability 𝑝 at the current quantum state.
• (actions: 𝑎𝑙) denotes the action list 𝑎𝑙, guiding us on how the circuit works.
• (isEnd: 𝑏) denotes termination with Boolean flag 𝑏.
Each state in 𝑆 is expressed as {𝑜𝑏𝑠}, where 𝑜𝑏𝑠 is a soup of those five distinct observable
components. The mState and #qubits observable components are newly added to deal with
mixed states compared to our previous work [2].
𝑇 now consists of six rewrite rules in our formalization. Let OCs be a Maude variable ofobservable component soups, MS and MS’ be Maude variables of whole quantum states, BM be
a Maude variable of bit maps, Prob and Prob’ be Maude variables of scalars, AL and AL’ be
Maude variables of action lists, B be a Maude variable of Boolean values, and N, N’, N1, and N2
are Maude variables of natural numbers.
The first rewrite rule is as follows:
crl [U] : {(mState: MS) (actions: (A AL)) (#qubits: N) OCs}=> {(mState: MS’) (actions: AL) (#qubits: N) OCs}
if isBasicAction(A) /\ MS’ := unitary(MS, A, N) .

The rule U simulates unitary transformation on the whole quantum state in mState observable
component if its basic action appears in actions observable component.
The next two rewrite rules are as follows:
crl [M0] :{(mState: MS) (actions: (M(N’) AL)) (prob: Prob) (bits: BM) (#qubits: N) OCs}=> {(mState: MS’) (actions: AL) (prob: (Prob .* Prob’)) (bits: insert(N’, 0, BM))(#qubits: N) OCs}
if {mState: MS’, prob: Prob’} := measure(MS, N, P0, N’) .
crl [M1] :{(mState: MS) (actions: (M(N’) AL)) (prob: Prob) (bits: BM) (#qubits: N) OCs}=> {(mState: MS’) (actions: AL) (prob: (Prob .* Prob’)) (bits: insert(N’, 1, BM))(#qubits: N) OCs}
if {mState: MS’, prob: Prob’} := measure(MS, N, P1, N’) .

where P0 and P1 are Maude constants of matrices representing the measurement operators
M 0 and M 1 , respectively. Therefore, the rules M0 and M1 govern the process of measuring aqubit at index N’ with the measurement operators M 0 and M 1 , respectively. In these rules,
the classical outcomes are stored accordingly into the bit map in bits observable component;59the probabilities and the post-measurement mixed states are updated in prob and mStateobservable components, respectively. It is important to note that these two rules introduce
non-deterministic probabilistic transitions when measuring a single qubit.
The next rewrite rule is identical to the one presented in our previous work [2]. It outlines
the processes of conditionally executing the next actions based on classical bits obtained frommeasurements if applicable.
rl [cif] :{(qstate: Q) (bits: ((N |-> N1),BM)) (actions: ((c[N] == N2 ? AL’) AL)) OCs}=> {(qstate: Q) (bits: ((N |-> N1), BM))(actions: ((if (N1 == N2) then AL’ else nil fi) AL)) OCs} .

This rule says that if c[N] == N2 ? AL’ exists in the action list and the classical bit N1 atindex N equals the conditional value N2, then the action list AL’ is added at the beginning of
the action list AL in actions observable component. This means that AL’ will be executed
next. Otherwise, it is simply ignored and AL remains unchanged.
The last two rules are the same as in our previous work [2] as follows:rl [end] : {(actions: nil) (isEnd: false) OCs}=> {(actions: nil) (isEnd: true) OCs} .
rl [stutter]: {(isEnd: true) OCs} => {(isEnd: true) OCs} .

The rule end indicates termination when the action list is empty, denoted as nil. On the other
hand, the rule stutter is to make 𝑇 total when isEnd observable component is true.

4. A Case Study: Quantum Teleportation
For the sake of simplicity, this section only demonstrates how to use our symbolic approach withdensity operators to conduct model checking for Quantum Teleportation [7]. Meanwhile, othercommunication protocols are similar and the full specifications of all quantum communication
protocols concerned in this paper are publicly available at https://github.com/canhminhdo/
QTC-Maude under the mixed-states folder.

4.1. Introduction
Quantum Teleportation, as described in [7], leverages the unique properties of entanglement inquantum mechanics to transmit an unknown quantum state |𝜓⟩ from Alice to Bob, utilizing
only three qubits and two classical bits. This protocol holds significant importance because of
the no-cloning theorem [13], which prohibits the exact copy of an arbitrary unknown quantum
state. As a result, the protocol becomes a crucial method for transmitting an arbitrary unknown
quantum state from one source to another.
The circuit illustrated in Figure 1 presents how the protocol works. Alice manipulates on
qubits 𝑞0 and 𝑞1 , and Bob manipulates on qubit 𝑞2 as follows:

60

61

where (x) denotes the tensor product; and a and b are Maude constants of scalars denoting
arbitrary scalars such that |a|2 + |b|2 = 1. We suppose that the mixed state consists of only
one pure state with a certain probability in the ensemble.
The set 𝐼 of initial states for Quantum Teleportation includes only one initial state as follows:{(isEnd: false)(#qubits: findN(ES))(mState: convert(ES)(prob: 1)(bits: empty)(actions: H(1) CX(1, 2) CX(0, 1) H(0)M(0) M(1)c[1] == 1 ? X(2)c[0] == 1 ? Z(2))}

where findN(_) and convert(_) are two functions to calculate the number of qubits and thedensity operator of a mixed state given an ensemble. Initially, isEnd observable component isfalse, prob observable component is one, mState represent the corresponding density operatorof the symbolic state as the input state of the protocol, actions observable component contains
the action list describing how the protocol works.

4.3. Model Checking Quantum Teleportation
Let 𝐾 and init be the Kripke structure and the initial state for Quantum Teleportation,
respectively. In order to perform model checking on the Kripke structure 𝐾 and verify thatit satisfies the desired properties, we define the set of atomic propositions 𝐴 and the labeling
function 𝐿. 𝐴 contains one atomic proposition, denoted as isSuccess. 𝐿 is defined as follows:eq {(isEnd: true) (mState: MS) (prob: Prob) (#qubits: N) OCs} |= isSuccess= Prob > 0 implies
tr[1]((tr[0](MS, N)), N) == (I (x) I (x) (PSI x (PSI)^+)) .
eq {OCs} |= PROP = false [owise] .

where PSI is the input state of the protocol being transferred, the function tr[_](_,_) take
inputs as the index at which the information of the qubit is erased, the mixed state, and thenumber of qubits. The function will erase information of a subsystem from the mixed state at
an index. Using this function we can retain the information of the qubit at the index 2 in thedensity operator. This function works as the partial trace over a quantum system [10].
The two equations say that isSuccess holds at a state if the state contains (isEnd:true), (mState: MS), (prob: Prob), and (#qbits: N) such that the condition tr[1]((tr[0](MS, N)), N) == (I (x) I (x) (PSI x (PSI)^+) holds whenever Prob > 0
holds, meaning that the qubit received by Bob at the end is equal to the qubit sent by Alice atthe beginning with a non-zero probability by means of density operators. Notice that, the use ofdensity operators to represent quantum states can eliminate the global phase when comparing
two quantum states. Let teleProp be an LTL formula defined as <> isSuccess, where <> isthe eventual temporal connective.

62

Table 2
Experimental results with pure states and mixed states for representing quantum states
Protocol

QubitsStatesPure States

Mixed States

Rewrite Steps

Time
≈ 0ms

Superdense Coding

2

9

685

Quantum Teleportation

3

27

4,340

Rewrite Steps

Time

2,088

2ms

3ms

29,09530ms

Quantum Secret Sharing

465

16,4499ms

211,831

519ms

Entanglement Swapping

4

33

6,930

4ms

56,19340ms

We want to model check that 𝐾 = ⟨𝑆, 𝐼, 𝑇, 𝐴, 𝐿⟩ satisfies teleProp from the initial state

init in Maude as follows:

red modelCheck(init, teleProp) .

No counterexample is found in just a few moments and so 𝐾 satisfies teleProp. In otherwords, we successfully verify the correctness of Quantum Teleportation by using our symbolicmodel checking approach with density operators.

5. Experimental Results
We used an iMac that carries a 4 GHz microprocessor with eight cores and 32 GB memory RAM
to conduct experiments in this section. As case studies, we conduct model checking experiments
to verify the correctness of several quantum communication protocols with our approach inwhich both pure states and mixed states are used for representing quantum states as follows:• Superdense Coding [6] for transmitting two classical bits using an entangled state,• Quantum Teleportation [7] for teleporting an arbitrary pure state by sending two bits ofclassical information,• Quantum Secret Sharing [8] for teleporting a pure state from a sender (Alice) to a receiver(Bob) with the help of a third party (Charlie),• Entanglement Swapping [9] for creating a new entangled state,
Superdense Coding is the simplest one that uses only two qubits; Quantum Teleportation
uses three qubits; Quantum Secret Sharing proposed relying on the mechanism of Quantum
Teleportation uses four qubits; and Entanglement Swapping uses four qubits. Note that theproperties being verified for both pure states and mixed states are identical in our experiments.
Our support tool and case studies are publicly available at https://github.com/canhminhdo/
QTC-Maude under the mixed-states folder.
The experimental results are shown in Table 2. The second and third columns denote thenumber of qubits in each protocol and the number of states in the reachable state space ofeach protocol under model checking, respectively. Notice that the number of states of each
protocol under model checking is the same for both pure states and mixed states. The fourthand fifth columns denote the number of rewriting steps performed for each protocol and the63verification time when pure states are used to represent quantum states; and similarly for thelast two columns when mixed states are used. Note that, in these experiments, the mixed statein each protocol consists of only one pure state with a certain probability in an ensemble.
Although all model checking experiments were completed in just a few moments, the numberof rewriting steps and the verification time for mixed states is considerably larger than that forpure states. This is not surprising because we intentionally used an ensemble that contains only
one pure state with a certain probability in these experiments, and the pure state is represented
by a vector |𝜓⟩, while the mixed state is represented by a density operator |𝜓⟩⟨𝜓|, which is amatrix. The calculation for a matrix is more expensive than that for a vector. However, with
mixed states, we can present a statistical mixture of multiple pure states and eliminate theglobal phase compared with the pure states. Our symbolic model checking quantum circuits in
Maude can handle both pure states and mixed states, showing its usefulness in quantum circuitverification.

6. Related WorkGay et al. [14] introduced a method for employing classical model checkers, such as PRISM,
a probabilistic model checker, to verify quantum protocols. In their approach, each quantum
state is assigned a distinct number of identifiers and transitions from one unique number toanother representing the operations of quantum gates and measurements. However, this method
necessitates the prior enumeration of states and the computation of state transitions, which
are subsequently encoded into a PRISM specification. Despite their development of a tool
called PRISMGEN to automate this process, its practicality is limited in real-world scenarios,
supporting only two or three qubits due to the exponential proliferation of state numbers. In
contrast, our approach does not require the pre-enumeration of states, as quantum states are
directly formalized using Dirac notation with scalar values. Furthermore, we utilize rewrite
rules to represent the effects of quantum gates and measurements, rendering our approachcapable of handling a larger number of qubits. For instance, we have successfully verified thecorrectness of Quantum Secret Sharing and Entanglement Swapping involving four qubits using
our approach.
Our approach to symbolic quantum circuit model checking draws inspiration from a priorwork by Yuan et al. [15], which closely resembles our methodology. However, it’s worth notingthat their approach primarily centers around theorem proving rather than model checking.
They adopt Dirac notation and a set of rules to formalize quantum states, gates, measurements,
and reason about quantum circuits within the Coq interactive theorem prover. Nevertheless, anotable distinction is that their approach often necessitates users to supply essential lemmas
to facilitate the completion of their proofs, a task that is generally considered challenging. In
contrast, our approach operates entirely autonomously, requiring no human intervention.

7. Conclusion
We have extended our symbolic approach to deal with mixed states using density operators andhave developed a support tool in Maude. Several quantum communication protocols have been64

successfully analyzed using our approach/support tool, including Superdense Coding, Quantum
Teleportation, Quantum Secret Sharing, and Entanglement Swapping. This demonstrates theusefulness of our symbolic model checking quantum circuits with density operators in Maude.
As one piece of future work, we would conduct more case studies, where a statistical mixture ofmultiple pure states is realistically presented in them.

Acknowledgments
The research was supported by JAIST Research Grant for Fundamental Research, by JST SICORP
Grant Number JPMJSC20C2, and by JSPS KAKENHI Grant Number JP23K19959.

References[1] P. Shor, Algorithms for quantum computation: discrete logarithms and factoring, in:Proceedings 35th Annual Symposium on Foundations of Computer Science, 1994, pp.
124–134. doi:10.1109/SFCS.1994.365700.
[2] C. M. Do, K. Ogata, Symbolic model checking quantum circuits in maude, in: The 35th
International Conference on Software Engineering and Knowledge Engineering, SEKE
2023, 2023, pp. 103–108. doi:10.18293/SEKE2023-014.
[3] P. A. M. Dirac, A new notation for quantum mechanics, Mathematical Proceedings of theCambridge Philosophical Society 35 (1939) 416–418. doi:10.1017/S0305004100021162.
[4] M. Clavel, et al., All About Maude, volume 4350 of Lecture Notes in Computer Science,
Springer, 2007. doi:10.1007/978-3-540-71999-1.
[5] J. Meseguer, Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming 81 (2012) 721–781. doi:10.1016/j.jlap.2012.06.003.
[6] C. H. Bennett, S. J. Wiesner, Communication via one- and two-particle operators on
einstein-podolsky-rosen states, Phys. Rev. Lett. 69 (1992) 2881–2884. doi:10.1103/
PhysRevLett.69.2881.
[7] C. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres, W. Wootters, Teleporting an
unknown quantum state via dual classical and einstein-podolsky-rosen channels, Physicalreview letters 70 (1993) 1895–1899. doi:10.1103/PhysRevLett.70.1895.
[8] M. Hillery, V. Bužek, A. Berthiaume, Quantum secret sharing, Physical Review A 59 (1999)
1829–1834. doi:10.1103/physreva.59.1829.
[9] M. Żukowski, A. Zeilinger, M. A. Horne, A. K. Ekert, “Event-ready-detectors” Bell experiment via entanglement swapping, Phys. Rev. Lett. 71 (1993) 4287–4290. doi:10.1103/
PhysRevLett.71.4287.
[10] M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information: 10th Anniversary Edition, Cambridge University Press, 2010. doi:10.1017/CBO9780511976667.
[11] T. Takagi, C. M. Do, K. Ogata, Automated quantum program verification in dynamic
quantum logic (to appear), in: DaLí: Dynamic Logic – New trends and applications, 2023.
[12] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem (Eds.), Handbook of Model Checking,Springer, 2018. doi:10.1007/978-3-319-10575-8.

65[13] W. K. Wootters, W. H. Zurek, A single quantum cannot be cloned, Nature 299 (1982)
802–803. doi:10.1038/299802a0.
[14] S. Gay, R. Nagarajan, N. Papanikolaou, Probabilistic model–checking of quantum protocols,
2005. doi:10.48550/arXiv.quant-ph/0504007.
[15] W. Shi, Q. Cao, Y. Deng, H. Jiang, Y. Feng, Symbolic reasoning about quantum circuits incoq, J. Comput. Sci. Technol. 36 (2021) 1291–1306. doi:10.1007/s11390-021-1637-9.

66

Reachability Analysis of the Equivalence of Two
Terms in Free Orthomodular Lattices
Tsubasa Takagi1 , Canh Minh Do2 and Kazuhiro Ogata2
1
2

Tokyo Institute of Technology, Tokyo, Japan
Japan Advanced Institute of Science and Technology, Nomi, Japan

Abstract

Since 1936, the algebraic structure of quantum mechanics called orthomodular lattices have attracted
many logicians’ attention. Over its long history, various complex theorems have been manually proven.
Some tools have been developed to automatically verify these theorems by means of checking theequivalence of two terms (the word problem). However, existing tools cannot deal with terms that consistof three or more free variables. Although the number of normal forms in free orthomodular lattices withthree or more generators is infinite, that of two generators is only 96. To overcome this limitation, we
transform the word problem into a reachability problem. Using this idea, we implement a support toolin Maude. It consists of a formal specification of free orthomodular lattices and an implementation of(1) the 96 normal forms of two generators and (2) a theorem describing when the distributive laws canbe applied. The reachability analysis is performed using the search command in Maude to deal withterms that consist of even three or more variables. We conduct some case studies with the support tool
to verify various complex theorems that existing tools cannot verify.

Keywords

Orthomodular Lattice, Word Problem, Reachability Analysis, Maude

1. Introduction
The algebraic structure of quantum mechanics has been discussed by many logicians since
1936 [1]. Among various algebras, orthomodular lattices (sometimes called quantum logic) [2]
are particularly significant because the set of all closed subspaces of a Hilbert space forms an
orthomodular lattice, which is called a Hilbert lattice [3].
So far, some theorems such as the Foulis-Holland theorem [4, 5] and a theorem [2, Corollary
VII.7.7] about skew join and skew meet are verified [6] with the aid of computer programs [7, 8].
Furthermore, several new theorems regarding the verification of the equivalence of two terms
have been obtained with the aid of these programs. For example, all associative operators [9],monotonic operators [10], and weak associative operators [11] in orthomodular lattices havebeen enumerated with their results, which could be hardly obtained without computer support.
The word problem for free orthomodular lattices remains an open problem in general [12].
To make matters worse, even if the word problem is solvable, it may not be implemented byfinite convergent AC (associative and commutative) term rewriting systems. For example, it isInternational Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols 2023
$ takagi.t.ah@m.titech.ac.jp (T. Takagi); canhdo@jaist.ac.jp (C. M. Do); ogata@jaist.ac.jp (K. Ogata) 0000-0001-9890-1015 (T. Takagi); 0000-0002-1601-4584 (C. M. Do); 0000-0002-4441-3259 (K. Ogata)67

known that there is no finite convergent AC term rewriting system for the equational theoryof lattices [13]. However, although the word problem may not be solvable, it is still worth
implementing a tool that can solve the word problem, not for any terms but for some specificterms of free orthomodular lattices, which consist of three or more free variables.
There are two existing programs [14, 7] for checking the equivalence of two terms in freeorthomodular lattices. However, these programs cannot deal with terms that consist of threeor more free variables. This is because there are infinite normal forms in three or more freegenerators, even though there are only 96 normal forms in the case of two free generators(Theorem 3.3). This limitation to some two free generators is fatal when proving theorems
expressed by three or more generators in orthomodular lattices.
In this paper, we overcome this limitation by incorporating the idea of reachability analysis
into a neither confluent nor terminating term rewriting system for free orthomodular lattices.
The word problem is transformed into a reachability problem in the term rewriting system
by searching for the reachable state space from an initial state. It is done by the breadth-firstsearch (BFS) to find a solution in which the two terms in the word problem are rewritten into
the same term after a finite number of rewrite steps, where each rewrite step can be regarded
as a state transition. The reachability problem is conducted through a breadth-first search in an
incremental way, which does not strictly require the reachable state space to be finite. However,
the reachability analysis may not terminate in general.
Based on this idea, we implement a support tool in Maude, a rewriting logic-based specification/programming language that can deal with terms that consist of three or more freevariables. The reachability analysis is performed using the search command, a reachability
analyzer, in Maude. The support tool consists of a formal specification of free orthomodular
lattices and an implementation of (1) the 96 normal forms of two generators (see Theorem 3.3)and (2) a theorem (see Theorem 3.4) describing when the distributive laws can be applied tocheck the word problem for free orthomodular lattices. Theorem 3.3 has been used in previous
work [14, 7], while Theorem 3.4 is a new theorem proposed in this paper. To demonstrate theeffectiveness of our approach, we verify the validity of some axioms with three free variables inseveral implication algebras [15, 16, 17, 18].
The rest of the paper is organized as follows. Section 2 reviews some kinds of lattices. Section 3
describes the theoretical background for the word problem for various free lattices and two
significant theorems in orthomodular lattices. Section 5 presents the implementation of ourtool in Maude. Section 6 shows some case studies. Section 7 compares our tool and existing
tools. Finally, Section 8 concludes the paper together with some future directions.

2. Preliminaries
This section presents some kinds of lattices, such as distributive lattices, modular lattices,ortholattices, Boolean lattices, modular ortholattices, and orthomodular lattices. All of theselattices are defined using only equations. This makes it possible to implement them in algebraic
specification languages (e.g., Maude [19]).

68

2.1. Distributive Lattice and Modular Lattice
Definition 2.1. A lattice is a triple (𝐿, ∧, ∨) that consists of a non-empty set 𝐿 and functions∧ : 𝐿 × 𝐿 → 𝐿 and ∨ : 𝐿 × 𝐿 → 𝐿 satisfying
1. (Associativity) 𝑝 ∧ (𝑞 ∧ 𝑟) = (𝑝 ∧ 𝑞) ∧ 𝑟 and 𝑝 ∨ (𝑞 ∨ 𝑟) = (𝑝 ∨ 𝑞) ∨ 𝑟,
2. (Commutativity) 𝑝 ∧ 𝑞 = 𝑞 ∧ 𝑝 and 𝑝 ∨ 𝑞 = 𝑞 ∨ 𝑝,
3. (Idempotency) 𝑝 ∧ 𝑝 = 𝑝 and 𝑝 ∨ 𝑝 = 𝑝,
4. (Absorption) 𝑝 ∧ (𝑝 ∨ 𝑞) = 𝑝 and 𝑝 ∨ (𝑝 ∧ 𝑞) = 𝑝.
Given a lattice (𝐿, ∧, ∨), a partial order (a binary relation that is reflexive, transitive, andantisymmetric) ≤ on 𝐿 is defined by≤ = {(𝑝, 𝑞) : 𝑝 ∧ 𝑞 = 𝑝} = {(𝑝, 𝑞) : 𝑝 ∨ 𝑞 = 𝑞}.
Then, 𝑝 ∧ 𝑞 is identical to the infimum (the greatest lower bound) of {𝑝, 𝑞}, and 𝑝 ∨ 𝑞 is identicalto the supremum (the least upper bound) of {𝑝, 𝑞}.
The following properties of lattices are of particular significance.
Definition 2.2. A lattice (𝐿, ∧, ∨) is said to be• bounded if it has the least element (denoted by ⋏) and the greatest element (denoted by⋎) under the partial order ≤.
• distributive if the distributive law holds:𝑝 ∧ (𝑞 ∨ 𝑟) = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟)
for any 𝑝, 𝑞, 𝑟 ∈ 𝐿.
• modular if the modular law holds:𝑝 ∧ (𝑞 ∨ (𝑝 ∧ 𝑟)) = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟)
for any 𝑝, 𝑞, 𝑟 ∈ 𝐿.
Example 2.3 (Powerset Lattice). Let ℘(𝑋) be the powerset of a set 𝑋. Then, (℘(𝑋), ∩, ∪)called the powerset lattice on 𝑋 is a distributive lattice.
Example 2.4. Let 𝒢 = (𝐺, +) be an additive group, and 𝐿(𝒢) be the set of all subgroups of 𝒢.
Then, (𝐿(𝒢), ∩, +) is a modular lattice, where + on 𝐿(𝒢) is defined by
𝐺1 + 𝐺2 = {𝑔1 + 𝑔2 : 𝑔1 ∈ 𝐺1 , 𝑔2 ∈ 𝐺2 }.
Note that 𝐺1 + 𝐺2 is the smallest subgroup of 𝒢 containing 𝐺1 ∪ 𝐺2 .
By using the partial order ≤, the modular law can be rephrased as follows [20]:𝑝 ≤ 𝑟 implies 𝑝 ∨ (𝑞 ∧ 𝑟) = (𝑝 ∨ 𝑞) ∧ 𝑟.

69

2.2. Ortholattice and Orthomodular Lattice
Definition 2.5. An ortholattice (also called an orthocomplemented lattice) is a bounded latticeequipped with an orthocomplementation. An orthocomplementation on a bounded lattice(𝐿, ∧, ∨) is a function ¬ : 𝐿 → 𝐿 such that
1. 𝑝 ∧ ¬𝑝 = ⋏ and 𝑝 ∨ ¬𝑝 = ⋎,2. ¬¬𝑝 = 𝑝,
3. ¬(𝑝 ∧ 𝑞) = ¬𝑝 ∨ ¬𝑞 and ¬(𝑝 ∨ 𝑞) = ¬𝑝 ∧ ¬𝑞,
for any 𝑝, 𝑞 ∈ 𝐿. In particular, distributive ortholattices are called Boolean lattices.
Example 2.6 (Four-dimensional Hypercube). The lattice depicted in the following Hasse
diagram is a Boolean lattice, where 𝑝 → 𝑞 and 𝑝 ↔ 𝑞 are abbreviations for ¬𝑝 ∨ 𝑞 and(𝑝 ∧ 𝑞) ∨ (¬𝑝 ∧ ¬𝑞), respectively. This lattice is called the four-dimensional hypercube and isdenoted by 24 .
⋎𝑝∨𝑞 𝑞 →𝑝𝑝𝑞

𝑝 → 𝑞 ¬𝑝 ∨ ¬𝑞𝑝↔𝑞𝑝 ↔ ¬𝑞 ¬𝑞

𝑝 ∧ 𝑞 𝑝 ∧ ¬𝑞¬𝑝¬𝑝 ∧ 𝑞¬𝑝 ∧ ¬𝑞⋏

Example 2.7 (Chinese Lantern). The lattice depicted in the following Hasse diagram is a(non-distributive) modular ortholattice. This lattice is called the Chinese lantern and is denotedby 𝑀 𝑂2 .
⋎
𝑝

¬𝑝

𝑞

¬𝑞

⋏
Example 2.8 (Boolean Powerset Lattice). Let 𝑐 be the set complementation in a set 𝑋. Then,(℘(𝑋), ⊆, 𝑐 ) is a Boolean lattice and is called the Boolean powerset lattice on 𝑋.
Example 2.9 ([3, Proposition 4.3]). Let ℋ = (𝐻 fin , +, ·) be a finite-dimensional Hilbert
space over the complex numbers and 𝒞(ℋ) be the set of all (closed) subspaces of ℋ. Then,(𝒞(ℋ), ∩, +, ⊥ ) is a modular ortholattice, where + on ℋ is defined by
𝑉1 + 𝑉2 = {𝑣1 + 𝑣2 : 𝑣1 ∈ 𝑉1 , 𝑣2 ∈ 𝑉2 },and 𝑣 ′ ∈ 𝑉 ⊥ if and only if the inner product of 𝑣 ′ and 𝑣 is 0 for any 𝑣 ∈ 𝑉 .

70

Note that 𝒞(ℋ) is not modular if the dimension of ℋ is infinite [3, Proposition 4.4]. However,quantum mechanics are formulated by an infinite dimensional Hilbert space in general. This
motivates us to weaken the modular law to the orthomodular law below.
Definition 2.10. An orthomodular lattice is an ortholattice (𝐿, ∧, ∨, ¬) satisfying the orthomodular law [3, Proposition 3.5]:
𝑝 ≤ 𝑞 implies 𝑞 = 𝑝 ∨ (¬𝑝 ∧ 𝑞),
for any 𝑝, 𝑞 ∈ 𝐿
For any Hilbert space ℋ, regardless of its dimension, (𝒞(ℋ), ∩, +, ⊥ ) is an orthomodular
lattice [3, Proposition 4.5]. Thus, modular ortholattices and orthomodular lattices are different.
By the following theorem, the class of orthomodular lattices is characterized only by equations.
Theorem 2.11. Let (𝐿, ∧, ∨, ¬) be an ortholattice. (𝐿, ∧, ∨, ¬) is an orthomodular lattice if andonly if𝑝 ∨ 𝑞 = 𝑝 ∨ (¬𝑝 ∧ (𝑝 ∨ 𝑞)),for any 𝑝, 𝑞 ∈ 𝐿.
Proof. See [2, Theorem II.5.1], and use the absorption law.
Definition 2.12. Let ℒ1 = (𝐿1 , ∧1 , ∨1 , ¬1 ) and ℒ2 = (𝐿2 , ∧2 , ∨2 , ¬2 ) be ortholatices. Then,ℒ1 × ℒ2 = (𝐿1 × 𝐿2 , ∧, ∨, ¬)defined by(𝑝1 , 𝑝2 ) ∧ (𝑞1 , 𝑞2 ) = (𝑝1 ∧1 𝑞1 , 𝑞1 ∧2 𝑞2 ),(𝑝1 , 𝑝2 ) ∨ (𝑞1 , 𝑞2 ) = (𝑝1 ∨1 𝑞1 , 𝑞1 ∨2 𝑞2 ),¬(𝑝1 , 𝑝2 ) = (¬1 𝑝1 , ¬2 𝑝2 )is an ortholattice and is called the direct product of ℒ1 and ℒ2 .

3. Theoretical Background
The main contribution of this paper is to implement a support tool to verify the equivalence of
two terms in free orthomodular lattices. Its principle is based on two fundamental theorems
explained in this section. Although the first theorem (Theorem 3.3) has been employed forthe implementation in the previous work [14, 7], the second theorem (Theorem 3.4) is a newtheorem to be proved in this paper and has not been used in previous work. The second theorem
allows verifying the equivalence between a broader class of terms than existing work.

713.1. Free Algebra
Definition 3.1. Let 𝒞 be a non-empty class of algebras. An algebra 𝐹𝑋 ∈ 𝒞 is called a freealgebra in 𝒞 generated by 𝑋, if 𝐹𝑋 is generated by 𝑋 ⊆ 𝐹𝑋 and every function 𝑉 : 𝑋 → 𝐴 ∈ 𝒞
can be uniquely extended to a homomorphism 𝑉̂︀ : 𝐹𝑋 → 𝐴.
Example 3.2. The Boolean lattice 24 in Example 2.6 is a free Boolean lattice with two generators
𝑝 and 𝑞.
𝑛

In general, the free Boolean lattice with 𝑛 generators is the Boolean lattice 22 that consists𝑛of 22 elements [20, Theorem III.7].

3.2. The Word Problem for Various Free Lattices
The problem of deciding whether or not two given terms (words) of algebras are equivalent iscalled the word problem for the algebras. One possible way to check it is to try to reduce thetwo given terms to the same term in a finite number of steps.
The word problem for various kinds of lattices is one of the central topics in lattice theory. It
has been shown that the word problem for free lattices is solvable [21] (for more details, see [22]).
The following results have been obtained for various free lattices with some restrictions.
• The word problem for free distributive lattices is solvable [23].
• The word problem for free modular lattices with 𝑛 ≤ 3 generators is solvable (because
the free modular lattice with three generators has only 28 terms [24]), and that for freemodular lattices with 𝑛 ≥ 4 generators is unsolvable [25].
• The word problem for free ortholattices is solvable [26].
• The word problem for the free modular ortholattice with 𝑛 ≤ 2 generators is solvable(because the free modular ortholattice with two generators has only 96 terms [27]), andthat for general free modular ortholattices remains an open problem [28].
• The word problem for the free orthomodular lattice with 𝑛 ≤ 2 generators is solvable(because the free orthomodular lattice with two generators has only 96 terms [2, Theorem
III.2.8]), and that for general free modular ortholattices remains an open problem [12].
From the perspective of quantum mechanics, the word problem for free orthomodular lattices
is the most significant among the above-listed word problems. This is because the set of all
closed subspaces (experimental propositions [1]) of a Hilbert space is an orthomodular lattice [3,Proposition 4.5].

3.3. Two Fundamental Theorems for Orthomodular Lattices
To solve the word problem for some specific free orthomodular lattices, we use two fundamental
theorems for orthomodular lattices.
The first fundamental theorem states that there are only 96 normal forms in the free orthomodular lattice with two generators. This theorem has been used in previous work [14, 7].

72

Theorem 3.3. 𝑀 𝑂2 × 24 is isomorphic to the free orthomodular lattice with two generators.
Proof. See [2, Theorem III.2.8].
Because the number of normal forms in 𝑀 𝑂2 is 6 (recall Example 2.7) and that in 24 is 16(recall Example 2.6), that of 𝑀 𝑂2 × 24 is 6 × 16 = 96.
Also, Theorem 3.3 clarifies the relationship between any two normal forms. Let 𝑎 be anelement of 𝑀 𝑂2 distinct from ⋏ and ⋎, and 2 = ({⋏, ⋎}, ∧, ∨, ¬) be the two-element Boolean
lattice. Then, for example, 𝑝 (referred to as p22 ) and ¬𝑝 ∧ (𝑝 ∨ 𝑞) (referred to as p68 ) are normal
forms corresponding to (𝑎, ⋎, ⋎, ⋏, ⋏) and (¬𝑎, ⋏, ⋏, ⋎, ⋏) in 𝑀 𝑂2 × 2 × 2 × 2 × 2, which
is isomorphic to 𝑀 𝑂2 × 24 , respectively [2, Fig. 18]. Note that 𝑎 be an element of 𝑀 𝑂2 . By
definitions of 𝑀 𝑂2 and 2,(𝑎, ⋎, ⋎, ⋏, ⋏) ∨ (¬𝑎, ⋏, ⋏, ⋎, ⋏) = (⋎, ⋎, ⋎, ⋎, ⋏).
Here, (⋎, ⋎, ⋎, ⋎, ⋏) corresponds to 𝑝 ∨ 𝑞 [2, Fig. 18] (referred to as p92 = p22 ∨ p68 ), which isalso one of the 96 normal forms. Therefore, we obtain the result that𝑝 ∨ (¬𝑝 ∧ (𝑝 ∨ 𝑞)) = 𝑝 ∨ 𝑞holds in orthomodular lattices. In fact, this equation is the orthomodular law (recall Theorem 2.11). A list describing the relationship between any two normal forms is in [2, Fig.
18].
The second fundamental theorem tells us when the distributive law can be applied in orthomodular lattice. This is a new theorem proposed in this paper.
Theorem 3.4. Let (𝐿, ∧, ∨, ¬) be an orthomodular lattice. Then, the following are equivalent:
1. 𝑝 ∧ (𝑞 ∨ 𝑟) = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟);
2. 𝑝 ∧ (¬𝑝 ∨ 𝑞) = 𝑝 ∧ 𝑞.
Dually, the following are also equivalent:
1. 𝑝 ∨ (𝑞 ∧ 𝑟) = (𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑟);
2. 𝑝 ∨ (¬𝑝 ∧ 𝑞) = 𝑝 ∨ 𝑞.
Proof. We only prove the first part of the theorem. The dual part is shown similarly.
Proof of (1) ⇒ (2). By (1),𝑝 ∧ (¬𝑝 ∨ 𝑞) = (𝑝 ∧ ¬𝑝) ∨ (𝑝 ∧ 𝑞) = 𝑝 ∧ 𝑞.
Proof of (2) ⇒ (1). Recall that the distributive inequality(𝑝 ∧ 𝑞) ∨ (𝑝 ∧ 𝑟) ≤ 𝑝 ∧ (𝑟 ∨ 𝑞)
always holds even in non-distributive lattices (see [29, Exercise 2.9 (ii)]). Thus, 𝑝 ∧ (𝑞 ∨ 𝑟) is
an upper bound of {𝑝 ∧ 𝑞, 𝑝 ∧ 𝑟}. Thus, it remains to show that 𝑝 ∧ (𝑞 ∨ 𝑟) is the least upperbound of {𝑝 ∧ 𝑞, 𝑝 ∧ 𝑟}: 𝑝 ∧ (𝑞 ∨ 𝑟) ≤ 𝑠 for any upper bound 𝑠 of {𝑝 ∧ 𝑞, 𝑝 ∧ 𝑟}. Clearly,(𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠 ≤ 𝑝 ∧ (𝑞 ∨ 𝑟).

73

By applying the orthomodular law (Definition 2.10),
𝑝 ∧ (𝑞 ∨ 𝑟) = ((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ∨ ((¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠)) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟))).
Hence, it suffices to show(¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠)) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟)) = ⋏.
Because 𝑠 is an upper bound of {𝑝 ∧ 𝑞, 𝑝 ∧ 𝑟}, we obtain 𝑝 ∧ 𝑞 ≤ 𝑠 and 𝑝 ∧ 𝑟 ≤ 𝑠. Therefore,𝑝 ∧ 𝑞 = (𝑝 ∧ 𝑞) ∧ 𝑠 ≤ (𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠
and𝑝 ∧ 𝑟 = (𝑝 ∧ 𝑟) ∧ 𝑠 ≤ (𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠.
That is,¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ≤ ¬(𝑝 ∧ 𝑞) = ¬𝑝 ∨ ¬𝑞
and¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ≤ ¬(𝑝 ∧ 𝑟) = ¬𝑝 ∨ ¬𝑟.
It follows from the assumption (2) that¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟)) ≤ (¬𝑝 ∨ ¬𝑞) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟))= ((¬𝑝 ∨ ¬𝑞) ∧ 𝑝) ∧ (𝑞 ∨ 𝑟) = (𝑝 ∧ ¬𝑞) ∧ (𝑞 ∨ 𝑟).
Similarly, we have¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟)) ≤ (𝑝 ∧ ¬𝑟) ∧ (𝑞 ∨ 𝑟).
Consequently,¬((𝑝 ∧ (𝑞 ∨ 𝑟)) ∧ 𝑠) ∧ (𝑝 ∧ (𝑞 ∨ 𝑟)) ≤ ((𝑝 ∧ ¬𝑞) ∧ (𝑞 ∨ 𝑟)) ∧ ((𝑝 ∧ ¬𝑟) ∧ (𝑞 ∨ 𝑟))= (𝑝 ∧ (¬𝑞 ∧ ¬𝑟)) ∧ (𝑞 ∨ 𝑟) = 𝑝 ∧ (¬(𝑞 ∨ 𝑟) ∧ (𝑞 ∨ 𝑟)) = 𝑝 ∧ ⋏ = ⋏.

In the next section, we combine these two fundamental theorems to implement a support
tool.

4. Implementation
We develop a support tool in Maude [19] to check the word problem for free orthomodular
lattices. Maude is a high-performance specification/programming based on rewriting logic [30].
The language can directly specify order-sorted equational logic and rewriting logic, and it
provides several formal analysis methods, such as reachability analysis through a breadth-firstsearch of the reachable state space from a given state. The reachability analysis is performed
using the search command in Maude. In the support tool, we formally specify free orthomodular lattices, and develop an implementation of Theorem 3.3 and Theorem 3.4 to check the word
problem using the search command. This section gives the syntax of the Maude language ina nutshell (see [19] for more details) and briefly describes how the tool is developed.

74

4.1. Overview of Maude
Functional modules
A functional module ℳ specifies an order-sorted equational logic theory (Σ , E ) with the syntax:
fmod ℳ is (Σ , E ) endfm, where Σ is an order-sorted signature and E is the collection ofequations in the functional module. (Σ , E ) may contain a set of declarations as follows:• importations of previously defined modules (protecting . . . or extending . . . or
including . . .)• declarations of sorts (sort 𝑠 . or sorts 𝑠 𝑠′ .)• subsort declarations (subsort 𝑠 < 𝑠′ .)• declarations of function symbols (op 𝑓 : 𝑠1 . . . 𝑠𝑛 → 𝑠 [𝑎𝑡𝑡1 . . . 𝑎𝑡𝑡𝑘 ] .)• declarations of variables (vars 𝑣 𝑣 ′ .)• declarations of unconditional equations (eq 𝑡 = 𝑡′ .)• declarations of conditional equations (ceq 𝑡 = 𝑡′ if 𝑐𝑜𝑛𝑑 .)where 𝑠, 𝑠1 , . . . , 𝑠𝑛 are sort names, 𝑣, 𝑣 ′ are variable names, 𝑡, 𝑡′ are terms, 𝑐𝑜𝑛𝑑 is a conjunctionof equations (i.e., 𝑡 = 𝑡′ and/or 𝑡 => 𝑡′ ), and 𝑎𝑡𝑡1 , . . . 𝑎𝑡𝑡𝑘 are equational attributes. Equations
are used as equational rules to perform the simplification in which instances of the left-handside pattern are subterms of a subject term replaced by the corresponding instances of theright-hand side. The process is called term rewriting, and the result of simplifying a term iscalled its normal form.
System modules
A system module ℛ specifies a rewrite theory (Σ , E , R) with the syntax: mod ℛ is (Σ , E , R)
endm, where Σ and E are the same as those in an equational theory, and R is the collection ofrewrite rules in the system module. (Σ , E , R) may contain all possible declarations in (Σ , E )and rewrite rules in R as follows:• declarations of unconditional rewrite rules (rl [𝑙𝑏𝑙] : 𝑢 => 𝑣 .)• declarations of conditional rewrite rules (crl [𝑙𝑏𝑙] : 𝑢 => 𝑣 if 𝑐𝑜𝑛𝑑 .)where 𝑙𝑏𝑙 is the name of a rewrite rule, 𝑢, 𝑣 are terms, and 𝑐𝑜𝑛𝑑 is a conjunction of equations
and/or rewrites (e.g., 𝑡 => 𝑡′ ). rewrite rules are executed as rewriting from left to right modulo
the equations in the system module and are regarded as local transition rules, making possible
many state transitions from a given state as concurrent changes of a system.

75

Reachability analysis
The word problem of two terms 𝑡1 and 𝑡2 can be transformed into a reachability problem.
Suppose that 𝑡 =?= 𝑡 = true for any term 𝑡, then the word problem is to check whether
true is reachable from 𝑡1 =?= 𝑡2 referred to as 𝑡1 =?= 𝑡2 →*𝑅,𝐸 true, where 𝑅, 𝐸 are
the rewrite rules and equations in the specification of a system concerned. If that is the case, thetwo terms 𝑡1 and 𝑡2 are reduced to the same term in a finite number of rewrite steps, meaningthat the word problem is solved for 𝑡1 and 𝑡2 .
For the sake of simplicity, we use a Boolean lattice ℒ = (𝐿, ∧, ∨, ¬) as an example todemonstrate how to use the search command in Maude to tackle the reachability problem tosolve the word problem for ℒ. The following system module formally specifies ℒ.
mod BOOLEAN−LATTICE issort Lattice .
ops bot top : −> Lattice [ctor] .
op not_ : Lattice −> Lattice [prec 31] .
op _and_ : Lattice Lattice −> Lattice [assoc comm prec 32] .
op _or_ : Lattice Lattice −> Lattice [assoc comm prec 33] .
op _|−>_ : Lattice Lattice −> Lattice [prec 34] .
vars P Q R : Lattice .
rl [imply] : P |−> Q => not P or Q .
−−− Idempotent Laws
eq P and P = P .
eq P or P = P .
−−− Absorption Laws
eq P and (P or Q) = P .
eq P or (P and Q) = P .
−−− Orthocomplementation
eq P and not P = bot .
eq P or not P = top .
eq not(not P) = P .
eq not (P and Q) = not P or not Q .
eq not (P or Q) = not P and not Q .
−−− Distributive Laws
eq P or (Q and R) = (P or Q) and (P or R) .
eq P and (Q or R) = (P and Q) or (P and R) .
−−− Additional Identities
eq not top = bot .
eq not bot = top .
eq P and top = P .
eq P and bot = bot .
eq P or bot = P .
eq P or top = top .
−−− Checking Equivalence of Two Lattices
op true : −> Lattice [ctor] .
op _=?=_ : Lattice Lattice −> Lattice .
eq P =?= P = true .
endm

where the _and_, _or_, not_, bot, top operators represent ∧, ∨, ¬, ⋏, ⋎ in the Boolean lattice ℒ, respectively. P, Q, and R are Maude variables of the sort Lattice representing elementsof 𝐿. The assoc and comm attributes denote associative and commutative properties. The
prec_ attribute, where _ is a natural number, denotes the precedences of operators for parsing
in Maude (e.g., not P and Q or R is parsed as ((not P)and Q)or R without using
parentheses). The idempotent laws, absorption laws, distributive laws, involution, complements,

76

identities, and De Morgan’s laws are defined in the form of equations, while the implication
is defined in the form of a rewrite rule (see the rule imply). Although we should define theimplication using an equation, we intentionally use the rewrite rule imply intending to makeconcurrent changes in this example. For example, if a term consists of at least two sub-terms ofin the form of implication, either one of the two sub-terms can be rewritten using the rewrite
rule imply, making concurrent changes for the subject term. This is because rewrite rules
can be used instead of equations for equational reasoning. The _=?=_ operator is used forconstructing the initial term of the word problem in reachability analysis such that whenever
two terms at both sides of the operator are equivalent, it becomes true, which is a special
element of 𝑃 denoting the validity of the word problem.
We define some arbitrary elements of 𝑃 in the form of some operators (or fresh constants) in
the following module:
mod BOOLEAN−LATTICE−TEST is
pr BOOLEAN−LATTICE .
ops p q r : −> Lattice .
endm

We can verify the axiom (I3) of Abbott’s implication algebra [15] using the following commandin Maude.
search [1] p |−> (q |−> r) =?= q |−> (p |−> r) =>* true .

The command says that we would like to search on the reachable state space of ℒ from theinitial state p |−> (q |−> r)=?= q |−> (p |−> r) to check whether there is one
solution in which true is reachable from the initial state after zero or more rewrite steps. Notethat given the initial state as a term, the rewrite rule imply can be applied at four positions of
the term, making four possible successor states from the initial state as follows:(1) not p or (q |−> r) =?= q |−> p |−> r(2) p |−> (not q or r) =?= q |−> p |−> r(3) p |−> q |−> r =?= not q or (p |−> r)(4) p |−> q |−> r =?= q |−> (not p or r)

In this way, the reachable state space of ℒ from the initial state is constructed. The result of thecommand returns a solution and then we can conclude that the axiom (I3) is verified using thesearch command in Maude.

5. A Support Tool
We develop a support tool in Maude and use the search command to check the word problem
for free orthomodular lattices. The tool is publicly available at https://github.com/canhminhdo/
FOM. The basic idea of developing the tool is similar to what we have described above on
how to use the search command to verify the axiom (I3) in Maude. Moreover, we develop an
implementation of Theorem 3.3 and Theorem 3.4 in Maude to check the word problem for freeorthomodular lattices.
First, we prepare a formal specification of free orthomodular lattices in Maude, where someproperties are specified, such as associativity, commutativity, idempotency of ∧ and ∨, the77absorption laws, De Morgan’s laws, and so on. All properties are described by means of equationsin Maude. Let 𝐸FOM be the sets of equations from specifying free orthomodular lattices.
Second, we formalize Theorem 3.4 with the compatibility relation using rewrite rules. If thesubject term can be applied by the rewrite rules of Theorem 3.4 at multiple positions, the orderof applying the rewrite rules may produce different results in the end. Therefore, we specify
Theorem 3.4 using rewrite rules instead of equations to make concurrent changes in our system
so that all possible cases can be taken into account using reachability analysis. Moreover, we
may need to apply distributive laws from not only left to right but also right to left. If we use
equations to do so, it will make an infinite computation because of a loop caused by constantly
applying the equations from left to right and vice versa for a subject term if distributive laws
are applicable. Therefore, we use rewrite rules to specify Theorem 3.4. Let 𝑅DIST be the set of
rewrite rules obtained from specifying Theorem 3.4.
Third, we formalize the 96 normal forms (Theorem 3.3), and then automatically generate all
equations for each p𝑖 ∧ p𝑗 , p𝑖 ∨ p𝑗 , and ¬p𝑖 that is again an element p𝑘 , where p𝑖 , p𝑗 , p𝑚 , andp𝑘 are elements of the 96 normal forms in [2, Fig. 18]. Because ¬p𝑖 can be obtained throughapplying De Morgan’s laws specified in 𝐸FOM , then we do not need to construct equations for¬p𝑖 of 96 normal forms. Hence, we only focus on generating equations for p𝑖 ∧ p𝑗 and p𝑖 ∨ p𝑗 .
For example, p92 = p22 ∨ p68 (see Subsection 3.3 for more details), and thus we can obtain thefollowing equation:
eq P or (not P and (P or Q)) = P or Q .

where P and Q are variables representing elements of free orthomodular lattices. Let 𝐸NF
be the set of equations obtained from generating all equations of the 96 normal forms. Notethat the left-hand side of each generated equation is simplified by using 𝐸FOM beforehandand unnecessary equations (e.g., eq P = P .) are removed. Hence, there are 5,520 distinct
equations in 𝐸NF generated automatically by the support tool.
Now the word problem is rephrased as the reachability problem 𝑡1 =?= 𝑡2 →*𝑅,𝐸 true
with the relation →*𝑅,𝐸 that is →*𝑅DIST ,𝐸FOM ∪𝐸NF .

6. Case Studies
We apply the support tool to show that some axioms with three free variables in several
implication algebras [16, 18, 15, 17] are valid. In these experiments, we used one node incomputing servers available at our institute that carries a 2.8 GHz microprocessor with 64 coresand 1.5 TB memory of RAM.
Before that, we briefly explain what implication algebras are. The operators ∧, ∨, and ¬ inorthomodular lattices (also in Boolean lattices) correspond to conjunction, disjunction, andnegation, respectively. In Boolean lattices (𝐿, ∧, ∨, ¬), the operator → (material implication)
on 𝑃 is defined by 𝑝 → 𝑞 = ¬𝑝 ∨ 𝑞. This operator → satisfies all the minimal requirements for
implication called the minimal implicative criteria:
1. 𝑝 ≤ 𝑞 implies 𝑝 → 𝑞 = ⋎;2. (Modus Ponens) 𝑝 ∧ (𝑝 → 𝑞) ≤ 𝑞;78

3. (Modus Tollens) ¬𝑞 ∧ (𝑝 → 𝑞) ≤ ¬𝑝.
On the other hand, in orthomodular lattices, there are three implication operators ⇝ (Sasaki implication [31] or quasi implication [15]), ↣ (Dishkant implication [18] or ortho-implication [16]),and ↠ (relevance implication [18]) that satisfy the minimal implicative criteria [3, Chapter 8]
defined by𝑝 ⇝ 𝑞 = ¬𝑝 ∨ (𝑝 ∧ 𝑞), 𝑝 ↣ 𝑞 = (¬𝑝 ∧ ¬𝑞) ∨ 𝑞,
𝑝 ↠ 𝑞 = ((𝑝 ∧ 𝑞) ∨ (¬𝑝 ∧ 𝑞)) ∨ (¬𝑝 ∧ ¬𝑞).
Note that all these three implication operators coincide with 𝑝 → 𝑞 in Boolean lattices (using
the distributive law).
For each implication satisfying the minimal implicative criteria, algebras that the only operator
is the implication (and ⋏) have been proposed and are called implication algebras. All the axiomsof these implication algebras are satisfied in orthomodular lattices by translating an implication
into a term in orthomodular lattices (for example, 𝑝 ⇝ 𝑞 is translated into ¬𝑝 ∨ (𝑝 ∧ 𝑞)).
Because any axioms that consist of two variables can be verified by existing tool [14, 7], we
confine our attention to axioms that consist of three variables in several implication algebras:• The axiom (Q2) of quasi-implication algebra [15]:(𝑝 ⇝ 𝑞) ⇝ (𝑝 ⇝ 𝑟) = (𝑞 ⇝ 𝑝) ⇝ (𝑞 ⇝ 𝑟).
• The axiom (O2) of ortho-implication algebra [16]:𝑝 ↣ ((𝑞 ↣ 𝑝) ↣ 𝑟) = 𝑝 ↣ 𝑟.
• The axiom (O5) of orthomodular implication algebra [17]:(((𝑝 ↣ 𝑞) ↣ 𝑞) ↣ 𝑟) ↣ (𝑝 ↣ 𝑟) = ⋎• The axiom (O6) of orthomodular implication algebra [17]:(((((((((𝑝 ↣ 𝑞) ↣ 𝑞) ↣ 𝑟) ↣ 𝑟) ↣ 𝑟) ↣ 𝑝) ↣ 𝑝) ↣ 𝑟) ↣ 𝑝) ↣ 𝑝= (((𝑝 ↣ 𝑞) ↣ 𝑞) ↣ 𝑟) ↣ 𝑟• The axiom (J4) of Sasaki implication algebra [18]:𝑝 ⇝ ((𝑝 ⇝ ((𝑞 ⇝ ((𝑞 ⇝ 𝑟) ⇝ ⋏)) ⇝ ⋏)) ⇝ ⋏)= 𝑟 ⇝ ((𝑟 ⇝ ((𝑝 ⇝ ((𝑝 ⇝ 𝑞) ⇝ ⋏)) ⇝ ⋏)) ⇝ ⋏).
• The axiom (K5) of Dishkant implication algebra [18]:(((𝑝 ↣ 𝑞) ↣ 𝑞) ↣ 𝑟) ↣ 𝑟 = (𝑝 ↣ ((𝑞 ↣ 𝑟) ↣ 𝑟)) ↣ ((𝑞 ↣ 𝑟) ↣ 𝑟).
• The axiom (L6) of relevance implication algebra [18]:(((𝑝 ↠ 𝑞) ↠ 𝑞) ↠ 𝑟) ↠ 𝑟 = (𝑝 ↠ ((𝑞 ↠ 𝑟) ↠ 𝑟)) ↠ ((𝑞 ↠ 𝑟) ↠ 𝑟).

79

Table 1
Experimental results for validating some axioms with our support toolTime
1,213ms
736ms
705ms
716ms
715ms
723ms
6d:19h:40m

Target Axiom
The axiom (Q2) in [15]The axiom (O2) in [16]The axiom (O5) in [17]The axiom (O6) in [17]The axiom (J4) in [18]The axiom (K5) in [18]The axiom (L6) in [18]The experimental data for checking these axioms are shown in Table 1. The first and second
columns denote the name of each axiom and the time taken to validate each axiom using
our support tool. For the first six axioms, our tool can quickly verify their validity for a few
moments, which is almost impossible to do so without the aid of computer programs, especiallythe axioms (O5), (J4), and (K5). For the last axiom (L6), our tool needs to spend six days, 19
hours, and 40 minutes to verify its validity because of its complexity, making a huge state spacein the reachability analysis. In summary, we can conclude the validity of axioms (Q2), (O2),(O5), (J4), and (K5) using our support tool. Transforming the word problem into a reachability
problem and the use of not only the 96 normal forms (Theorem 3.3) but also Theorem 3.4 forthe applicability of distributive laws make our tool extremely useful and distinguishable fromexisting tools for checking the word problem in free orthomodular lattices.

7. Related WorkIn [14], a program is implemented to reduce a term in the free orthomodular lattice 𝐹 (𝑝, 𝑞)
with two generators 𝑝 and 𝑞 to the normal (canonical) form. It relies on the fact that 𝐹 (𝑝, 𝑞)
consists of the 96 normal forms (Theorem 3.3) [2].
After that, in [7], a program that can reduce a term in the free orthomodular lattice
𝐹 (𝑝, 𝑞, 𝑟1 , . . . , 𝑟𝑛 ) generated by 𝑛 + 2 terms 𝑝, 𝑞, 𝑟1 , . . . , 𝑟𝑛 , where 1 ≤ 𝑛 ≤ 9, and each𝑟𝑖 commutes with all other generators. Note that 𝑝 is said to commute with 𝑞, denoted by 𝑝𝐶𝑞,if
𝑝 = (𝑝 ∧ 𝑞) ∨ (𝑝 ∧ ¬𝑞).
The implementation in [7] relies on the fact that 𝐹 (𝑝, 𝑞, 𝑟1 , . . . , 𝑟𝑛 ) is isomorphic to thedirect product of 2𝑛 copies of 𝐹 (𝑝, 𝑞) [32]. Different from the program in [14], that in [7]makes it possible to verify a much broader class of theorems in orthomodular lattice theory [6],such as the Foulis-Holland theorem [4, 5] and a theorem [2, Corollary VII.7.7] about skew join
and skew meet. In addition, some problems, such as verification of associative operators [9],monotonic operators [10], and weak associative operators [11] of operations on orthomodular
lattices, which can be reduced to verification of terms in 𝐹 (𝑝, 𝑞, 𝑟1 , . . . , 𝑟𝑛 ) are solved using
the program in [7].
Although both implementations in [14] and [7] can help to solve various problems, they still
have limitations: that in [14] can only deal with terms consisting of two generators, and that80

in [7] can only deal with terms in a free orthomodular lattice with restricted generators.
Our tool can overcome these limitations when three or more generators are allowed to be
used in terms. Based on Theorem 3.3 and 3.4, our tool effectively checks the word problem infree orthomodular lattices without any restrictions and can cover a broader class of the word
problems compared to existing tools.

8. Conclusion
Using a reachability analysis, we have described how to develop the support tool for checking
the word problem with three or more generators for free orthomodular lattices. The tool
implemented in Maude consists of the formal specification of free orthomodular lattices and theimplementation of two fundamental theorems (Theorem 3.3 and Theorem 3.4). We have used
the search command in Maude to conduct the reachability analysis to conclude the validity
of some complicated theorems, demonstrating the power of our support tool.

Acknowledgments
The research of the first author was supported by Grant-in-Aid for JSPS Research Fellow Grant
Number JP22KJ1483. The research of the second and the third authors was supported by JST
SICORP Grant Number JPMJSC20C2 and JSPS KAKENHI Grant Number JP24H03370.

References[1] G. Birkhoff, J. von Neumann, The logic of quantum mechanics, Annals of mathematics 57(1936) 823–843.
[2] L. Beran, Orthomodular lattices: algebraic approach, volume 18 of Mathematics and its
Applications, 1985.
[3] M. Rédei, Quantum logic in algebraic approach, volume 91 of Fundamental Theories ofPhysics, Springer, 1998.
[4] D. J. Foulis, A note on orthomodular lattices, Portugaliae mathematica 21 (1962) 65–72.
[5] S. S. Holland, A radon-nikodym theorem in dimension lattices, Transactions of theAmerican Mathematical Society 108 (1963) 66–87.
[6] M. Hyčko, M. Navara, Decidability in orthomodular lattices, International Journal of
Theoretical Physics 44 (2005) 2239–2248.
[7] M. Hyčko, Implications and equivalences in orthomodular lattices, Demonstratio Mathematica 38 (2005) 777–792.
[8] N. D. Megill, M. Pavičić, Quantum implication algebras, International Journal of Theoretical
Physics 42 (2003) 2807–2822.
[9] J. Gabriëls, M. Navara, Associativity of operations on orthomodular lattices, Mathematica
Slovaca 62 (2012) 1069–1078.
[10] J. J. Gabriëls, M. Navara, Computer proof of monotonicity of operations on orthomodular
lattices, Information Sciences 236 (2013) 205–217.

81

[11] S. M. Gagola, J. J. Gabriëls, M. Navara, Weaker forms of associativity in orthomodular
lattices, Algebra universalis 73 (2015) 249–266.
[12] G. Bruns, J. Harding, Algebraic aspects of orthomodular lattices, in: Current researchin operational quantum logic, volume 111 of Fundamental Theories of Physics, 2000, pp.
37–65.
[13] R. Freese, J. Ježek, J. B. Nation, Term rewrite systems for lattice theory, Journal of Symbolic
Computation 16 (1993) 279–288.
[14] N. D. Megill, M. Pavičić, Orthomodular lattices and a quantum algebra, International
Journal of Theoretical Physics 40 (2001) 1387–1410.
[15] G. M. Hardegree, Quasi-implication algebras, part I: Elementary theory, Algebra Universalis
12 (1981) 30–47.
[16] J. C. Abbott, Orthoimplication algebras, Studia Logica 35 (1976) 173–177.
[17] I. Chajda, R. Halas̆, H. Länger, Orthomodular implication algebras, International Journalof Theoretical Physics 40 (2001) 1875–1884.
[18] G. N. Georgacarakos, Equationally definable implication algebras for orthomodular lattices,
Studia Logica 39 (1980) 5–18.
[19] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott (Eds.), All
About Maude - A High-Performance Logical Framework, How to Specify, Program andVerify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science, 2007.
[20] G. Birkhoff, Lattice theory, volume 25, third ed., American Mathematical Society, 1940.
[21] P. M. Whitman, Free lattices, Annals of Mathematics 42 (1941) 325–330.
[22] R. Freese, J. Ježek, J. B. Nation, Free lattices, volume 42 of Mathematical Surveys andMonographs, American Mathematical Society, 1995.
[23] K. Takeuchi, The word problem for free distributive lattices, Journal of the MathematicalSociety of Japan 21 (1969) 330–333.
[24] R. Dedekind, Ueber die von drei moduln erzeugte dualgruppe, Mathematische Annalen 53(1900) 371–403.
[25] C. Herrmann, On the word problem for the modular lattice with four free generators,
Mathematische Annalen 265 (1983) 513–527.
[26] G. Bruns, Free ortholattices, Canadian Journal of Mathematics 28 (1976) 977–985.
[27] J. Kotas, An axiom system for the modular logic, Studia Logica 21 (1967) 17–38.
[28] M. S. Roddy, On the word problem for orthocomplemented modular lattices, Canadian
Journal of Mathematics 41 (1989) 961–1004.
[29] B. A. Davey, H. A. Priestley, Introduction to lattices and order, 2nd ed., Cambridge University Press, 2002.
[30] J. Meseguer, Twenty years of rewriting logic, J. Log. Algebraic Methods Program. 81 (2012)
721–781.
[31] L. Herman, E. Marsden, R. Piziak, Implication connectives in orthomodular lattices., Notre
Dame Journal of Formal Logic 16 (1975) 305–328.
[32] M. Navara, On generating finite orthomodular sublattices, Tatra Mountains Mathematical
Publications 10 (1997) 109–117.

82

Theoretical Foundation for Equivalence Checking of
Quantum Circuits
Canh Minh Do* , Kazuhiro Ogata
Japan Advanced Institute of Science and Technology, 1-8 Asahidai, Nomi, Japan

Abstract

Quantum circuits are typically used to design quantum algorithms at a high abstraction level without
considering specific hardware restrictions. To execute quantum circuits on an actual quantum device, theymust undergo a compilation process, transforming the high abstraction level into a low abstraction levelthat conforms to all restrictions imposed on the target device. As a result, the original quantum circuits
and their compiled counterparts differ significantly. Therefore, it is crucial to verify the equivalence of
two quantum circuits constructed from quantum gates based on their functionality. This paper presents
a theoretical foundation for checking the equivalence of quantum circuits based on which an algorithm
is constructed. The equivalence of quantum circuits can be reduced to matrix equivalence modulo a
global phase. To achieve this, we compare each column vector of two matrices modulo the same global
phase, making it significantly faster than the actual matrix equivalence check, especially in cases ofnon-equivalent quantum circuits.

Keywords

Observable Equivalence, Density Matrices, Equivalence Checking, Quantum Circuits

1. Introduction
Quantum computing is a rapidly emerging technology that uses the principles of quantum
mechanics to solve complex problems beyond the capabilities of current classical computing.
Several quantum algorithms have been proposed, showing significant improvements overclassical algorithms, such as Shor’s fast algorithms for discrete logarithms and factoring in
1994 [1]. Although practical quantum computers capable of running such algorithms effectively
are not yet available, recent exponential investments from big companies like IBM, Google,
Microsoft, and Intel bring the future of the quantum era within closer reach.
Quantum circuits are a natural model of quantum computation, comprising qubits andquantum operations (e.g., quantum gates), that can be used to design and implement quantum
algorithms. However, quantum circuits are typically used to design quantum algorithms at
a high abstraction level without considering specific hardware restrictions. To execute thequantum circuits on an actual quantum device, they have to undergo a compilation process,transforming the high abstraction level to a low abstraction level that conforms to all restrictions
The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, November 11, 2023, Brisbane, Australia*
Corresponding author.
$ canhdo@jaist.ac.jp (C. M. Do); ogata@jaist.ac.jp (K. Ogata) 0000-0002-1601-4584 (C. M. Do); 0000-0002-4441-3259 (K. Ogata)83

imposed on the targeted device. More precisely, this compilation process has several key aspects
as follows. Firstly, quantum devices natively support only a limited set of quantum operations.
Consequently, quantum circuits intended for the target device must be expressed using only
these native quantum operations. This requires a decomposition (or translation) step of nonnative quantum operations into sequences of native ones [2, 3, 4]. Secondly, logical qubits
used in quantum circuits have to be mapped to physical qubits on the target device. However,this mapping cannot be arbitrary because the target device imposes restrictions on which
physical qubits can interact with each other. To achieve this, a mapping (or routing) step isrequired, which involves adding SWAP and Hadmard gates to quantum circuits [5, 6, 7]. Lastly,
after the decomposition and mapping steps, the size of quantum circuits tends to increase,posing challenges for their execution on quantum devices due to noise and decoherence effects.
Therefore, an optimization step is required to reduce the size of quantum circuits in terms of thenumber of quantum gates [8, 9, 10]. As a result of these processes, the quantum circuit definedat a high abstraction level and its compiled counterpart defined at a low abstraction level are
significantly different. Therefore, it is crucial to verify the equivalence of two quantum circuits
based on their functionality.
The functionality of quantum circuits can be described by a sequence of quantum gates,
which are represented by unitary matrices. Given two quantum circuits constructed from′ . . . 𝑈 ′ , the two quantum circuits
quantum gates in the form of 𝑈 = 𝑈𝑚 . . . 𝑈0 and 𝑈 ′ = 𝑈𝑚′
0are considered equivalent if 𝑈 is equal to 𝑈 ′ modulo a global phase, which is physicallyunobservable [11]. Directly comparing 𝑈 and 𝑈 ′ is inefficient because it requires costly matrix′ . . . 𝑈 ′ to obtain 𝑈 and 𝑈 ′ for comparison. Moreover,matrix multiplications 𝑈𝑚 . . . 𝑈0 and 𝑈𝑚′
0
if 𝑈 is significantly different from 𝑈 ′ , constructing the entire elements of both matrices is
unnecessary. Instead, we can compare each column of two matrices modulo a global phase.
Concretely, for each basis vector |𝜑𝑖 ⟩ in an orthonormal basis of a Hilbert space, if 𝑈 |𝜑𝑖 ⟩ isequal to 𝑈 ′ |𝜑𝑖 ⟩ modulo the same global phase, then the two quantum circuits are equivalent. It
is important to note that we may need a few iterations to check that some quantum circuits
are not equivalent in cases of non-equivalent quantum circuits, making it significantly fasterthan the actual matrix equivalence check. We present a theoretical foundation for checking theequivalence of quantum circuits with a theorem to guarantee the correctness of our approach.
An algorithm is also constructed based on our theorem.
The rest of the paper is organized as follows: Sect. 2 provides the basics of quantum mechanics
related mostly to linear algebra, Sect. 3 proposes a theoretical foundation of equivalence checkingof quantum circuits in this work based on which an algorithm is constructed, Sect. 4 presents
some existing work, and Sect. 5 concludes the paper with some pieces of future work.

2. Basic Quantum Mechanics
In classical computing, the fundamental unit of information is a bit whose value is either 0
or 1. In quantum computing, the counterpart is a quantum bit or qubit, which has two basis
states, conventionally(︃ )︃
(︃ )︃written in Dirac notation [12] as |0⟩ and |1⟩, which denote two column
10vectorsand, respectively. In quantum theory, a general state of a quantum system0184

is a superposition or linear combination of basis states. A quantum state is a unit vector in a
Hilbert space ℋ, which is a vector space equipped with an inner product such that each Cauchy
sequence has a limit. The state of a single qubit is |𝜓⟩ = 𝛼 |0⟩ + 𝛽 |1⟩, where 𝛼 and 𝛽 are22complex numbers such that(︃ |𝛼|)︃ + |𝛽| = 1. States can be represented by column complex𝛼vectors as follows: |𝜓⟩ == 𝛼 |0⟩ + 𝛽 |1⟩, where {|0⟩ , |1⟩} forms an orthonormal basis
𝛽of the two-dimensional complex vector space.
The basis {|0⟩ , |1⟩} is called as the standard basis. Besides, there are some other orthonormalbases studied in the literature, such as diagonal (or dual, or Hadamard) basis consisting of thefollowing vectors:|+⟩ = √12 (|0⟩ + |1⟩) and |−⟩ = √12 (|0⟩ − |1⟩)
The evolution of a closed quantum system can be performed by a unitary transformation.
If the state of a qubit is represented by a column vector, then a unitary transformation 𝑈 canbe represented by a complex-value matrix such that 𝑈 𝑈 † = 𝑈 † 𝑈 = 𝐼 or 𝑈 † = 𝑈 −1 , where𝑈 † is the conjugate transpose of 𝑈 . 𝑈 acts on the Hilbert space ℋ transforming a state |𝜓⟩to a state |𝜓 ′ ⟩ by a matrix multiplication such that |𝜓 ′ ⟩ = 𝑈 |𝜓⟩. There are some frequently
used quantum gates in applications: the Hadamard gate 𝐻, the identity gate 𝐼, the Pauli gates
𝑋, 𝑌 , and 𝑍, and the controlled-NOT gate CX . Note that the CX gate performs on two
qubits, while the remaining gates perform on a single qubit. Their matrix representations are as
follows:
(︃
)︃
(︃
)︃
(︃
)︃
1 0
0 1
0 −𝑖
𝐼2 =
,
𝑋=
,
𝑌 =
,
0 1
1 0
𝑖 0
⎛
⎞
1 0 0 0
⎜
⎟
(︃
(︃
)︃
)︃
⎜0 1 0 0⎟
1 1
1 0
⎜
⎟
1
𝑍=
,
𝐻 = √2,
𝐶𝑋 = ⎜
⎟.
⎜
⎟
0 −1
1 −1
0
0
0
1
⎝
⎠
0 0 1 0where 𝑖 is the imaginary unit. For example, the Hadamard gate on a single qubit performs the
mapping |0⟩ ↦→ √12 (|0⟩ + |1⟩) and |1⟩ ↦→ √12 (|0⟩ − |1⟩). The controlled-NOT gate on pairs ofqubits performs the mapping |00⟩ ↦→ |00⟩ , |01⟩ ↦→ |01⟩ , |10⟩ ↦→ |11⟩ , |11⟩ ↦→ |10⟩, which
can be understood as inverting the second qubit (referred to as the target) if and only if the first
qubit (referred to as the control) is one.
For multiple qubits, we use the tensor product of Hilbert spaces. Let ℋ1 and ℋ2 be two
Hilbert spaces. Their tensor product ℋ1 ⊗ ℋ2 is defined as a vector space consisting of linear
combinations of the vectors |𝜓1 𝜓2 ⟩ = |𝜓1 ⟩ |𝜓2 ⟩ = |𝜓1 ⟩⊗|𝜓2 ⟩, where |𝜓1 ⟩ ∈ ℋ1 and |𝜓2 ⟩ ∈ ℋ2 .
Systems of two or more qubits may be in entangled states, meaning that states of qubits arecorrelated and inseparable. Entanglement shows that an entangled state of two qubits cannot
be expressed as a tensor product of single-qubit states. We can use 𝐻 and CX gates to create
entangled states as follows: 𝐶𝑋((𝐻 ⊗ 𝐼) |00⟩) = √12 (|00⟩ + |11⟩).

85

Let |𝜓⟩ be a quantum state and 𝜃 ∈ [0, 2𝜋). In quantum mechanics, the state 𝑒𝑖𝜃 |𝜓⟩ isconsidered to be physically equal to |𝜓⟩ with respect to the global phase factor 𝑒𝑖𝜃 . From an
observable perspective, two states are undistinguishable if they differ only by a global phase.
We can use density matrices |𝜓⟩⟨𝜓| to present quantum states |𝜓⟩ from which we can eliminate
the global phase factor as follows: 𝑒𝑖𝜃 |𝜓⟩ (𝑒𝑖𝜃 |𝜓⟩)† = 𝑒𝑖𝜃 |𝜓⟩ 𝑒−𝑖𝜃 ⟨𝜓| = |𝜓⟩⟨𝜓|.

3. Equivalence Checking of Quantum Circuits
This section presents the theoretical foundation of equivalence checking of quantum circuits byintroducing a theorem based on which an algorithm is constructed.

3.1. Theoretical Foundation
We propose a method for checking the equivalence of quantum circuits constructed fromquantum gates based on their functionality. We suppose that quantum circuits operate on
quantum states in a Hilbert space ℋ with 𝑛 qubits. The unitary evolution of quantum systems
is described by unitary matrices whose size is 2𝑛 × 2𝑛 . We first define the equivalence checking
problem of quantum circuits.
Definition 3.1 (Equivalence checking problem). Given two quantum circuits represented by′ . . . 𝑈 ′ , the equivalence checking problem of 𝑈
unitary matrices, 𝑈 = 𝑈𝑚 . . . 𝑈0 and 𝑈 ′ = 𝑈𝑚
′
0
′
𝑖𝜃
′
and 𝑈 is asked to check whether 𝑈 = 𝑒 𝑈 for some 𝜃 ∈ [0, 2𝜋).
We call 𝑒𝑖𝜃 a global phase that is physically unobservable [11]. In quantum mechanics,
quantum states that differ only by a global phase are physically indistinguishable and equivalent
under observation [11]. Hence, we define observable equivalence for quantum states as follows:
Definition 3.2 (Observable equivalence for quantum states). |𝜓⟩ ≈ |𝜓 ′ ⟩ (or |𝜓⟩ ≈𝜃 |𝜓 ′ ⟩ tomake it clear from the context) is defined as |𝜓⟩ = 𝑒𝑖𝜃 |𝜓 ′ ⟩ for some 𝜃 ∈ [0, 2𝜋).
To check |𝜓⟩ ≈ |𝜓 ′ ⟩, we can check the equality of their density matrices |𝜓⟩⟨𝜓| and |𝜓 ′ ⟩⟨𝜓 ′ |.
Because using density matrices to represent quantum states can eliminate the global phase, it isa handy trick to check the observable equivalence of two quantum states by comparing theirdensity matrices. This result is derived from the following lemma.
Lemma 3.1. |𝜓⟩ ≈ |𝜓 ′ ⟩ if and only if |𝜓⟩⟨𝜓| = |𝜓 ′ ⟩⟨𝜓 ′ |.
Proof. For the ‘only if ’ part (the ⇒ direction), it is straightforward.
We now consider the ‘if ’ part (the ⇐ direction). Let {|𝜑0 ⟩ , . . . , |𝜑𝑖 ⟩ , . . . |𝜑2𝑛 −1 ⟩} be an
orthonormal basis of ℋ with 𝑛 dimension. There exists 𝑐0 , . . . , 𝑐𝑖 , . . . , 𝑐2𝑛 −1 such that |𝜓⟩ =𝑐0 |𝜑0 ⟩ + · · · + 𝑐𝑖 |𝜑𝑖 ⟩ + · · · + 𝑐2𝑛−1 |𝜑2𝑛 −1 ⟩ and |𝑐0 |2 + · · · + |𝑐𝑖 |2 + · · · + |𝑐2𝑛 −1 |2 = 1. Similarly,
we have |𝜓 ′ ⟩ = 𝑐′0 |𝜑0 ⟩ + · · · + 𝑐′𝑖 |𝜑𝑖 ⟩ + · · · + 𝑐′2𝑛−1 |𝜑2𝑛 −1 ⟩. Let A and A’ be 2𝑛 × 2𝑛 matrices
denoting |𝜓⟩⟨𝜓| and |𝜓 ′ ⟩⟨𝜓 ′ |, respectively. The elements of matrix A are calculated as follows:
𝑎𝑖𝑗 = ⟨𝜑𝑖 | 𝐴 |𝜑𝑗 ⟩= ⟨𝜑𝑖 |𝜓⟩ ⟨𝜓|𝜑𝑗 ⟩86

= 𝑐𝑖 𝑐*𝑗
Similarly, the elements of matrix A’ are calculated as follows: 𝑎′𝑖𝑗 = 𝑐′𝑖 𝑐′*𝑗 .
′𝑛
We have 𝑎𝑖𝑗 = 𝑎𝑖𝑗 for any 𝑖, 𝑗 ∈ [0 . . . 2 − 1] because of A = A’ from the assumption. Let us
consider 𝑎𝑖𝑖 = 𝑎′𝑖𝑖 as follows:
𝑎𝑖𝑖 = 𝑎′𝑖𝑖
⇔ 𝑐𝑖 𝑐*𝑖 = 𝑐′𝑖 𝑐′*𝑖′′⇔ 𝑟𝑒𝑖𝛼 (𝑟.𝑒𝑖𝛼 )* = 𝑟′ 𝑒𝑖𝛼 (𝑟′ 𝑒𝑖𝛼 )*⇔𝑟=𝑟(by the exponential form of complex numbers)′(because r and r’ are non-negative numbers)′

We have 𝑐𝑖 = 𝑟𝑒𝑖𝛼 , 𝑐′𝑖 = 𝑟′ 𝑒𝑖𝛼 , and 𝑟 = 𝑟′ , where 𝑖 ∈ [0 . . . 2𝑛 − 1]. Let us consider two cases:• If 𝑟 = 𝑟′ = 0, then it is immediate that 𝑐𝑖 = 𝑒𝑖𝜃𝑖 𝑐′𝑖 for some 𝜃𝑖 ∈ [0, 2𝜋).
𝑖𝛼′𝑖(𝛼−𝛼 ) = 𝑒𝑖𝜃𝑖 , where 𝜃 = 𝛼 − 𝛼′ . Then, we• If 𝑟 = 𝑟′ ̸= 0, then we have 𝑐𝑐𝑖′ = 𝑟𝑟𝑒𝑖′ 𝑒𝑖𝛼′ = 𝑒𝑖have 𝑐𝑖 = 𝑒𝑖𝜃𝑖 𝑐′𝑖 for some 𝜃𝑖 ∈ [0, 2𝜋).

Therefore, for all 𝑖 ∈ [0 . . . 2𝑛 − 1], there exists 𝜃𝑖 ∈ [0, 2𝜋) such that 𝑐𝑖 = 𝑒𝑖𝜃𝑖 𝑐′𝑖 . Now let us
consider 𝑎𝑖𝑗 = 𝑎′𝑖𝑗 as follows:
𝑎𝑖𝑗 = 𝑎′𝑖𝑗
⇔ 𝑐𝑖 𝑐*𝑗 = 𝑐′𝑖 𝑐′*𝑗⇔ 𝑒𝑖𝜃𝑖 𝑐′𝑖 (𝑒𝑖𝜃𝑗 𝑐′𝑗 )* = 𝑐′𝑖 𝑐′*𝑗(by the result above)′ ′*⇔ 𝑒𝑖(𝜃𝑖 −𝜃𝑗 ) 𝑐′𝑖 𝑐′*
𝑗 = 𝑐𝑖 𝑐𝑗

Therefore, we have 𝜃𝑖 = 𝜃𝑗 for any 𝑐𝑖 , 𝑐𝑗 ̸= 0. It indicates that |𝜓⟩ = 𝑒𝑖𝜃 |𝜓 ′ ⟩ for some𝜃 ∈ [0, 2𝜋). From Definition 3.2, we have |𝜓⟩ ≈ |𝜓 ′ ⟩.
Recall to check the equivalence of quantum circuits 𝑈 and 𝑈 ′ , we need to check whether
𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋). We can use the following lemma to solve this problem.
Lemma 3.2. Let 𝑈 and 𝑈 ′ be 2𝑛 × 2𝑛 unitary matrices, then 𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋)
if and only if 𝑈 |𝜓⟩ ≈𝜃 𝑈 ′ |𝜓⟩ for any vector |𝜓⟩ ∈ ℋ.
Proof. For the ‘only if ’ part (the ⇒ direction), for any |𝜓⟩, we have 𝑈 |𝜓⟩ = 𝑒𝑖𝜃 𝑈 ′ |𝜓⟩ for some𝜃 ∈ [0, 2𝜋) using the assumption. From Definition 3.2, we have 𝑒𝑖𝜃 𝑈 ′ |𝜓⟩ ≈ 𝑈 ′ |𝜓⟩. Therefore,
𝑈 |𝜓⟩ ≈𝜃 𝑈 ′ |𝜓⟩.
For the ‘if ’ part (the ⇐ direction), because 𝑈 |𝜓⟩ ≈𝜃 𝑈 ′ |𝜓⟩ for any |𝜓⟩ from the assumption,
we have 𝑈 |𝜓⟩ = 𝑒𝑖𝜃 𝑈 ′ |𝜓⟩ for some 𝜃 ∈ [0, 2𝜋). Therefore, 𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋).

87

In Lemma 3.2, it is unfeasible to consider any vector |𝜓⟩ ∈ ℋ because there are infinite
vectors in ℋ. Therefore, we introduce the following lemma to help us check whether 𝑈 = 𝑒𝑖𝜃 𝑈 ′by considering only basis vectors in an orthonormal basis of ℋ. If the dimension of ℋ is 𝑛, we
need to consider at most 2𝑛 basis vectors with respect to the same global phase.
Lemma 3.3. Let 𝑈 and 𝑈 ′ be 2𝑛 × 2𝑛 matrices, then 𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋) if andonly if 𝑈 |𝜑𝑖 ⟩ ≈𝜃 𝑈 ′ |𝜑𝑖 ⟩ for each basis vector |𝜑𝑖 ⟩ in an orthonormal basis of ℋ.
Proof. The ‘only if ’ part (the ⇒ direction) is immediate from Lemma 3.2.
For the ‘if ’ part (the ⇐ direction), let {|𝜑0 ⟩ , . . . , |𝜑𝑖 ⟩ , . . . |𝜑2𝑛 −1 ⟩} be an orthonormal basis ofℋ with 𝑛 dimension. For each basis vector 𝜑𝑖 , we have 𝑈 |𝜑𝑖 ⟩ ≈𝜃 𝑈 ′ |𝜑𝑖 ⟩ from the assumption.
From Definition 3.2, we have 𝑈 |𝜑𝑖 ⟩ = 𝑒𝑖𝜃 𝑈 ′ |𝜑𝑖 ⟩ for some 𝜃 ∈ [0, 2𝜋). Therefore, for any
complex number 𝑐𝑖 , we have 𝑈 𝑐𝑖 |𝜑𝑖 ⟩ = 𝑒𝑖𝜃 𝑈 ′ 𝑐𝑖 |𝜑𝑖 ⟩ (1).
For arbitrary |𝜓⟩ ∈ ℋ, there exists 𝑐0 , . . . , 𝑐𝑖 , . . . , 𝑐2𝑛 −1 such that |𝜓⟩ = 𝑐0 |𝜑0 ⟩ + · · · +𝑐𝑖 |𝜑𝑖 ⟩ + · · · + 𝑐2𝑛−1 |𝜑2𝑛 −1 ⟩ and |𝑐0 |2 + · · · + |𝑐𝑖 |2 + · · · + |𝑐2𝑛 −1 |2 = 1. Because of (1), we
have the following:
𝑈 |𝜓⟩ = 𝑈 𝑐0 |𝜑0 ⟩ + · · · + 𝑈 𝑐𝑖 |𝜑𝑖 ⟩ + · · · + 𝑈 𝑐2𝑛 −1 |𝜑2𝑛 −1 ⟩= 𝑒𝑖𝜃 𝑈 ′ 𝑐0 |𝜑0 ⟩ + · · · + 𝑒𝑖𝜃 𝑈 ′ 𝑐𝑖 |𝜑𝑖 ⟩ + · · · + 𝑒𝑖𝜃 𝑈 ′ 𝑐2𝑛 −1 |𝜑2𝑛 −1 ⟩= 𝑒𝑖𝜃 𝑈 ′ (𝑐0 |𝜑0 ⟩ + · · · + 𝑐𝑖 |𝜑𝑖 ⟩ + · · · + 𝑐2𝑛 −1 |𝜑2𝑛 −1 ⟩)= 𝑒𝑖𝜃 𝑈 ′ |𝜓⟩for any |𝜓⟩ and 𝜃. It means that 𝑈 |𝜓⟩ ≈𝜃 𝑈 ′ |𝜓⟩ for any vector |𝜓⟩. Therefore, 𝑈 = 𝑒𝑖𝜃 𝑈 ′ byLemma 3.2.
Remark 3.1. Checking 𝑈 |𝜓𝑖 ⟩ ≈𝜃 𝑈 ′ |𝜓𝑖 ⟩ is actually checking the observable equivalence of
the 𝑖-th column vector of 𝑈 and the 𝑖-th column vector of 𝑈 ′ with respect to the phase 𝜃.
Lemma 3.4. 𝑈 |𝜑𝑖 ⟩ ≈𝜃 𝑈 ′ |𝜑𝑖 ⟩ for each basis vector |𝜑𝑖 ⟩ in an orthonormal basis of ℋ if andonly if 𝑈 |𝜑𝑖 ⟩ ≈ 𝑈 ′ |𝜑𝑖 ⟩ for each |𝜑𝑖 ⟩ and 𝑈 |𝜑𝑖 ⟩ (𝑈 |𝜑𝑗 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)† for each |𝜑𝑖 ⟩and |𝜑𝑗 ⟩.
Proof. For the ‘only if ’ part (the ⇒ direction), we have 𝑈 |𝜑𝑖 ⟩ ≈ 𝑈 ′ |𝜑𝑖 ⟩ for each basis vector|𝜑𝑖 ⟩ using the assumption. Moreover, we have 𝑈 |𝜑𝑖 ⟩ = 𝑒𝑖𝜃 𝑈 ′ |𝜑𝑖 ⟩ and 𝑈 |𝜑𝑗 ⟩ = 𝑒𝑖𝜃 𝑈 ′ |𝜑𝑗 ⟩ foreach |𝜑𝑖 ⟩ and |𝜑𝑗 ⟩. Therefore, 𝑈 |𝜑𝑖 ⟩ (𝑈 |𝜑𝑗 ⟩)† = 𝑒𝑖𝜃 𝑈 ′ |𝜑𝑖 ⟩ (𝑒𝑖𝜃 𝑈 ′ |𝜑𝑗 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)†For the ‘if ’ part (the ⇐ direction), we have 𝑈 |𝜑𝑖 ⟩ = 𝑒𝑖𝜃𝑖 𝑈 ′ |𝜑𝑖 ⟩ and 𝑈 |𝜑𝑗 ⟩ = 𝑒𝑖𝜃𝑗 𝑈 ′ |𝜑𝑗 ⟩ foreach |𝜑𝑖 ⟩ and |𝜑𝑗 ⟩ using the first condition in the assumption. For the second condition in theassumption, we have as follows:
𝑈 |𝜑𝑖 ⟩ (𝑈 |𝜑𝑗 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)†⇔ 𝑒𝑖𝜃𝑖 𝑈 ′ |𝜑𝑖 ⟩ (𝑒𝑖𝜃𝑗 𝑈 ′ |𝜑𝑗 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)†⇔ 𝑒𝑖(𝜃𝑖 −𝜃𝑗 ) 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)†Therefore, we have 𝜃𝑖 = 𝜃𝑗 for each |𝜑𝑖 ⟩ and |𝜑𝑗 ⟩. It indicates that 𝑈 |𝜑𝑖 ⟩ ≈𝜃 𝑈 ′ |𝜑𝑖 ⟩ for eachbasis vector |𝜑𝑖 ⟩.

88

Algorithm 1: Equivalence Checking of Quantum Circuits
input : 𝑛 – the dimension of a Hilbert space′ . . . 𝑈 ′ – two quantum circuits
𝑈 = 𝑈𝑚 . . . 𝑈0 and 𝑈 ′ = 𝑈𝑚′0{|𝜑0 ⟩ , . . . , |𝜑2𝑛 −1 ⟩} – an orthonormal basis of a Hilbert space ℋ𝜃 ∈ [0, 2𝜋) – the phase
output : True (𝑈 = 𝑒𝑖𝜃 𝑈 ′ ) or False (𝑈 ̸= 𝑒𝑖𝜃 𝑈 ′ )1 forall |𝜑𝑖 ⟩ ∈ {|𝜑0 ⟩ , . . . , |𝜑2𝑛 −1 ⟩} do|𝑢𝑖 ⟩ = 𝑈𝑚 · (. . . (𝑈0 · |𝜑𝑖 ⟩) . . . )′ · (. . . (𝑈 ′ · |𝜑 ⟩) . . . )3|𝑢′𝑖 ⟩ = 𝑈𝑚′𝑖
04
if |𝑢𝑖 ⟩⟨𝑢𝑖 | ̸= |𝑢′𝑖 ⟩⟨𝑢′𝑖 | then5
return False
6
if 𝑖 ̸= 0 ∧ |𝑢0 ⟩⟨𝑢𝑖 | ̸= |𝑢′0 ⟩⟨𝑢′𝑖 | then7
return False
8 return True
2

Based on Lemma 3.1, Lemma 3.3 and Lemma 3.4, we introduce the following theorem tocheck whether 𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋).
Theorem 3.5. Let 𝑈 and 𝑈 ′ be 2𝑛 × 2𝑛 matrices, then 𝑈 = 𝑒𝑖𝜃 𝑈 ′ for some 𝜃 ∈ [0, 2𝜋) if
and only if 𝑈 |𝜑𝑖 ⟩ (𝑈 |𝜑𝑖 ⟩)† = 𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑖 ⟩)† for each basis vector 𝜑𝑖 and 𝑈 |𝜑𝑖 ⟩ (𝑈 |𝜑𝑗 ⟩)† =𝑈 ′ |𝜑𝑖 ⟩ (𝑈 ′ |𝜑𝑗 ⟩)† for each |𝜑𝑖 ⟩ and |𝜑𝑗 ⟩ in an orthonormal basis of ℋ.
Proof. It is immediate from Lemma 3.1, Lemma 3.3 and Lemma 3.4.
′ . . . 𝑈′
It is extremely expensive to calculate matrix-matrix multiplications 𝑈𝑚 . . . 𝑈0 and 𝑈𝑚′0
to obtain 𝑈 and 𝑈 ′ and subsequently multiple with each |𝜑𝑖 ⟩ and |𝜑𝑗 ⟩ in Theorem 3.5 becauseof the exponential size of unitary matrices. Instead, we can perform a series of matrix-vector
multiplications between unitary matrices and vectors in sequence as follows:⃒ 0 ⟩︀⃒ ⟩︀⃒ ⟩︀
⃒𝑢 = 𝑈0 |𝜑𝑖 ⟩ , ⃒𝑢1 = 𝑈1 ⃒𝑢0 , . . . , |𝑢𝑚 ⟩ = 𝑈𝑚 · 𝑢𝑚−1
𝑖
𝑖
𝑖
𝑖
𝑖

The 𝑖-th column vector of matrix 𝑈 is |𝑢𝑖 ⟩ (i.e., |𝑢𝑚𝑖 ⟩) and similarly for the 𝑖-th column vector|𝑢′𝑖 ⟩ of matrix 𝑈 ′ . We are now ready to check whether |𝑢𝑖 ⟩⟨𝑢𝑖 | is equal to |𝑢′𝑖 ⟩⟨𝑢′𝑖 | for the first
condition in Theorem 3.5. Moreover, for the secondin Theorem 3.5, it suffices to fix⃒ ⟩⟨ condition
⃒
⃒ ′
⃒
′
′
|𝑢𝑖 ⟩ and |𝑢𝑖 ⟩, and check whether |𝑢𝑖 ⟩⟨𝑢𝑗 | = ⃒𝑢𝑖 𝑢𝑗 ⃒ for all 𝑗 ̸= 𝑖. This is an efficient way tohandle the calculation in Theorem 3.5.

3.2. Algorithm for Equivalence Checking of Quantum Circuits
An algorithm for equivalence checking of quantum circuits can be constructed based on
Theorem 3.5, which is shown as Algorithm 1. Given two quantum circuits in the form of′ . . . 𝑈 ′ , and an orthonormal basis {|𝜑 ⟩ , . . . , |𝜑 𝑛 ⟩}, for each𝑈 = 𝑈𝑚 . . . 𝑈0 and 𝑈 ′ = 𝑈𝑚
′
0
2 −1
0
basis vector 𝜑𝑖 , we first construct the series of matrix-vector multiplications between unitarymatrices and vectors to obtain |𝑢𝑖 ⟩ and |𝑢′𝑖 ⟩ in the code fragment at lines 2–3. We then check89whether their corresponding density matrices |𝑢𝑖 ⟩⟨𝑢𝑖 | and |𝑢′𝑖 ⟩⟨𝑢′𝑖 | are equal for the first condition in Theorem 3.5 in the code fragment at lines 4–5. If this is not the case, False is returned.
Otherwise, we keep on checking for the second condition in Theorem 3.5 except for the case of
the basis vector |𝜑0 ⟩ in the code fragment at lines 6–7. If |𝑢0 ⟩⟨𝑢𝑖 | is not equal to |𝑢′0 ⟩⟨𝑢′𝑖 |, False
is returned. Otherwise, we move to check for other basis vectors. True is returned at the end
once all basis vectors have been checked.

4. Related Work
L. Burgholzer et al. [13] have proposed an advanced method for equivalence checking ofquantum circuits based on a decision diagram. Their approach involves two quantum circuits′ . . . 𝑈 ′ as inputs and they check whether the two quantum circuits are
𝑈 = 𝑈𝑚 . . . 𝑈0 and 𝑈𝑚′
0equivalent. They leverage two key observations: (1) quantum circuits are inherently reversible,and (2) even small differences in quantum circuits may impact the overall behavior of quantum
circuits. Their strategy is as follows. For (2), they first randomly prepare some basis vectors 𝜑𝑖and calculate the 𝑖-th column of each matrix 𝑈 and 𝑈 ′ to obtain |𝑢𝑖 ⟩ and |𝑢′𝑖 ⟩ as we do. They thencompare |𝑢𝑖 ⟩ and |𝑢′𝑖 ⟩ modulo the global phase by using the fidelity, denoted ℱ = | ⟨𝑢𝑖 |𝑢′𝑖 ⟩ |2 ,to measure the overlap between the two states. The two states are considered equivalent if
the fidelity between them is 1 up to a given tolerance 𝜀. This is an approximate estimation,
while we use their density matrices for the comparison, which provides an exact estimation.
After several runs, if they find |𝑢𝑖 ⟩ and |𝑢′𝑖 ⟩ that are not equivalent, the process is stopped.
Otherwise, they attempt to resolve 𝑈 ⇒ 𝐼 ⇐ 𝑈 ′ into the identity matrix 𝐼 based on (1) tosolve the equivalence checking problem. However, calculating 𝑈𝑖 (𝑈𝑖′′ )† involves an expensive
matrix-matrix multiplication. Moreover, they seem not to consider the global phase in thisstep. We have proven a theorem that it suffices to consider all basis vectors in an orthonormal
basis with the same global phase to conclude the equivalence checking problem. Our approachconsiders the global phase and can be adopted by other approaches/tools for checking theequivalence of quantum circuits.

5. Conclusion
We have presented a theoretical foundation for checking the equivalence of quantum circuits
based on which an algorithm is constructed. The equivalence checking process is simplified
to comparing each column vector of two unitary matrices, representing two quantum circuits,
modulo the same global phase. To eliminate the global phase during the comparison, we compare
their corresponding density matrices instead of their column vectors. To guarantee the same
global phase is used, we compare the outer products of two columns from each unitary matrix,
with one column fixed. We have proven a theorem to guarantee the correctness of our approach.
As one piece of future work, we would develop a support tool based on symbolic reasoningin [14, 15] for our approach and conduct case studies to demonstrate the effectiveness of ourapproach for equivalence checking of quantum circuits.

90

Acknowledgments
The research was supported by JAIST Research Grant for Fundamental Research, by JST SICORP
Grant Number JPMJSC20C2, and by JSPS KAKENHI Grant Number JP23K19959.

References[1] P. Shor, Algorithms for quantum computation: discrete logarithms and factoring, in:Proceedings 35th Annual Symposium on Foundations of Computer Science, 1994, pp.
124–134. doi:10.1109/SFCS.1994.365700.
[2] B. Giles, P. Selinger, Exact synthesis of multiqubit clifford+𝑡 circuits, Phys. Rev. A 87 (2013)
032332. doi:10.1103/PhysRevA.87.032332.
[3] M. Amy, D. Maslov, M. Mosca, M. Roetteler, A meet-in-the-middle algorithm for fast
synthesis of depth-optimal quantum circuits, Trans. Comp.-Aided Des. Integ. Cir. Sys. 32(2013) 818–830. doi:10.1109/TCAD.2013.2244643.
[4] D. Maslov, Advantages of using relative-phase toffoli gates with an application to multiple
control toffoli optimization, Physical Review A 93 (2016). doi:10.1103/physreva.93.
022311.
[5] M. Y. Siraichi, V. F. d. Santos, C. Collange, F. M. Q. Pereira, Qubit allocation, in: Proceedingsof the 2018 International Symposium on Code Generation and Optimization, CGO 2018,
Association for Computing Machinery, New York, NY, USA, 2018, p. 113–125. doi:10.
1145/3168822.
[6] A. Zulehner, A. Paler, R. Wille, Efficient mapping of quantum circuits to the ibm qx
architectures, in: 2018 Design, Automation & Test in Europe Conference & Exhibition(DATE), 2018, pp. 1135–1138. doi:10.23919/DATE.2018.8342181.
[7] A. Cowtan, S. Dilkes, R. Duncan, A. Krajenbrink, W. Simmons, S. Sivarajah, On the qubit
routing problem (2019). doi:10.4230/LIPICS.TQC.2019.5.
[8] D. Maslov, G. W. Dueck, D. M. Miller, C. Negrevergne, Quantum circuit simplificationand level compaction, Trans. Comp.-Aided Des. Integ. Cir. Sys. 27 (2008) 436–444. doi:10.
1109/TCAD.2007.911334.
[9] Z. Sasanian, D. M. Miller, Reversible and quantum circuit optimization: A functional
approach, in: R. Glück, T. Yokoyama (Eds.), Reversible Computation, Springer Berlin
Heidelberg, 2013, pp. 112–124. doi:10.1007/978-3-642-36315-3_9.
[10] Y. Nam, N. J. Ross, Y. Su, A. M. Childs, D. Maslov, Automated optimization of large
quantum circuits with continuous parameters, npj Quantum Information 4 (2018) 23.
doi:10.1038/s41534-018-0072-4.
[11] M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information: 10th Anniversary Edition, Cambridge University Press, 2010. doi:10.1017/CBO9780511976667.
[12] P. A. M. Dirac, A new notation for quantum mechanics, Mathematical Proceedings of theCambridge Philosophical Society 35 (1939) 416–418. doi:10.1017/S0305004100021162.
[13] L. Burgholzer, R. Wille, Advanced equivalence checking for quantum circuits, IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems 40 (2021)
1810–1824. doi:10.1109/TCAD.2020.3032630.

91

[14] C. M. Do, K. Ogata, Symbolic model checking quantum circuits in maude, in: The 35th
International Conference on Software Engineering and Knowledge Engineering, SEKE
2023, 2023, pp. 103–108. doi:10.18293/SEKE2023-014.
[15] T. Takagi, C. M. Do, K. Ogata, Automated quantum program verification in dynamic
quantum logic (to appear), in: DaLí: Dynamic Logic – New trends and applications, 2023.

92