This thesis presents the ASIC implementation of the RSA algorithm, which is one of the most widely used Public Key Cryptosystems (PKC) in the world. In RSA Cryptosystem, modular exponentiation of large integers is used for both encryption and decryption processes. The security of the RSA increases as the number of the bits increase. However, as the numbers become larger (1024-bit or higher) the challenge is to provide architectures, which can be implemented in hardware, operate at high clock speeds, use a minimum of resources and can be used in real-time applications. In this thesis, a semi-custom VLSI implementation of the RSA Cryptosystem is performed for both 512-bit and 1024-bit processes using 0.35&micro / m AMI Semiconductor Standard Cell Libraries. By suiting the design into a systolic and regular architecture, the broadcasting signals and routing delays are minimized in the implementation. With this regular architecture, the results of 3ns clock period (627Kbps) using 87K gates (8.7mm2 with I/O pads) for the 512-bit implementation, and 4ns clock period (237Kps) using 132K gates (10.4mm2 with I/O pads) for the 1024-bit implementation have been achieved. These results are obtained for the worst-case conditions and they include the post-layout routing delays. The design is also verified in real time using the Xilinx V2000E FPGA on the Celoxica RC1000 Hardware. The 1024-bit VLSI implementation has been sent to IMEC for fabrication as a prototype chip through Europractice Multi-Project Wafer (MPW) runs.

This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

Maintenance of the structural integrity and damage detection are critical for all massive and complicated new and aging structures. A structural health monitoring (SHM) system intends to identify damage on the structure under monitoring, so that necessary action can be taken in advance to avoid catastrophic results. Impedance-based SHM utilizes a piezoelectric ceramic as a collocated actuator and sensor, which measures the electrical impedance of the piezoelectric ceramic over a certain frequency range. The impedance profile of a structure under monitoring is compared against a reference profile obtained from the healthy structure. An existing approach called the sinc method adopts a sinc wave excitation and performs traditional discrete Fourier transform (DFT) based structural condition assessment. The sinc method requires rather intensive computing and a digital-to-analog converter (DAC) to generate a sinc excitation signal. It also needs an analog-to-digital converter (ADC) to measure the response voltage, from which impedance profile is obtained through a DFT. This dissertation investigates system design approaches for impedance-based structural health monitoring (SHM), in which a primary goal is low power dissipation. First, we investigated behaviors of piezoelectric ceramics and proposed an electrical model in order to enable us to conduct system level analysis and evaluation of an SHM system. Unloaded and loaded piezoelectric ceramics were electrically modeled with lumped linear circuit components, which allowed us to perform system level simulations for various environmental conditions. Next, we explored a signaling method called the wideband method, which uses a pseudorandom noise (PN) sequence for excitation of the structure rather than a signal with a particular waveform. The wideband method simplifies generation of the excitation signal and eliminates a digital-to-analog converter (DAC). The system form factor and power dissipation is decreased compared to the previously existing system based on a sinc signal. A prototype system was implemented on a digital signal processor (DSP) board to validate its approach. Third, we studied another low-power design approach which employs binary signals for structural excitation and structural response measurement was proposed. The binary method measures only the polarity of a response signal to acquire the admittance phase, and compares the measured phase against that of a healthy structure. The binary method eliminates the need for a DAC and an ADC. Two prototypes were developed: one with a DSP board and the other with a microcontroller board. Both prototypes demonstrated reduction of power dissipation compared with those for the sinc method and for the wideband method. The microcontroller based prototype achieved an on-board SHM system. Finally, we proposed an analytical method to assess the quality of the damage detection for the binary method. Using our method, one can obtain the confidence level of a damage detection for a given damage distance. / Ph. D.

This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

Elliptic curves were first proposed as a basis for public key cryptography in the mid 1980's. They provide public key cryptosystems based on the difficulty of the elliptic curve discrete logarithm problem (ECDLP) , which is so called because of its similarity to the discrete logarithm problem (DLP) over the integers modulo a large prime. One benefit of elliptic curve cryptosystems (ECCs) is that they can use a much shorter key length than other public key cryptosystems to provide an equivalent level of security. For example, 160 bit ECCs are believed to provide about the same level of security as 1024 bit RSA. Also, the level of security provided by an ECC increases faster with key size than for integer based discrete logarithm (dl) or RSA cryptosystems. ECCs can also provide a faster implementation than RSA or dl systems, and use less bandwidth and power. These issues can be crucial in lightweight applications such as smart cards. In the last few years, ECCs have been included or proposed for inclusion in internationally recognized standards. Thus elliptic curve cryptography is set to become an integral part of lightweight applications in the immediate future. This thesis presents an analysis of several important issues for ECCs on lightweight devices. It begins with an introduction to elliptic curves and the algorithms required to implement an ECC. It then gives an analysis of the speed, code size and memory usage of various possible implementation options. Enough details are presented to enable an implementer to choose for implementation those algorithms which give the greatest speed whilst conforming to the code size and ram restrictions of a particular lightweight device. Recommendations are made for new functions to be included on coprocessors for lightweight devices to support ECC implementations Another issue of concern for implementers is the side-channel attacks that have recently been proposed. They obtain information about the cryptosystem by measuring side-channel information such as power consumption and processing time and the information is then used to break implementations that have not incorporated appropriate defences. A new method of defence to protect an implementation from the simple power analysis (spa) method of attack is presented in this thesis. It requires 44% fewer additions and 11% more doublings than the commonly recommended defence of performing a point addition in every loop of the binary scalar multiplication algorithm. The algorithm forms a contribution to the current range of possible spa defences which has a good speed but low memory usage. Another topic of paramount importance to ECCs for lightweight applications is whether the security of fixed curves is equivalent to that of random curves. Because of the inability of lightweight devices to generate secure random curves, fixed curves are used in such devices. These curves provide the additional advantage of requiring less bandwidth, code size and processing time. However, it is intuitively obvious that a large precomputation to aid in the breaking of the elliptic curve discrete logarithm problem (ECDLP) can be made for a fixed curve which would be unavailable for a random curve. Therefore, it would appear that fixed curves are less secure than random curves, but quantifying the loss of security is much more difficult. The thesis performs an examination of fixed curve security taking this observation into account, and includes a definition of equivalent security and an analysis of a variation of Pollard's rho method where computations from solutions of previous ECDLPs can be used to solve subsequent ECDLPs on the same curve. A lower bound on the expected time to solve such ECDLPs using this method is presented, as well as an approximation of the expected time remaining to solve an ECDLP when a given size of precomputation is available. It is concluded that adding a total of 11 bits to the size of a fixed curve provides an equivalent level of security compared to random curves. The final part of the thesis deals with proofs of security of key exchange protocols in the Canetti-Krawczyk proof model. This model has been used since it offers the advantage of a modular proof with reusable components. Firstly a password-based authentication mechanism and its security proof are discussed, followed by an analysis of the use of the authentication mechanism in key exchange protocols. The Canetti-Krawczyk model is then used to examine secure tripartite (three party) key exchange protocols. Tripartite key exchange protocols are particularly suited to ECCs because of the availability of bilinear mappings on elliptic curves, which allow more efficient tripartite key exchange protocols.