BSc Final Year Project Software

Over the years I've been fortunate to supervise many undergraduate students working on their final year BSc Computer Science projects. These students have developed a wide range of useful studies, software tools and prototypes that are too numerous to list here. Below is a small selection of these. We make them freely available under a FreeBSD style license on the understanding that we do not provide any support.

Analyzing Authentication Protocols

For his final year BSc project Daithi O Crualaoich implemented a tool for reasoning about authentication protocols within the BSW Logic (also known as the Simple Logic). Theory Generation was used to provide the basic reasoning engine for the logic. Its a nice worked example of using TG in general (although our provided metric is incomplete; but we've found it to be quite workable in practice). There are two tools. The Verify tool takes a protocol specification, along with associated assumptions and goals, and attempts to verify the goals. The synthesis tool allows you to synthesise (viz, calculate) a protocol specification from a goal; the user manually interacts with the tool to direct it towards the designed protocol.

• Synthesis Tool synth.jar. Execute as java -jar synth.jar. The synthesis script for a (corrected version) of WooLam demonstrates its use.
• Verification Tool ver.jar. Execute as java -jar ver.jar .
• Some examples of protocol specifications in the logic: WooLam Protocol; Wide Mouth Frog.

Java implementation of KeyNote

For his final year BSc project Eoghan Huggard implemented, in Java, the KeyNote trust management system, as described in RFC 2704. The current tarball of his interpreter can be found here, and this includes some additional tools and code provided by Thomas Quillinan. You should use the examples as documentation in order to understand how to use the API in practice.

Trust Management of Change Control

Change Management systems have regulatory requirements and can therefore be regarded as critical system requiring a moderate degree of assurance. Thus, software providing Change Management control will need some form of assurance evaluation. Louise O'Driscoll used the JKeyNote tool to demonstrate that an architecture based around Trust Management can provide part of this assurance. A tarball of her prototype system is here and her project report is here.