Formal Verification of Cryptographic Protocols

Public Key Infrastructures (PKIs) are a major enabling technology to allow secure eCommerce to be conducted over the Internet. The sucess of eCommerce in the long run will depend on many issues, but most notably will be user confidence in the security of tansactions on the Internet. This project will investigate the application of formal techniques to the specification, analysis and verification of public key infrastructures and related security protocols to order to prove (or disprove!) their security.

Formal Verification of Mobile Distributed Systems

Modern society has become reliant on software systems for many mission-critical and life-critical functions. Very little of this software has been proven to be correct and error-free despite our vunerablility to these software systems. One approach to verification of these software systems is to use formal mathematical logics and theorem provers. This project will investigate the use of the pi-calculus and term-rewriting for the specification and verification of distributed and embedded systems. The basic idea is to take a property of the system to be verified and using a weakest precondition semantics of the pi-calculus, that will be developed as part of the project, to generate the required preconditions on the system for this property to hold.

Generating behavioural specifications from semi-formal design methodologies.

UML is a popular design notations used in industry. The typical usage of UML is as a semi-formal graphical description of the system to be developed. The lack of logical/mathematical formality means that multiple interpretation of the same set of diagrams is possible and there is no way of verifying that a system behaves
in a specfied manner. The introduction of the Object Constraint Language, OCL,  has provided a means by which a UML diagram can be annotated with constraints on the objects in the system. These constraints are in the form of preconditions, postconditions and invariants. By themselves they do not enable a behavioural
specification of the system. This project will investigate whether a combination the UML state diagram, message sequence charts etc. (with restrictions) can be mapped in to a behavioural descritption of the system that is suitable for verifiaction.

Computer Go

This project will examine strategic planning in games by investigating how computers and play the game of Go. The history of the game Go streches back 4000 years and the game has essentially remained unchanged. It is a territorial game played on a board marked with a 19x19 grid, on which players place coloured stones. The winner is the player who has encircled the most space. Despite these, and other simple rules, the game of Go is strategically rich and has posed many problems for computers. The standard of the best Go programs are that of average amateurs. The search techniques developed for Computer Chess will not work. Computer Go represents many challenges in relation to strategy formulation, planning and evaluation

Learning Evaluation Functions in Computer Games from a Corpus of Expert Games

Todate computers' most successful approach to games such as chess is a combination of search and evaluation. While a lot of research effort has been invested in developing better search algorithms the evaluation functions have been largely ignored. The focus of this project is to investigate different techniques for training an evaluation function from a large corpus of games played by expert. As part of this project mut-dimensional evaluation functions and their resolution mechanisms will be compared against 1-dimensional evaluation functions.

If you are interested in these projects or similar project please contact me.