=Paper= {{Paper |id=Vol-3176/paper3 |storemode=property |title= Formal design and verification of cryptographic circuits: Application to symmetric block ciphers |pdfUrl=https://ceur-ws.org/Vol-3176/paper3.pdf |volume=Vol-3176 |authors=Abir Bitat,Salah Merniz |dblpUrl=https://dblp.org/rec/conf/rif/BitatM22 }} == Formal design and verification of cryptographic circuits: Application to symmetric block ciphers == https://ceur-ws.org/Vol-3176/paper3.pdf 
Formal design and verification of cryptographic
circuits: Application to symmetric block ciphers
Abir. BITAT1 , Salah MERNIZ1
1
    MISC Laboratory, IFA departement, NTIC Faculty, Abdelhamid MEHRI-Constantine2 University


                                         Abstract
                                         Cryptographic circuits have become indispensable in most systems where security is the main criteria.
                                         That is why it is important to verify the correctness of their design. In this paper we propose a formal
                                         methodology for design and verification of the cryptographic circuits; it combines two techniques, the
                                         SAT Solver technique, which is automatic and has been used to verify the correctness of combinational
                                         logic parts; and, the induction technique, which has been used for sequential logic parts.
                                             The proposed approach consists of using the functional Hardware Description Language (HDL) Lava
                                         to describe both behavioural and structural aspects of a circuit; using Finite State Machines (FSMs). And
                                         then to verify the specification and check the equivalence of the implementation against it, in order to
                                         prove the circuit’s correctness.
                                             To show the features of the proposed approach, it was applied to verify implementations of both se-
                                         quential and pipelined architectures of the symmetric block cipher AES (Advanced Encryption Standard).

                                         Keywords
                                         Formal design, Formal verification, Cryptographic circuits, Functional approach, FSMD, Finite State
                                         Machine with Data-path, Symmetric cryptography, AES, Functional language, Functional HDL




1. Introduction
Nowadays networks are trusted with extremely sensitive information; hence the importance of
cryptography which makes its security possible. As a consequence, cryptographic co-processors
have become indispensable in many modern applications. A co-processor is a hardware module
that adds functions to a standard CPU; a cryptographic one adds cryptographic IP cores special-
ized for encryption and decryption operations. Due to the sensitivity of the security matter; it
is important to design and implement these circuits correctly.
   Circuits design process goes through several steps; the first one consists in converting the
informal description of the design to an algorithmic specification. From this latter, a micro-
architectural implementation is derived through refinement; followed by a series of design steps
reducing the abstraction levels until a realizable description is obtained. After each of these
design steps; a verification process is performed.
   Design verification of hardware can either concern non functional aspects like time, power
and layout, or functional verification; this latter, consists in checking that the structural imple-
mentation provides the same behavior mentioned in the behavioral specification; which can

RIF 2022: The 11th Seminary of Computer Science research at Feminin, March 10, 2022, Constantine, Algeria
$ abir.bitat@univ-constantine2.dz (Abir. BITAT); salah.merniz@univ-constantine2.dz (S. MERNIZ)
 0000-0003-1748-4286 (Abir. BITAT); 0000-0001-6544-7063 (S. MERNIZ)
                                       Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)
be done in quite a few ways, such as simulation, formal proof, and semi-formal verification in
which the former techniques are combined.
  In this work, we use formal methods in order to design and verify the cryptographic cir-
cuits through functional verification. In section 2 we discuss related literature. In section 3,
we explain our design and verification methodology. In section 4, we demonstrate how we
applied our approach in order to verify sequential and pipelined architectures of the symmetric
cryptographic circuit AES. And finally conclusions are drawn in section 5.


2. Related works
Imperative HDLs like VHDL and verilog, are still the most used for describing digital circuits.
Therefore, the majority of the existing similar works are based on using them [1], [2], [3],
[4], [5]. These languages are intended for description, simulation and synthesis of hardware;
but not for formal verification due to their lack of formal semantics; in addition, they do not
allow descriptions of the highest levels of design. As a consequence, most of the mentioned
works use the simulation technique [2], [3], [4], which is not sufficient for critical systems
such as the cryptographic circuits because it does not guarantee the absence of errors. It is
possible to use formal verification on circuits described with imperatives HDLs, but with a great
deal of difficulties; the behavioral specification that hides all implementation details therefore
needs more powerful abstraction and structuring mechanisms [5]. For the verification of such
complex circuits, deductive methods were used [1]; which is quite difficult, because it requires
user guidance through all the verification process. Symbolic computation was used for the
verification of cryptographic circuits in some algebraic approaches [6], [7]; similarly to the work
presented herein, they use the hierarchy technique in order to reduce the complexity of design
and therefore simplify the verification task. Equivalence checking and completion functions
were used in a formal approach [8] for the verification of RTL descriptions in imperative
HDL VHDL. A language and tool that support automated formal verification of cryptographic
assembly code was proposed in [9]. As for the pipelined implementations of cryptographic
circuits; the imperative HDL VHDL was used for the description and simulation of some crypto-
processors in [10]; and formal verification was applied, but no details about the method that
was used were mentioned.
   Even though there exists several functional approaches that were applied for the verification
of digital circuits; to the best of our knowledge; beside the work presented herein, there is only
one approach for the implementation and verification of cryptographic circuits [11]. However;
this approach uses the functional language only for the behavioral specification; but it uses
an imperative HDL for the structural implementation; which brings back some translation
difficulties between the two descriptions.


3. The proposed approach
The design process of a circuit is divided into several steps, where the implementation resulting
on a certain abstraction level is used as the specification on the next lower one. A verification
phase is mandatory after each step, to avoid the propagation of errors between the abstraction
levels. Therefore, in order to verify the correctness of a certain implementation, it is sufficient
to compare it to its already verified specification. The most challenging verification step is that
of the highest levels of abstraction; this difficulty is caused by the gap between descriptions as
the majority of HDLs don’t allow ones at those levels.
   In this work, we propose a methodology of formal design and verification for the cryp-
tographic circuits, we target the higher levels of abstraction, and we verify that the micro-
architectural description of a cryptographic circuit is equivalent to the algorithmic one.
   The other attribute of our proposed approach is that we use the functional language Haskell
and its embedded HDL Lava to describe the circuits. This choice is motivated by their interesting
characteristics such as: having formal descriptions that can be reasoned about; the composition
of functions in the same way that complex circuits are composed; having much more concise
descriptions, which makes finding errors easier; and last but not least, Lava has some incorpo-
rated tools for formal verification of circuits; which in our knowledge have never been used for
the verification of the cryptographic circuits.
   A FSMD (Finite State Machine with Datapath) model provides a systematic approach for
designing sequential circuits; it combines a controller, modeled as a FSM, and a dapapath. We
model both descriptions of the circuit (behavioral and structural) as FSMs.
   A FSM in Haskell is a recursive function fsm, which represents the output function; it takes
as input a π‘ π‘–βˆ’1 with the next state function called step, like shown in the following form:

                                  𝑓 π‘ π‘š 𝑛 𝑠𝑖 = 𝑓 π‘ π‘š (𝑛 βˆ’ 1) 𝑠𝑗
                                     π‘€β„Žπ‘’π‘Ÿπ‘’
                                            𝑠𝑗 = 𝑠𝑑𝑒𝑝 𝑠𝑖

Since the two descriptions are at different levels of abstraction, they deal with different types
of data; therefore, a mapping function abs is needed between the two them. Thus, in order to
verify the implementation; the following theorem must be proved:

                       βˆ€ 𝑠𝑖 ∈ π‘ π‘‘π‘Žπ‘‘π‘’π‘ , 𝑓 π‘ π‘šπ‘† (π‘Žπ‘π‘  𝑠𝑖 ) = π‘Žπ‘π‘  (𝑓 π‘ π‘šπΌ 𝑠𝑖 )                        (1)

   The proof of this theorem must be decomposed. Since both descriptions are hierarchical, we
need to start by verifying the simplest components at the lowest level of hierarchy. Once they
are verified, the verification of the upper components that they compose becomes possible.
   The combinational parts of the implementation can be verified automatically using the SAT
solver tool of Lava. As for the sequential parts; we use induction and equational reasoning.
   When performing equivalence checking using SAT solvers, if the two descriptions are equiv-
alents, the output of the Xor gate should be always False. If the output becomes True for any
input sequence, it means that the SAT solver found a satisfiable assignment, which implies that
the descriptions are producing different outputs for the same input.
   In order to verify that two descriptions are equivalent, we have to define a safety property
that expresses their equivalence. A safety property states that some condition is always true.
This property is also defined as a function in the following form:

    π‘π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦πΈπ‘žπ‘’π‘–π‘£ 𝑖𝑛 = π‘œπ‘˜
         π‘€β„Žπ‘’π‘Ÿπ‘’
              π‘œπ‘’π‘‘1 = π‘‘π‘’π‘ π‘π‘Ÿπ‘–π‘π‘‘π‘–π‘œπ‘›1 𝑖𝑛
              π‘œπ‘’π‘‘2 = π‘‘π‘’π‘ π‘π‘Ÿπ‘–π‘π‘‘π‘–π‘œπ‘›2 𝑖𝑛
              π‘œπ‘˜ = π‘œπ‘’π‘‘1 <==> π‘œπ‘’π‘‘2π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž

  To verify this property we use the Lava function satzoo, which is a call to the satisfiability
solver: π‘ π‘Žπ‘‘π‘§π‘œπ‘œ π‘π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦πΈπ‘žπ‘’π‘–π‘£.
  Since we want to verify that a component implements correctly its specification (which works
with a different data type); the equivalence property should be defined in the following way
instead:

    π‘π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦πΈπ‘žπ‘’π‘–π‘£ 𝑖𝑛 = π‘œπ‘˜
         π‘€β„Žπ‘’π‘Ÿπ‘’
              π‘œπ‘’π‘‘1 = 𝑠𝑝𝑒𝑐𝑖𝑓 π‘–π‘π‘Žπ‘‘π‘–π‘œπ‘› (π‘Žπ‘π‘  𝑖𝑛)
              π‘œπ‘’π‘‘2 = π‘Žπ‘π‘  (π‘–π‘šπ‘π‘™π‘’π‘šπ‘’π‘›π‘‘π‘Žπ‘‘π‘–π‘œπ‘› 𝑖𝑛)
              π‘œπ‘˜ = π‘œπ‘’π‘‘1 <==> π‘œπ‘’π‘‘2π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž

  Now, for the verification of the sequential part, which is the FSM it self, meaning the imple-
mentation of the whole circuit; we use induction like we mentioned previously. So, we start
by verifying the base case (a); then we prove (b) that if the property holds for a step n; then it
should hold for the following step n-1.

                 (π‘Ž) 𝑓 π‘ π‘šπ‘† 0 (π‘Žπ‘π‘  𝑠𝑖 ) = π‘Žπ‘π‘  (𝑓 π‘ π‘šπΌ 0 𝑠𝑖 )
                 (𝑏) 𝑓 π‘ π‘šπ‘† 𝑛 (π‘Žπ‘π‘  𝑠𝑖 ) = π‘Žπ‘π‘  (𝑓 π‘ π‘šπΌ 𝑛 𝑠𝑖 ) β‡’
                            𝑓 π‘ π‘šπ‘† (𝑛 βˆ’ 1) (π‘Žπ‘π‘  𝑠𝑖 ) = π‘Žπ‘π‘  (𝑓 π‘ π‘šπΌ (𝑛 βˆ’ 1) 𝑠𝑖 )

   The proposed approach for verifying both sequential and pipelined architectures is summa-
rized in Fig.1. We start by checking if the behavioural description of the sequential architecture
holds the verification property (1) ; then, we verify the sequential implementation against its
specification (2). As for the pipelined architecture, we verify the equivalence of its specifica-
tion to the sequential one (3); and finally we verify its implementation against the verified
specification (4).
   We prove the verification property (1) and equivalence property (3) using Lava’s SAT solver.
We also use this latter to verify the inner sub-components of the circuits, like shown in Fig.2.
Then we will be able to prove the equivalence properties (i.e. (2), and (4)) using induction.


4. Application and results
Advanced Encryption Standard (AES) [14] is a symmetric block cipher, constructed based on
the Rijandael system; it encrypts blocks of 128 bits using a key of 128 bits size, 129, or 256 bits
depending on the system’s version. We demonstrate our proposed approach on AES128.
   The encryption consists of ten identical rounds of processing; each of which includes four
steps: sub bytes, shift rows, mix columns and add key; except for the last one, where the mix
Figure 1: Global view of the proposed approach.




Figure 2: Automatic verification of the combinational parts.


columns function is not performed. The decryption on the other hand, uses the inverse of these
functions in a different order.
  The key expansion function uses the cipher key to produce sub-keys in the same number of
rounds. In this work, we pre-calculate the sub-keys in advance.

4.1. Formal design of the Sequential architecture
The basic hardware architecture used to implement an encryption or decryption unit of the
symmetric AES cipher is shown in Fig.3. This architecture characteristics is that only one block
of data is encrypted at a time.
Figure 3: Basic iterative architecture.


4.1.1. Behavioural description
The AES core is composed of three units: encryption unit, decryption unit, and key expansion
unit in order to pre-calculate the sub-keys. It is defined by the function seqSpecAES, which takes
as inputs a text text, a key key and the operation type op.

    π‘ π‘’π‘žπ‘†π‘π‘’π‘π΄πΈπ‘†(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦) = 𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀
          π‘€β„Žπ‘’π‘Ÿπ‘’
              π‘˜π‘’π‘¦π‘  = π‘˜π‘’π‘¦πΈπ‘₯π‘π‘Žπ‘›π‘ π‘–π‘œπ‘›π‘† 10 π‘˜π‘’π‘¦
              𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀 = 𝑖𝑓 (π‘œπ‘ == 1) π‘‘β„Žπ‘’π‘› (π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))
              𝑒𝑙𝑠𝑒 (π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž

The function seqSpecEnc converts the text from ascii to hexadecimal, and decomposes it into
blocks of 128bits, and send them sequentially to the function that encrypts one block of data.
The behavioral description of this encryption unit is expressed as a FSM in Lava, represented by
the recursive function seqSpecEncFSM, which takes as input the stat 𝑠𝑖 which is composed of: the
round number n, one block of the plain text pt, the current cipher text ct, and the pre-calculated
sets of sub-keys keys; and it calculates the round cipher text using the next state function
stepSeqSpecEnc.

    π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ) = π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑𝑁 𝑒𝑀, π‘˜π‘’π‘¦π‘ )
           π‘€β„Žπ‘’π‘Ÿπ‘’
                   𝑠𝑒𝑙 = (𝑛 == 10)
                   𝑠𝑒 = (𝑛 == 1)
                   𝑖𝑑 = π‘šπ‘’π‘₯𝑆 (𝑠𝑒𝑙, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘† ( (π‘˜π‘’π‘¦π‘ !!0) , 𝑝𝑑), 𝑐𝑑)
                   𝑐𝑑𝑁 𝑒𝑀 = π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(𝑠𝑒, 𝑖𝑑, π‘˜π‘’π‘¦π‘ !!(10 βˆ’ (𝑛 βˆ’ 1)))
   π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(𝑠𝑒, 𝑖𝑑, π‘–π‘˜) = (𝑐𝑑𝑁 𝑒𝑀)
          π‘€β„Žπ‘’π‘Ÿπ‘’
                 𝑐𝑑𝑁 𝑒𝑀 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘–π‘˜, π‘šπ‘’π‘₯𝑆(𝑠𝑒, π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆 𝑖𝑑),
                               π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ π‘†(π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆 𝑖𝑑))))


  The selector sel controls whether to take the initial plain text pt or the current round cipher
text ct; and the selector se controls whether to perform the mix Columns function or not.
  The seqSpecDecFSM function is a FSM as well that represents the behavioral description of
the decryption unit.


  π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ) = π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), 𝑝𝑑𝑁 𝑒𝑀, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )
        π‘€β„Žπ‘’π‘Ÿπ‘’
                𝑠𝑒𝑙 = (𝑛 == 10)
                𝑠𝑒 = (𝑛 == 1)
                𝑖𝑑 = π‘šπ‘’π‘₯𝑆 (𝑠𝑒𝑙, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘† ( (π‘˜π‘’π‘¦π‘ !!10) , 𝑐𝑑), 𝑝𝑑)
                𝑐𝑑𝑁 𝑒𝑀 = π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘(𝑠𝑒, 𝑖𝑑, π‘˜π‘’π‘¦π‘ !!(𝑛 βˆ’ 1))


 π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘(𝑠𝑒, 𝑖𝑑, π‘–π‘˜) = (𝑝𝑑𝑁 𝑒𝑀)
        π‘€β„Žπ‘’π‘Ÿπ‘’
                𝑝𝑑𝑁 𝑒𝑀 = π‘šπ‘’π‘₯𝑆(𝑠𝑒, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘–π‘˜, (𝑖𝑛𝑣𝑆𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘–π‘›π‘£π‘†β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘† 𝑖𝑑)))
                , 𝑖𝑛𝑣𝑀 𝑖π‘₯πΆπ‘™π‘šπ‘ π‘†(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘–π‘˜, (𝑖𝑛𝑣𝑆𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘–π‘›π‘£π‘†β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘† 𝑖𝑑)))))

4.1.2. Structural description
The hardware implementation of AES is described in the same hierarchical way as the behavioral
description; it is composed of three components : the key expansion function keyExpansionI,
the encryption function seqImpEnc, and the decryption function seqImpDec.


 π‘ π‘’π‘žπΌπ‘šπ‘π΄πΈπ‘†(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦) = 𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀
        π‘€β„Žπ‘’π‘Ÿπ‘’
               π‘˜π‘’π‘¦π‘  = π‘˜π‘’π‘¦πΈπ‘₯π‘π‘Žπ‘›π‘ π‘–π‘œπ‘›πΌ 10 π‘˜π‘’π‘¦
               𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀 = 𝑖𝑓 (π‘œπ‘ == 1) π‘‘β„Žπ‘’π‘› (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))𝑒𝑙𝑠𝑒 (π‘ π‘’π‘žπΌπ‘šπ‘π·π‘’π‘
               (𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))


  The encryption function seqImpEnc converts the text from ascii to hexadecimal to binary
and decompose it into blocks of 128bits and send it sequentially block by block to the function
seqImpEncFSM, which is the FSM that models the structural description of the encryption unit.
    π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ) = π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑𝑁 𝑒𝑀, π‘˜π‘’π‘¦π‘ )
           π‘€β„Žπ‘’π‘Ÿπ‘’
                 𝑠𝑒𝑙 = (𝑛 == 10)
                 𝑠𝑒 = (𝑛 == 1)
                 𝑖𝑑 = π‘šπ‘’π‘₯𝐼 (𝑠𝑒𝑙, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ ( (π‘˜π‘’π‘¦π‘ !!0), 𝑝𝑑), 𝑐𝑑)
                 𝑐𝑑𝑁 𝑒𝑀 = π‘ π‘‘π‘’π‘π‘†π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘(𝑠𝑒, 𝑖𝑑, π‘˜π‘’π‘¦π‘ !!(𝑛 βˆ’ 1))


    π‘ π‘‘π‘’π‘π‘†π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘(𝑠𝑒, 𝑖𝑑, π‘–π‘˜) = (𝑐𝑑𝑁 𝑒𝑀)
              π‘€β„Žπ‘’π‘Ÿπ‘’
                 𝑐𝑑𝑁 𝑒𝑀 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(π‘–π‘˜, π‘šπ‘’π‘₯𝐼(𝑠𝑒, π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 𝑖𝑑),
                             π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ πΌ(π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 𝑖𝑑))))


   The inner components of this circuit (seqImpEncFSM), like muxI, addKeyI... are defined in
terms of their structure using gates, unlike the muxS, addKeyS... which express the behavior of
that component.

   π‘šπ‘’π‘₯𝑆(𝑠𝑒𝑙, π‘Ž, 𝑏) = 𝑖𝑓 𝑠𝑒𝑙 π‘‘β„Žπ‘Žπ‘› π‘Ž 𝑒𝑙𝑠𝑒 𝑏
   π‘šπ‘’π‘₯𝐼(𝑠𝑒𝑙, π‘Ž, 𝑏) = π‘œπ‘ŸπΌ (π‘Žπ‘›π‘‘πΌ 𝑠𝑒𝑙 π‘Ž) (π‘Žπ‘›π‘‘πΌ (π‘›π‘œπ‘‘πΌ 𝑠𝑒𝑙) 𝑏)π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž


  The hardware implementations of the main four components of AES are the followings:
   – Add Key: is implemented using the bitwise XOR gate; and therefore it is the inverse of
     itself.
   – Shift Rows: is a left cyclic shift of bits. The inverse shift rows is a right cyclic shift.
   – Sub Bytes: relies on operations in the Galois Field GF (28 ); it can be implemented using
     only logic i.e. implementing circuits for the multiplication operation, the inverse operation,
     and for the affine transformation operation; or using the S-boxes, or Look-Up-Tables
     (LUTs); which are implemented as Read Only Memories (ROMs). We need 16 8x8 bit
     ROMs for the encryption and 16 for the Inverse Sub Bytes.
   – Mix Columns: relies on operations in GF(28 ) as well, and can be expressed using only
     logic or LUTs too; which are implemented as 8x8 bit ROMs for each of the multiplication
     operations of both encryption and decryption process.
  seqImpDecFSM function represents the structural description of the decryption unit.

4.2. Formal design of the Pipelined architecture
There are several architectures possible for pipelined block ciphers [15] ; we chose the one with
inner-round pipelining depicted in Fig.4. with four pipeline stages. This makes it possible to
encrypt four blocks simultaneously.
Figure 4: Basic iterative with inner-round pipelining.


4.2.1. Behavioral description
Similarly to the sequential architecture; AES is composed of three units: encryption, decryption,
and key expansion. This latter is the same as in the sequential architecture.


    𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐴𝐸𝑆(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦) = 𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀
           π‘€β„Žπ‘’π‘Ÿπ‘’
              π‘˜π‘’π‘¦π‘  = π‘˜π‘’π‘¦πΈπ‘₯π‘π‘Žπ‘›π‘ π‘–π‘œπ‘›π‘† 10 π‘˜π‘’π‘¦
              𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀 = 𝑖𝑓 (π‘œπ‘ == 1) π‘‘β„Žπ‘’π‘› (𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(𝑑𝑒π‘₯𝑑,
              π‘˜π‘’π‘¦π‘ ))𝑒𝑙𝑠𝑒 (𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž


  The function pipeSpecEnc converts the text from ascii to hexadecimal, decomposes it into
blocks of 128bits, and send them to the function pipeSpecEncFSM that encrypts four blocks of
data. Unlike in the sequential architecture, where the number of states equals the number of
rounds; in this architecture, more internal states appear; which represents the pipeline stages
registers. Thus, the next-state function stepPipeSpecEnc is a recursive function that takes as
input the number of internal step n, the pre-calculated keys keys, and the current state of the
four stages registers (c1,c2,c3,c4).
𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐𝐹 𝑆𝑀 (𝑝4π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ ) = 𝑐4π‘π‘™π‘œπ‘π‘˜π‘ 
π‘€β„Žπ‘’π‘Ÿπ‘’
𝑒 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ π‘†(π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(𝑝4π‘π‘™π‘π‘˜π‘ !!0, (π‘˜π‘’π‘¦π‘ !!0)))))
𝑑 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(𝑝4π‘π‘™π‘π‘˜π‘ !!1, (π‘˜π‘’π‘¦π‘ !!0))))
𝑐 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(𝑏3 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(𝑝4π‘π‘™π‘π‘˜π‘ !!2, (π‘˜π‘’π‘¦π‘ !!0)))
𝑏 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(𝑝4π‘π‘™π‘π‘˜π‘ !!3, (π‘˜π‘’π‘¦π‘ !!0))
(𝑛, (𝑐1, 𝑐2, 𝑐3, 𝑐4), π‘˜) = 𝑠𝑑𝑒𝑝(34, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )
𝑐𝑑1 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†((π‘˜π‘’π‘¦π‘ !!10), 𝑐3)
𝑐𝑑2 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†((π‘˜π‘’π‘¦π‘ !!10), (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘† 𝑐2))
𝑐𝑑3 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†((π‘˜π‘’π‘¦π‘ !!10), π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆 𝑐1))
𝑐𝑑4 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†((π‘˜π‘’π‘¦π‘ !!10), (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†((π‘˜π‘’π‘¦π‘ !!9), 𝑐4)))))
𝑐4π‘π‘™π‘œπ‘π‘˜π‘  = [𝑐𝑑1, 𝑐𝑑2, 𝑐𝑑3, 𝑐𝑑4]

𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ) = 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐((𝑛 βˆ’ 1), (𝑏𝑛, 𝑐𝑛, 𝑑𝑛, 𝑒𝑛), π‘˜π‘’π‘¦π‘ )
π‘€β„Žπ‘’π‘Ÿπ‘’
π‘˜ = π‘€β„Žπ‘Žπ‘‘πΎπ‘’π‘¦ 𝑛 π‘˜π‘’π‘¦π‘ 
𝑐𝑛 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆 𝑏
𝑑𝑛 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘† 𝑐
𝑒𝑛 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ π‘† 𝑑
𝑏𝑛 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘† (π‘˜, 𝑒)
  The decryption function pipeSpecDecFSM is also a FSM; it’s next-state function is step-
PipeSpecDec.

4.2.2. Structural description
Like for the sequential architecture, the hardware implementation of pipelined AES is described
in the same hierarchical way as its behavioral description; it is composed of three components
: the key expansion function keyExpansionI, the encryption function pipeImpEnc, and the
decryption function pipeImpDec.


 π‘π‘–π‘π‘’πΌπ‘šπ‘π΄πΈπ‘†(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦) = 𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀
       π‘€β„Žπ‘’π‘Ÿπ‘’
           π‘˜π‘’π‘¦π‘  = π‘˜π‘’π‘¦πΈπ‘₯π‘π‘Žπ‘›π‘ π‘–π‘œπ‘›πΌ 10 π‘˜π‘’π‘¦
           𝑑𝑒π‘₯𝑑𝑁 𝑒𝑀 = 𝑖𝑓 (π‘œπ‘ == 1) π‘‘β„Žπ‘’π‘› (π‘π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ )) 𝑒𝑙𝑠𝑒 (π‘π‘–π‘π‘’πΌπ‘šπ‘π·π‘’π‘
           (𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ))π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž

  The encryption function PipeImpEnc converts the text from ascii to hexadecimal to binary
and decompose it into blocks of 128bits and send them to the function pipeImpEncFSM, which is
the FSM that models the structural description of the encryption unit.


π‘π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑝4π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ ) = 𝑐4π‘π‘™π‘œπ‘π‘˜π‘ 
 π‘€β„Žπ‘’π‘Ÿπ‘’
    𝑒 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ πΌ(π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(𝑝4π‘π‘™π‘π‘˜π‘ !!0, (π‘˜π‘’π‘¦π‘ !!0)))))
    𝑑 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(𝑝4π‘π‘™π‘π‘˜π‘ !!1, (π‘˜π‘’π‘¦π‘ !!0))))
    𝑐 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(𝑝4π‘π‘™π‘π‘˜π‘ !!2, (π‘˜π‘’π‘¦π‘ !!0)))
    𝑏 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(𝑝4π‘π‘™π‘π‘˜π‘ !!3, (π‘˜π‘’π‘¦π‘ !!0))
    (𝑛, (𝑐1, 𝑐2, 𝑐3, 𝑐4), π‘˜) = 𝑠𝑑𝑒𝑝𝐼(34, (𝑏4, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )
    𝑐𝑑1 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ((π‘˜π‘’π‘¦π‘ !!10), 𝑐3)
    𝑐𝑑2 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ((π‘˜π‘’π‘¦π‘ !!10), (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌπ‘2))
    𝑐𝑑3 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ((π‘˜π‘’π‘¦π‘ !!10), (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼𝑐1)))
    𝑐𝑑4 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ((π‘˜π‘’π‘¦π‘ !!10), (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ(𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼(π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ((π‘˜π‘’π‘¦π‘ !!9), 𝑐4)))))
    𝑐4π‘π‘™π‘œπ‘π‘˜π‘  = [𝑐𝑑1, 𝑐𝑑2, 𝑐𝑑3, 𝑐𝑑4]


𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ) = 𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘((𝑛 βˆ’ 1), (𝑏𝑛, 𝑐𝑛, 𝑑𝑛, 𝑒𝑛), π‘˜π‘’π‘¦π‘ )
 π‘€β„Žπ‘’π‘Ÿπ‘’
    π‘˜ = π‘€β„Žπ‘Žπ‘‘πΎπ‘’π‘¦ 𝑛 π‘˜π‘’π‘¦π‘ 
    𝑐𝑛 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼𝑏
    𝑑𝑛 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌπ‘
    𝑒𝑛 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘ πΌπ‘‘
    𝑏𝑛 = π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(π‘˜, 𝑒)


   The pipeImpDecFSM function represents the decryption FSM; it’s next-state function is
stepPipeImpDec.

4.3. Formal verification
In order to verify that both sequential and pipelined architectures implement correctly the
behavior of their specifications; seven theorems have to be proved.

   1. First we need to verify the correctness property of the initial specification, which is
      expressed by the following theorem:

                             βˆ€ π‘š, π·π‘’π‘π‘Ÿπ‘¦π‘π‘‘π‘–π‘œπ‘›(πΈπ‘›π‘π‘Ÿπ‘¦π‘π‘‘π‘–π‘œπ‘› π‘š) = π‘š                            (2)

   2. Then we need to verify the equivalence of the implementation of the encryption unit to
      its specification:


      βˆ€ 𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ; π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
                                                                                           (3)
   3. And the equivalence of the decryption unit implementation against its specification:


      βˆ€ 𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ; π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘π·π‘’π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
                                                                                            (4)
   4. Afterwards, we need to verify the equivalence between the specification of the pipelined
      text encryption unit and the sequential one :

               βˆ€ 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ; π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ) = 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ )             (5)
   5. And the equivalence between the specification of the pipelined text decryption unit and
      the sequential one:

                βˆ€ 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ; π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ) = 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ )                  (6)
   6. Finally, we need to verify the equivalence of the pipelined implementation of the encryp-
      tion unit against its specification:


      βˆ€ 𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ; 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐𝐹 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
                                                                                         (7)
   7. And respectively, we need to verify the equivalence of the pipelined implementation of
      the decryption unit against its specification:


      βˆ€ 𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ; 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐𝐹 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘π‘–π‘π‘’πΌπ‘šπ‘π·π‘’π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
                                                                                    (8)

4.3.1. Formal verification of the sequential architecture
Theorem (2) is written in Lava in the following form:


π‘£π‘’π‘Ÿπ‘–π‘“ π‘–π‘π‘Žπ‘‘π‘–π‘œπ‘›π‘ƒ π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦ (𝑝𝑑, π‘˜π‘’π‘¦π‘ ) = π‘œπ‘˜
        π‘€β„Žπ‘’π‘Ÿπ‘’
              𝑝𝑑0 = 𝑓 π‘Ÿπ‘œπ‘šπΏπ‘–π‘ π‘‘π‘‡ π‘œπ‘†π‘‘π‘Žπ‘‘π‘’ 𝑝𝑑
              π‘˜π‘’π‘¦π‘ 0 = 𝑓 π‘Ÿπ‘œπ‘šπΏπ‘–π‘ π‘‘π‘‡ π‘œπΏπ‘–π‘ π‘‘π‘‚π‘“ π‘†π‘‘π‘Žπ‘‘π‘’π‘  π‘˜π‘’π‘¦π‘ 
              (𝑛1, 𝑝𝑑1, 𝑐𝑑1, π‘˜1) = π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (10, 𝑝𝑑0, [[[ ]]], π‘˜π‘’π‘¦π‘ 0)
              (𝑛2, 𝑝𝑑2, 𝑐𝑑2, π‘˜2) = π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘πΉ 𝑆𝑀 (10, [[[ ]]], 𝑐𝑑1, π‘˜π‘’π‘¦π‘ 0)π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž
              π‘œπ‘˜ = 𝑝𝑑0 <==> 𝑝𝑑2


  Because lists are infinite structures, we need to define a verification property that is explicit
about the sizes:


 π‘£π‘’π‘Ÿπ‘–π‘“ 𝑃 π‘Ÿπ‘œπ‘πΉ π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ 𝑛 π‘š =
      𝑓 π‘œπ‘Ÿπ΄π‘™π‘™ (𝑙𝑖𝑠𝑑 𝑛) $ βˆ– 𝑝𝑑 βˆ’ >
              𝑓 π‘œπ‘Ÿπ΄π‘™π‘™ (𝑙𝑖𝑠𝑑 π‘š) $ βˆ– π‘˜π‘’π‘¦π‘  βˆ’ >
                       π‘£π‘’π‘Ÿπ‘–π‘“ π‘–π‘π‘Žπ‘‘π‘–π‘œπ‘›π‘ƒ π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦(𝑝𝑑, π‘˜π‘’π‘¦π‘ )π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž


  To prove this property we call the satzoo function:
π‘ π‘Žπ‘‘π‘§π‘œπ‘œ π‘π‘Ÿπ‘œπ‘π‘‰ π‘’π‘Ÿπ‘–π‘“ 𝐹 π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ 128 1408 (1408 is the total of eleven 128bit size keys); it returns
Valid, which means that the specification holds that property.
  In order to be able to prove theorem (3) and (4), we need to verify the descriptions internal
components; using the same method as for theorem (2); to the multiplexer component, the main
four operations (sub bytes, shift rows, mix columns, and add key), and their inverses:


π‘π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦πΈπ‘žπ‘’π‘–π‘£π‘†π‘’π‘π΅π‘¦π‘‘π‘’π‘  𝑠 = π‘œπ‘˜π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž
     π‘€β„Žπ‘’π‘Ÿπ‘’
          π‘₯ = 𝑓 π‘Ÿπ‘œπ‘šπΏπ‘–π‘ π‘‘π‘‡ π‘œπ‘†π‘‘π‘Žπ‘‘π‘’ 𝑠
          π‘œπ‘’π‘‘1 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆 (π‘Žπ‘π‘  π‘₯)
          π‘œπ‘’π‘‘2 = π‘Žπ‘π‘  (𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 𝑠)
          π‘œπ‘˜ = π‘œπ‘’π‘‘1 <==> π‘œπ‘’π‘‘2


π‘π‘Ÿπ‘œπ‘πΈπ‘žπ‘’π‘–π‘£π‘†π‘’π‘π΅π‘¦π‘‘π‘’π‘ πΉ π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ 𝑛 =
                       𝑓 π‘œπ‘Ÿπ΄π‘™π‘™ (𝑙𝑖𝑠𝑑 𝑛) $ βˆ– 𝑠 βˆ’ >
                               π‘π‘Ÿπ‘œπ‘π‘’π‘Ÿπ‘‘π‘¦πΈπ‘žπ‘’π‘–π‘£π‘†π‘’π‘π΅π‘¦π‘‘π‘’π‘  π‘ π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž


  π‘ π‘Žπ‘‘π‘§π‘œπ‘œ π‘π‘Ÿπ‘œπ‘πΈπ‘žπ‘’π‘–π‘£π‘†π‘’π‘π΅π‘¦π‘‘π‘’π‘ πΉ π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ 128

  All these properties were satisfied and gave back the answer Valid; which means that the
implementations of these components are correct.

  The sub-circuit stepSeqImpEnc that is composed of the previously verified components is also
correct according to the theorem proved above.


    βˆ€ 𝑖𝑛, 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 𝑖𝑛), π‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Žπ‘Ž
    βˆ€ 𝑖𝑛, π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ 𝑖𝑛),
    βˆ€ 𝑖𝑛, π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ π‘†(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ πΌ 𝑖𝑛),
    βˆ€ 𝑖𝑛, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ 𝑖𝑛),
    βˆ€ 𝑖𝑛, π‘šπ‘’π‘₯𝑆(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (π‘šπ‘’π‘₯𝐼 𝑖𝑛),
     β‡’ βˆ€ 𝑖𝑛, π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(π‘Žπ‘π‘  𝑖𝑛) = π‘Žπ‘π‘ (π‘ π‘‘π‘’π‘π‘†π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘ 𝑖𝑛)

  Now that all the inner-components are verified, we verify the encryption FSM using induction.

Basis:


   π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )
   π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )
   β‡’ π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (0, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
Induction step:
βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑝𝑑, 𝑐𝑑 ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]; π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
β‡’ π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ ((π‘›βˆ’1), 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 ((π‘›βˆ’1), 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
= π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑𝑖 , π‘˜π‘’π‘¦π‘ ))
π‘€π‘–π‘‘β„Ž 𝑐𝑑𝑖 = π‘ π‘‘π‘’π‘π‘†π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘ 𝑐𝑑
π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
= π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (𝑛, π‘Žπ‘π‘  𝑝𝑑, π‘Žπ‘π‘  𝑐𝑑, π‘Žπ‘π‘  π‘˜π‘’π‘¦π‘ )
= π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), π‘Žπ‘π‘  𝑝𝑑, 𝑐𝑑𝑠 , π‘Žπ‘π‘  π‘˜π‘’π‘¦π‘ )
π‘€π‘–π‘‘β„Ž 𝑐𝑑𝑠 = π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘ (π‘Žπ‘π‘  𝑐𝑑)
π‘ π‘‘π‘’π‘π‘†π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(π‘Žπ‘π‘  𝑐𝑑) = π‘Žπ‘π‘ (π‘ π‘‘π‘’π‘π‘†π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘ 𝑐𝑑)
β‡’ 𝑐𝑑𝑠 = π‘Žπ‘π‘  𝑐𝑑𝑖
= π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), π‘Žπ‘π‘  𝑝𝑑, π‘Žπ‘π‘  𝑐𝑑𝑖 , π‘Žπ‘π‘  π‘˜π‘’π‘¦π‘ )
= π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑𝑖 , π‘˜π‘’π‘¦π‘ ))

β‡’ π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))
= π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 ((𝑛 βˆ’ 1), 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))

  We verified the correctness of the decryption unit’s implementation in the same way.

β‡’ βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑝𝑑, 𝑐𝑑 ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]; π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™π΅π‘œπ‘œπ‘™]]]];
π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘πΉ 𝑆𝑀 (π‘Žπ‘π‘ (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘π·π‘’π‘πΉ 𝑆𝑀 (𝑛, 𝑝𝑑, 𝑐𝑑, π‘˜π‘’π‘¦π‘ ))

β‡’ βˆ€ π‘œπ‘ ∈ 𝐼𝑛𝑑, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦ ∈ [πΆβ„Žπ‘Žπ‘Ÿ];
π‘ π‘’π‘žπ‘†π‘π‘’π‘π΄πΈπ‘†(π‘Žπ‘π‘ (π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦)) = π‘Žπ‘π‘ (π‘ π‘’π‘žπΌπ‘šπ‘π΄πΈπ‘†(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦))


4.3.2. Formal verification of the pipelined architecture
For the verification of the pipelined behavioral description against the sequential one, we verify
the equivalence of their upper components that encrypts multiple blocks of data; because the
next state in the sequential FSM consists of the result after one round; however, the next state
in the pipelined FSM is the result of one inner-round pipeline stage.
π‘’π‘žπ‘’π‘–π‘£π‘ƒ π‘Ÿπ‘œπ‘π‘†π‘’π‘žπ‘ƒ 𝑖𝑝(𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ ) = π‘œπ‘˜
π‘€β„Žπ‘’π‘Ÿπ‘’
𝑑π‘₯𝑑 = 𝑓 π‘Ÿπ‘œπ‘šπ‘‡ 𝑒π‘₯𝑑𝑇 π‘œπ΅π‘™π‘œπ‘π‘˜π‘  𝑑𝑒π‘₯𝑑
π‘˜π‘  = 𝑓 π‘Ÿπ‘œπ‘šπΏπ‘–π‘ π‘‘π‘‡ π‘œπ‘†π‘‘π‘Žπ‘‘π‘’ π‘˜π‘’π‘¦π‘ 
π‘œπ‘’π‘‘1 = π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘(𝑑π‘₯𝑑, π‘˜π‘ )
π‘œπ‘’π‘‘2 = 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(𝑑π‘₯𝑑, π‘˜π‘ )
π‘œπ‘˜ = π‘œπ‘’π‘‘1 <==> π‘œπ‘’π‘‘2
π‘’π‘žπ‘’π‘–π‘£π‘ƒ π‘Ÿπ‘œπ‘π‘†π‘’π‘žπ‘ƒ 𝑖𝑝𝐹 π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ 𝑛 π‘š =
𝑓 π‘œπ‘Ÿπ΄π‘™π‘™ (𝑙𝑖𝑠𝑑 𝑛) $ βˆ– 𝑑𝑒π‘₯𝑑 βˆ’ >
𝑓 π‘œπ‘Ÿπ΄π‘™π‘™ (𝑙𝑖𝑠𝑑 π‘š) $ βˆ– π‘˜π‘’π‘¦π‘  βˆ’ >
π‘’π‘žπ‘’π‘–π‘£π‘ƒ π‘Ÿπ‘œπ‘π‘†π‘’π‘žπ‘ƒ 𝑖𝑝 (𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦π‘ )

   We can only verify the property for a fixed text size at the time.
π‘ π‘Žπ‘‘π‘§π‘œπ‘œ π‘’π‘žπ‘’π‘–π‘£π‘ƒ π‘Ÿπ‘œπ‘π‘†π‘’π‘žπ‘ƒ 𝑖𝑝𝐹 π‘œπ‘Ÿπ‘†π‘–π‘§π‘’ (π‘™π‘’π‘›π‘”π‘‘β„Ž 𝑑𝑒π‘₯𝑑) 128
   For the implementation of the pipelined architecture, we check its equivalence to the behav-
ioral description using induction. Since the inner components are the same for the sequential
architecture we do not need to verify their equivalence.


βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑏, 𝑐, 𝑑, 𝑒 ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]]; π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™π΅π‘œπ‘œπ‘™]]]];
𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘  (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘ (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))

Basis:

𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ (0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )
π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )
β‡’ 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ (0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(0, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))


Induction step:
βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑏, 𝑐, 𝑑, 𝑒, ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]], π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) β‡’

𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ ((π‘›βˆ’1), (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘((π‘›βˆ’1), (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))

𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))
= 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐((𝑛, (π‘Žπ‘π‘  𝑏, π‘Žπ‘π‘  𝑐, π‘Žπ‘π‘  𝑑, π‘Žπ‘π‘  𝑒), π‘Žπ‘π‘  π‘˜π‘’π‘¦π‘ ))
= 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(((𝑛 βˆ’ 1), (𝑏𝑠 , 𝑐𝑠 , 𝑑𝑠 , 𝑒𝑠 ), π‘˜π‘’π‘¦π‘ ))
π‘€π‘–π‘‘β„Ž 𝑏𝑠 = π‘Žπ‘‘π‘‘πΎπ‘†(π‘Žπ‘π‘  𝑒, π‘˜)
𝑐𝑠 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘π‘  𝑏)
𝑑𝑠 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(π‘Žπ‘π‘  𝑐)
𝑒𝑠 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ π‘†(π‘Žπ‘π‘  𝑑)

π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))
= π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘((𝑛 βˆ’ 1), (𝑏𝑖 , 𝑐𝑖 , 𝑑𝑖 , 𝑒𝑖 ), π‘˜π‘’π‘¦π‘ ))
π‘€π‘–π‘‘β„Ž 𝑏𝑠 = π‘Žπ‘‘π‘‘πΎπΌ(𝑒, π‘˜)
𝑐𝑖 = 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼𝑏
𝑑𝑖 = π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌπ‘
𝑒𝑖 = π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ πΌπ‘‘

π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘Žπ‘π‘  𝑒, π‘˜) = π‘Žπ‘π‘ (π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ(𝑒, π‘˜)) β‡’ 𝑏𝑠 = π‘Žπ‘π‘  𝑏𝑖
𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘π‘  𝑏) = π‘Žπ‘π‘ (𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 𝑏) β‡’ 𝑐𝑠 = π‘Žπ‘π‘  𝑐𝑖
π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(π‘Žπ‘π‘  𝑐) = π‘Žπ‘π‘ (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ 𝑐) β‡’ 𝑑𝑠 = π‘Žπ‘π‘  𝑑𝑖
π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ π‘†(π‘Žπ‘π‘  𝑑) = π‘Žπ‘π‘ (π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ πΌ 𝑑) β‡’ 𝑒𝑠 = π‘Žπ‘π‘  𝑒𝑖

β‡’ 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(((𝑛 βˆ’ 1), (𝑏𝑠 , 𝑐𝑠 , 𝑑𝑠 , 𝑒𝑠 ), π‘˜π‘’π‘¦π‘ ))
= 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(((𝑛 βˆ’ 1), (π‘Žπ‘π‘  𝑏𝑖 , π‘Žπ‘π‘  𝑐𝑖 , π‘Žπ‘π‘  𝑑𝑖 , π‘Žπ‘π‘  𝑒𝑖 ), π‘˜π‘’π‘¦π‘ ))
= 𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ ((𝑛 βˆ’ 1), (𝑏𝑖 , 𝑐𝑖 , 𝑑𝑖 , 𝑒𝑖 ), π‘˜π‘’π‘¦π‘ )
= π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘((𝑛 βˆ’ 1), (𝑏𝑖 , 𝑐𝑖 , 𝑑𝑖 , 𝑒𝑖 ), π‘˜π‘’π‘¦π‘ ))

β‡’ βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑏, 𝑐, 𝑑, 𝑒, ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]], π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐(π‘Žπ‘π‘ (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))

  We verify the decryption unit in the same way as the encryption one.

βˆ€ 𝑛 ∈ 𝐼𝑛𝑑; 𝑏, 𝑐, 𝑑, 𝑒, ∈ [[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]], π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
𝑠𝑑𝑒𝑝𝑃 𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐(π‘Žπ‘π‘ (𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (𝑠𝑑𝑒𝑝𝑃 π‘–π‘π‘’πΌπ‘šπ‘π·π‘’π‘(𝑛, (𝑏, 𝑐, 𝑑, 𝑒), π‘˜π‘’π‘¦π‘ ))

  Now that we verified the equivalence between the pipelined step function’s implementation
and its specification; the equivalence of the upper-components is verified.

βˆ€ π‘π‘™π‘œπ‘π‘˜π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]], π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐𝐹 𝑆𝑀 (π‘Žπ‘π‘ (π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘π‘–π‘π‘’πΌπ‘šπ‘πΈπ‘›π‘πΉ 𝑆𝑀 (π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ ))

βˆ€ π‘π‘™π‘œπ‘π‘˜π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]], π‘˜π‘’π‘¦π‘  ∈ [[[[π‘†π‘–π‘”π‘›π‘Žπ‘™ π΅π‘œπ‘œπ‘™]]]];
𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐𝑐𝐹 𝑆𝑀 (π‘Žπ‘π‘ (π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ )) = π‘Žπ‘π‘ (π‘π‘–π‘π‘’πΌπ‘šπ‘π·π‘’π‘πΉ 𝑆𝑀 (π‘π‘™π‘œπ‘π‘˜π‘ , π‘˜π‘’π‘¦π‘ ))

β‡’ βˆ€ π‘œπ‘ ∈ 𝐼𝑛𝑑, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦ ∈ [πΆβ„Žπ‘Žπ‘Ÿ];
𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐴𝐸𝑆(π‘Žπ‘π‘ (π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦)) = π‘Žπ‘π‘ (π‘π‘–π‘π‘’πΌπ‘šπ‘π΄πΈπ‘†(π‘œπ‘, 𝑑𝑒π‘₯𝑑, π‘˜π‘’π‘¦))

   In table I, we show how long the verification process took for the main sub-components and
of the complete AES sequential circuit. As we can notice, all the theorems that has been proved
automatically using the Lava’s SAT solver, took less than 2s. As for theorems (3) and (4), which
express the equivalence between the sequential encryption FSM specification (sEFSMS) and its
implementation (sEFSMI), and between the sequential decryption FSM specification (sDFSMS)
and its implementation (sDFSMI) respectively; they were proved manually using induction in
a simple straightforward way. Each of these theorems took from 3 to 5 minutes to be proved.
This makes the total amount of time needed for the verification of the whole circuit 490.5 s (A =
the total of the Automatic verification / M = the total of the Manual verification).
   Table II shows the time that was taken for the verification of the AES pipelined circuit.
Theorems (5) and (6), which express the equivalence between the specification of the sequential
architecture and that of the pipelined one, where proved automatically using Lava’s SAT solver.
As for the verification of the pipelined implementation against its verified specification, we
proved theorems (7) and (8) using induction. This makes the total of the verification time for
the pipelined circuit 421.97 s.
           Component Property ...................................... Theorem   Method Verification
                        number                                                        Time (s)
           AES Spec     βˆ€π‘₯, π·π‘’π‘π‘Ÿπ‘¦π‘π‘‘π‘–π‘œπ‘›(πΈπ‘›π‘π‘Ÿπ‘¦π‘π‘‘π‘–π‘œπ‘› π‘₯) = π‘₯                       SAT    1.05
                        .............. (1)
           Mux          βˆ€π‘₯, π‘šπ‘’π‘₯𝑆(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (π‘šπ‘’π‘₯𝐼 π‘₯)                          SAT      1.78
           Xor          βˆ€π‘₯, π‘₯π‘œπ‘Ÿπ‘†(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (π‘₯π‘œπ‘ŸπΌ π‘₯)                          SAT      0.73
           AddKey       βˆ€π‘₯, π‘Žπ‘‘π‘‘πΎπ‘’π‘¦π‘†(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (π‘Žπ‘‘π‘‘πΎπ‘’π‘¦πΌ π‘₯)                    SAT      1.08
           SubBytes     βˆ€π‘₯, 𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝑆(π‘Žπ‘π‘                  π‘₯)               =   SAT      1.18
                        π‘Žπ‘π‘ (𝑠𝑒𝑏𝐡𝑦𝑑𝑒𝑠𝐼 π‘₯)
           ShiftRows    βˆ€π‘₯, π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ π‘†(π‘Žπ‘π‘                  π‘₯)             =   SAT      1.18
                        π‘Žπ‘π‘ (π‘ β„Žπ‘–π‘“ π‘‘π‘…π‘œπ‘€π‘ πΌ π‘₯)
           MixClms      βˆ€π‘₯, π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ π‘†(π‘Žπ‘π‘                    π‘₯)             =   SAT      0.86
                        π‘Žπ‘π‘ (π‘šπ‘–π‘₯πΆπ‘™π‘šπ‘›π‘ πΌ π‘₯)
           KeyExp       βˆ€π‘₯, π‘˜π‘’π‘¦πΈπ‘₯𝑝𝑆(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (π‘˜π‘’π‘¦πΈπ‘₯𝑝𝐼 π‘₯)                    SAT       0.72
           AESEnc       βˆ€π‘₯, 𝑠𝐸𝐹 𝑆𝑀 𝑆(π‘Žπ‘π‘                  π‘₯)                =   Induction ≃ 300
                        π‘Žπ‘π‘ (𝑠𝐸𝐹 𝑆𝑀 𝐼 π‘₯) .... (2)
           InvSubBytes βˆ€π‘₯, 𝑖𝑛𝑣𝑆𝐡𝑆(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (𝑖𝑛𝑣𝑆𝐡𝐼 π‘₯)                       SAT       0.72
           InvShiftRows βˆ€π‘₯, 𝑖𝑛𝑣𝑆𝑅𝑆(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (𝑖𝑛𝑣𝑆𝑅𝐼 π‘₯)                      SAT       0.6
           InvMixClms βˆ€π‘₯, 𝑖𝑛𝑣𝑀 𝐢𝑆(π‘Žπ‘π‘  π‘₯) = π‘Žπ‘π‘ (𝑖𝑛𝑣𝑀 𝐢𝐼 π‘₯)                      SAT       0.6
           AESdec       βˆ€π‘₯, 𝑠𝐷𝐹 𝑆𝑀 𝑆(π‘Žπ‘π‘                  π‘₯)                =   Induction ≃ 180
                        π‘Žπ‘π‘ (𝑠𝐷𝐹 𝑆𝑀 𝐼 π‘₯) .... (3)
           Total                                                                        A= 10.5
           (AESseq
           Circuit)                                                                     M= 480
Table 1
Verification time of the sequential AES circuit and its inner-components.


   Finally, in table III, we recapitulate the different works related to the proposed approach. As
we can see, the majority of the existing works are based on an imperative approaches. These
approaches are well suited for simulation [2],[3], but we notice that it is still possible to use them
for formal verification as well [1],[4],[5],[8],[9],[10]. In this case, the description for the design
and verification is long and complex. Only one functional approach beside ours exists that
targeted the cryptographic circuits [11]; no details about the verification time were mentioned.
A couple of the existing works are based on an algebraic approach [6],[7]; similarly to our work,
they use the hierarchy technique for proof decomposition; which makes the verification process
easier. As we can see, our proposed methodology takes half the time for the verification of the
same cryptographic circuit.


5. Conclusions
In this paper, we presented a formal design and verification methodology for symmetric cryp-
tographic circuits. We combine the two techniques (induction and SAT solver) for verifying
different parts of the implementation. The proposed approach was demonstrated over both
sequential and pipelined architectures of the symmetric cipher AES128. As prospects, we aim
to optimize the methodology into a fully automtic one, and to be able to design and verify the
           Component Property ...................................... Theorem   Method Verification
                      number                                                          Time (s)
           AESencSpec βˆ€π‘₯, π‘ π‘’π‘žπ‘†π‘π‘’π‘πΈπ‘›π‘ π‘₯ = 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐸𝑛𝑐 π‘₯                         SAT    1.12
                      ............ (4)
           AESdecSpec βˆ€π‘₯, π‘ π‘’π‘žπ‘†π‘π‘’π‘π·π‘’π‘ π‘₯ = 𝑝𝑖𝑝𝑒𝑆𝑝𝑒𝑐𝐷𝑒𝑐 π‘₯                         SAT      0.85
                      ............ (5)
           AESencImp βˆ€π‘₯, 𝑝𝐸𝐹 𝑆𝑀 𝑆(π‘Žπ‘π‘                     π‘₯)                =   Induction ≃ 240
                      π‘Žπ‘π‘ (𝑝𝐸𝐹 𝑆𝑀 𝐼 π‘₯) .... (6)
           AESdecImp βˆ€π‘₯, 𝑝𝐷𝐹 𝑆𝑀 𝑆(π‘Žπ‘π‘                     π‘₯)                =   Induction ≃ 180
                      π‘Žπ‘π‘ (𝑝𝐷𝐹 𝑆𝑀 𝐼 π‘₯) .... (7)
           Total (AE-                                                                   A= 1.97
           Spip
           Circuit)                                                                     M= 420
Table 2
Verification time of the pipelined AES circuit.

   Work         Approach        Verification Method                Cryptographic circuit         Verification
                                                                                                 Time (s)
   [5] 2003     Imperative      Formal methods                     DES                           59
   [10] 2004    Imperative      Formal methods/simulation          AES128                        /
   [1] 2006     Imperative      Theorem proving                    SHA1                          /
   [8] 2007     Imperative      Equivalence checking               Pipelined KASUMI              180 .. 540
   [11] 2007    Functional      Formal methods                     AES128                        /
   [4] 2008     Imperative      Equivalence checking               Pipelined KASUMI              180 .. 540
   [6] 2012     Algebraic       Formal methods                     AES128 datapath               800
   [7] 2014     Algebraic       Formal methods                     AES128                        844
   [3] 2014     Imperative      Simulation                         AES256                        /
   [2] 2015     Imperative      Simulation                         TDES                          /
   [9] 2017     Imperative      Formal methods                     Pipelined AES128              2300
   This work    Functional      Formal methods                     Sequential AES128             490.5
   This work    Functional      Formal methods                     Pipelined AES128              421.97
Table 3
Comparative table of the related literature’s verification methods and time.


super-scalar architectures.


References
 [1] Toma, D. "Vérification Formelle des systèmes numériques par démonstration de théorèmes:
     application aux composants cryptographiques" (Doctoral dissertation) (2006).
 [2] Singh, Kirat Pal, and Shivani Parmar. "Design of high performance MIPS cryptography
     processor based on T-DES algorithm." arXiv preprint arXiv:1503.03166 (2015).
 [3] Ali, Imran, Gulistan Raja, and Ahmad Khalil Khan. "A 16-Bit Architecture of Advanced
     Encryption Standard for Embedded Applications." 2014 12th International Conference on
     Frontiers of Information Technology. IEEE, (2014).
 [4] Lam, Chiu Hong. "Verification of pipelined ciphers". MS thesis. University of Waterloo,
     (2009).
 [5] Clarke, E., Kroening, D. "Hardware verification using ANSI-C programs as a reference". In
     Proceedings of the ASP-DAC Asia and South Pacific Design Automation Conference. pp.
     308-311. IEEE. (2003).
 [6] Homma, Naofumi, Kazuya Saito, and Takafumi Aoki. "A Formal Approach to Designing
     Cryptographic Processors Based on 𝐺𝐹 (2π‘š ) Arithmetic Circuits." IEEE Transactions on
     Information Forensics and Security vol. 7, no 1, p. 3-13. (2011).
 [7] Homma, Naofumi, Kazuya Saito, and Takafumi Aoki. "Toward formal design of practical
     cryptographic hardware based on Galois field arithmetic." IEEE Transactions on Computers.
     vol. 63, no 10, p. 2604-2613 (2013).
 [8] Lam, Chiu Hong, and Mark D. Aagaard. "Formal Verification of a Pipelined Cryptographic
     Circuit Using Equivalence Checking and Completion Functions." 2007 Canadian Conference
     on Electrical and Computer Engineering. IEEE, p. 1401-1404. (2007).
 [9] Bond, Barry, et al. "Vale: Verifying high-performance cryptographic assembly code." 26th
     USENIX Security Symposium (USENIX Security 17). p. 917-934. (2017).
[10] Kim, Ho Won, and Sunggu Lee. "Design and implementation of a private and public key
     crypto processor and its application to a security system." IEEE Transactions on Consumer
     Electronics.vol. 50, no 1, p. 214-224. (2004).
[11] Lewis, Jeff. "Cryptol: specification, implementation and verification of high-grade cryp-
     tographic applications." Proceedings of the 2007 ACM workshop on Formal methods in
     security engineering. p. 41-41.(2007).
[12] Wolfs, Davy, et al. "Design automation for cryptographic hardware using functional
     languages." Proceedings of the 32nd WIC Symposium on Information Theory in the
     Benelux. Werkgemeenschap voor Informatie-en Communicatietheorie.; Netherlands, p.
     194-201. (2011).
[13] Guo, Xiaolong, et al. "Pre-silicon security verification and validation: A formal perspective."
     Proceedings of the 52nd Annual Design Automation Conference. p. 1-6. (2015).
[14] Daemen, Joan, and Vincent Rijmen. The design of Rijndael: AES-the advanced encryption
     standard. Springer Science and Business Media, (2013).
[15] Gaj, K., and Chodowiec, P. (2009). FPGA and ASIC implementations of AES. In Crypto-
     graphic engineering (pp. 235-294). Springer, Boston, MA.