|
UWSpace >
University of Waterloo >
Electronic Theses and Dissertations (UW) >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/10012/4267
|
| Title: | Verification of Pipelined Ciphers |
| Authors: | Lam, Chiu Hong |
| Keywords: | verification
cryptography
pipelining
cipher
kasumi
welch-gong
fpga
hardware
vhdl
completion functions |
| Approved Date: | 29-Jan-2009 |
| Date Submitted: | 2009 |
| Abstract: | The purpose of this thesis is to explore the formal verification technique of completion functions and equivalence checking by verifying two pipelined cryptographic circuits, KASUMI and WG ciphers. Most of current methods of communications either involve a personal computer or a mobile phone. To ensure that the information is exchanged in a secure manner, encryption circuits are used to transform the information into an unintelligible form. To be highly secure, this type of circuits is generally designed such that it is hard to analyze. Due to this fact, it becomes hard to locate a design error in the verification of cryptographic circuits. Therefore, cryptographic circuits pose significant challenges in the area of formal verification. Formal verification use mathematics to formulate correctness criteria of designs, to develop mathematical models of designs, and to verify designs against their correctness criteria.
The results of this work can extend the existing collection of verification methods as well as benefiting the area of cryptography. In this thesis, we implemented the KASUMI cipher in VHDL, and we applied the optimization technique of pipelining to create three additional implementations of KASUMI. We verified the three pipelined implementations of KASUMI with completion functions and equivalence checking. During the verification of KASUMI, we developed a methodology to handle the completion functions efficiently based on VHDL generic parameters. We implemented the WG cipher in VHDL, and we applied the optimization techniques of pipelining and hardware re-use to create an optimized implementation of WG. We verified the optimized implementation of WG with completion functions and equivalence checking. During the verification of WG, we developed the methodology of ``skipping" that can decrease the number of verification obligations required to verify the correctness of a circuit. During the verification of WG, we developed a way of applying the completion functions approach such that it can deal with a circuit that has been optimized with hardware re-use. |
| Program: | Electrical and Computer Engineering |
| Department: | Electrical and Computer Engineering |
| Degree: | Master of Applied Science |
| URI: | http://hdl.handle.net/10012/4267 |
| Appears in Collections: | Faculty of Engineering Theses and Dissertations
Electronic Theses and Dissertations (UW)
|
This item is protected by original copyright
|
All items in UWSpace are protected by copyright, with all rights reserved.
|
