Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le Chapitre 6 vise la composition.Nous montrons dans le Chapitre 3 comment reduire certains problemes d'une algebre quotient des termes a l'algebre libre des termes en utilisant des ensembles fortement complets de variants. Nous montrons que, si l'algebre quotient est donnee par un systeme de reecriture de termes convergent et optimalement reducteur (optimally reducing), alors des ensembles fortement complets de variants existent et sont finis et calculables.Dans le Chapitre 4, nous montrons que l'equivalence statique pour (des classes) de theories equationnelles, dont les theories sous-terme convergentes, la theorie de l'engagement a trappe (trapdoor commitment) et la theorie de signature en aveugle (blind signatures), est decidable en temps polynomial. Nous avons implemente de maniere efficace cette procedure.Dans le Chapitre 5, nous etendons la procedure de decision precedente a l'equivalence de traces. Nous utilisons des ensembles fortement complets de variants du Chapitre 3 pour reduire le probleme a l'algebre libre. Nous modelisons chaque trace du protocole comme une theorie de Horn et nous utilisons un raffinement de la resolution pour resoudre cette theorie. Meme si nous n'avons pas reussi a prouver que la procedure de resolution termine toujours, nous l'avons implementee et utilisee pour donner la premiere preuve automatique de l'anonymat dans le protocole de vote electronique FOO.Dans le Chapitre 6, nous etudions la composition de protocoles. Nous montrons que la composition de deux protocoles qui utilisent des primitives cryptographiques disjointes est sure s'ils ne revelent et ne reutilisent pas les secrets partages. Nous montrons qu'une forme d'etiquettage de protocoles est suffisante pour assurer la disjonction pour un ensemble fixe de primitives cryptographiques. / This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

Predicting the location and timing of rainfall events has important social and economic impacts. It is also important to have the ability to predict the amount of rainfall accurately. In operational centres forecasters use deterministic model output data as guidance for a subjective probabilistic rainfall forecast. The aim of this research is to determine the skill in an objective multi-model, multi-institute objective probabilistic forecast system. This was done by obtaining the rainfall forecast of two high-resolution regional models operational in South Africa. The first model is the Unified Model (UM) which is operational at the South African Weather Service. The UM contributed three members which differ in physics, data assimilation techniques and horisontal resolution. The second model is the Conformal-Cubic Atmospheric Model (CCAM) which is operational at the Council for Scientific and Industrial Research which in turn contributed two members to the ensemble system differing in horisontal resolution. A single-model ensemble was constructed for the UM and CCAM models respectively with each of the individual members having equal weights. The UM and CCAM single-model ensemble prediction models have been used in turn to construct a multi-model ensemble prediction system, using simple un-weighted averaging. The multi-model system was used to predict the 24-hour rainfall totals for three austral summer half-year seasons of 2006/07 to 2008/09. The forecast of this system was rigorously tested using observed rainfall data for the same period. From the multi-model system it has been found that the probabilistic forecast has good significant skill in predicting rainfall. The multi-model system proved to have skill and shows discrimination between events and non-events. This study has shown that it is possible to make an objective probabilistic rainfall forecast by constructing a multi-model, multi-institute system with high resolution regional models currently operational in South Africa. Thus, probabilistic rainfall forecasts with usable skill can be made with the use of a multi-model short-range ensemble prediction system over the South African domain. Such a system is not currently operational in South Africa. Copyright / Dissertation (MSc)--University of Pretoria, 2012. / Geography, Geoinformatics and Meteorology / Unrestricted

Alloy is a lightweight formal modeling tool that generates instances of a software specification to check properties of the design. This work demonstrates the use of Alloy for the rapid development of autonomous vehicle driving protocols. We contribute two driving protocols: a Normal protocol that represents the unpredictable yet safe driving behavior of typical human drivers, and a Connected protocol that employs connected technology for cooperative autonomous driving. Using five properties that define safe and productive driving actions, we analyze the performance of our protocols in mixed traffic. Lightweight formal modeling is a valuable way to reason about driving protocols early in the development process because it can automate the checking of safety and productivity properties and prevent costly design flaws.

The goal of this thesis is to analyze and to find solutions of optimization problems derived from automation of functional verification of hardware using artificial neural networks. Verification of any integrated circuit (so called Design Under Verification, DUV) using technique called coverage-driven verification and universal verification methodology (UVM) is carried out by sending stimuli inputs into DUV. The verification environment continuously monitors percentual coverage of DUV functionality given by the specification. In current context, coverage stands for measurable property of DUV, like count of verified arithemtic operations or count of executed lines of code. Based on the final coverage, it is possible to determine whether the coverage of DUV is high enough to declare DUV as verified. Otherwise, the input stimuli set needs to change in order to achieve higher coverage. Current trend is to generate this set by technique called constrained-random stimulus generation. We will practice this technique by using pseudorandom program generator (PNG). In this paper, we propose multiple solutions for following two optimization problems. First problem is ongoing modification of PNG constraints in such a way that the DUV can be verified by generated stimuli as quickly as possible. Second one is the problem of seeking the smallest set of stimuli such that this set verifies DUV. The qualities of the proposed solutions are verified on 32-bit application-specific instruction set processors (ASIPs) called Codasip uRISC and Codix Cobalt.

The topic of the master´s thesis is to verify Acquisition Engine and Tracking Engine in the Microcore GNSS Baseband digital circuit from Honeywell. Theoretical part contains a brief introduction into the satellite position determination, basic principles of the verified blocks is given and UVM methodology is introduced. Practical part contains requirements, test cases and test procedures. The verification environment is also described. In the last part of the thesis is the verification process and it´s results.

This work aims at methods, which are suitable for mixed-signal integrated circuit verification. The emphasis is on the Assertion-based verification. In practice there are two languages, which can be used for this method - PSL and SystemVerilog. These languages are compared between each other and individually tested to find their capabilities, functional limits and restrictions. One of them will be integrated into verification flow of SCG Czech Design Center s. r. o. company to develop ABV methodology in analog and mixed-signal domain.

The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.

NULL Convention Logic (NCL) is a Quasi-Delay Insensitive (QDI) asynchronous design paradigm that aims to tackle some of the major problems synchronous designs are facing as the industry trend of increased clock rates and decreased feature size continues. The clock in synchronous designs is becoming increasingly difficult to manage and causing more power consumption than ever before. NCL circuits address some of these issues by requiring less power, producing less noise and electro-magnetic interference, and being more robust to Process, Voltage, and Temperature (PVT) variations. With the increase in popularity of asynchronous designs, a formal verification methodology is crucial for ensuring these circuits operate correctly. Four automated formal verification methodologies have been developed, three to ensure delay-insensitivity of an NCL circuit (i.e., prove Input-Completeness, Observability, and Completion-Completeness properties), and one to aid in proving functional equivalence between an NCL circuit and its synchronous counterpart. Note that an NCL circuit can be functionally correct and still not be input-complete, observable, or completion-complete, which could cause the circuit to operate correctly under normal conditions, but malfunction when circuit timing drastically changes (e.g., significantly reduced supply voltage, extreme temperatures). Since NCL circuits are implemented using dual-rail logic (i.e., 2 wires, rail0 and rail1, represent one bit of data), part of the functional equivalence verification involves ensuring that the NCL rail0 logic is the inverse of its rail1 logic. Equivalence verification optimizations and alternative invariant checking methods were investigated and proved to decrease verification times of identical circuits substantially. This work will be a major step toward NCL circuits being utilized more frequently in industry, since it provides an automated verification method to prove correctness of an NCL implementation and equivalence to its synchronous specification, which is the industry standard.

This thesis is focused on tools which are used to analyzed security protocols. In the beginning of the thesis key goals of security protocols are mentioned and also basic attacks on them are illustrated. Subsequently basic verification techniques, specification languages and verification tools are described. Next part of thesis contains description of protocols in common syntax. Then the main standards used for evaluation of information security products are mentioned. In the end of thesis two well-known verification tools – AVISPA and Scyther - are described and compared to designed methodology of comparing verification tools and their outputs.

Tato diplomová práce se zabývá verifikací integrovaných obvodů pracujících ve smíšeném módu. Teoretická část práce obsahuje přehled moderních verifikačních metod a zaměřuje se zejména na „assertion based methodology“ . V praktické části práce jsou pak rozebrány popisné jazyky používané u této metody, a následně je vytvořen kód pro verifikaci bloku řídícího obvodu spínaných zdrojů.