Gavin Keighren's Curriculum Vitae
Listed below are my main academic qualifications and achievements along with my employment history, selected publications and some additional information.
For a full list of my publications, including abstracts, please see here.
If you require anything further please contact me at gkeighren@hotmail.com and I'll do my best to pass on what you're looking for.
Please note that this page will print black-on-white with certian elements such as the navigation bar removed.
|
|
|
|
Education and Qualifications |
Top |
| Sep '07 – Present |
|
The University of Edinburgh
|
|
|
PhD in Informatics
|
|
|
| • |
Research aim is to investigate how the analysis of security APIs can be improved.
This is a continuation of the line of research initially undertaken for my Masters thesis, and is likely to culminate in the production of new analysis tools and/or methods.
|
|
| Sep '05 – Aug '06 |
|
The University of Edinburgh
|
|
|
MSc in Artificial Intelligence
|
|
Pass with Distinction
|
|
|
| • |
Specialised in knowledge representation and reasoning, which focuses on the discovery, capture and use of information in an efficient and beneficial manner.
|
| • |
Modules studied: Automated Reasoning,
Automated Planning,
Knowledge Modelling and Management,
Parallel Programming Languages and Systems,
Design and Analysis of Parallel Algorithms,
Fundamentals of Artificial Intelligence,
Introduction to Java Programming, and
Multi-Agent Semantic Web Systems.
|
| • |
Course also involved a research review covering the state-of-the-art in any sub-field of artificial intelligence.
The web page for the module is here, and my review can be found here.
|
| • |
For my thesis, I investigated methods to formally verify the correctness of security APIs for key-management systems.
|
|
| Oct '99 – Jun '03 |
|
The University of Edinburgh
|
|
|
BSc (Hons) in Artificial Intelligence with Computer Science
|
|
2:2
|
|
|
| • |
Accredited by the British Computer Society.
|
| • |
Grade based upon work carried out in years three and four of the course.
|
| • |
Third year modules: Algorithms and Data Structures,
Automated Reasoning,
Computer Communications,
Database Systems,
Functional Programming and Specification,
Knowledge Engineering,
Knowledge Representation,
Learning from Data 1,
Professional Issues,
AI Large Practical,
System Design Project.
|
| • |
Fourth year modules: Computer Algebra,
Computer Graphics,
Formal Programming Language Semantics,
Knowledge Management,
Modelling and Simulation,
Propositional Methods,
Honours Project.
|
|
|
|
|
|
Employment History |
Top |
| Jun '07 – Aug '07 |
|
Contract Employment at The University of Edinburgh
|
|
|
Worked within the School of Informatics to create products which could be used to grab the interest of potential future students, as well as demonstrate some of the work undertaken within the School of Informatics.
| • |
Developed a workshop on cryptography aimed at high-school pupils in their third or fourth year.
|
| • |
Produced an interactive software demonstration of a security API attack which could discover PINs from encrypted ATM traffic.
The program was (intentionally) unable to obtain actual PINs, as it did not communicate with a security module in a live ATM.
Furthermore, the attack has been known for some time now and is protected against in practice.
|
|
| Sep '06 – Oct '06 |
|
Research Assistant at The University of Edinburgh
|
|
|
Worked within the School of Informatics in order to continue the research which I had carried out for my Masters thesis.
| • |
Helped design and develop a custom decision procedure for the analysis of IBM's CCA API, which is used by security modules in a large number of ATMs.
This work along with results from my MSc thesis were included in a paper accepted to the TACAS '07 conference.
A technical report based upon the submitted paper can be found
hereat http://www.inf.ed.ac.uk/publications/report/0863.html.
|
| • |
Authored a technical report containing the research originally presented in my MSc thesis. It can be found
hereat http://www.inf.ed.ac.uk/publications/report/0862.html.
|
| • |
Modified technical report for submission to the 2006 Special Issue of the Information and Computation journal.
|
|
| Mar '04 – Aug '05 |
|
Assistant Researcher at ITC‑irst, Trento, Italy
|
|
|
Worked within the Formal Methods Group (part of the Autonomous Reasoning Systems Division) as a member of the team responsible for the continuing development of the model checker NuSMV.
| • |
From March 2004 to September 2004, worked on an EU funded part of the CALCULEMUS project — one goal of which is to develop the next generation of computer-aided verification tools that harness the power of computer algebra systems. Work included:
| |
– |
adding extra functionality to NuSMV.
|
| |
– |
benchmarking and testing the software.
|
| |
– |
investigating and implementing methods to reduce the run-time of the SAT-based Bounded Model Checking routines.
|
|
| • |
From October 2004 to December 2004, worked on the Prosyd project, which has a wider aim of establishing an industry-wide paradigm for the design and development of electronic systems. Work included:
| |
– |
close analysis of how NuSMV modelled electrical circuits.
|
| |
– |
benchmarking and testing of new algorithms that were developed.
|
|
| • |
From January 2005 to August 2005, worked remotely from home in Edinburgh.
Focused on modifying NuSMV's internal representation of models to allow expressions involving unbounded integers.
Goal was to increase the expressiveness of NuSMV and was motivated by work previously carried out on the MathSAT tool.
|
|
|
|
|
|
Selected Publications |
Top |
| [1] |
|
V. Cortier, G. Keighren and G. Steel.
Automatic Analysis of the Security of XOR‑Based Key Management Schemes.
In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2007), Lecture Notes in Computer Science number 4424, pages 538–552.
Available online at http://www.loria.fr/~cortier/Papiers/TACAS07.pdf.
|
| [2] |
|
G. Keighren.
Model Checking IBM's Common Cryptographic Architecture API.
Technical Report EDI‑INF‑RR‑0862, School of Informatics, The University of Edinburgh, Oct. 2006.
Available from http://www.inf.ed.ac.uk/publications/report/.
|
| [3] |
|
G. Keighren.
Model Checking Security APIs.
MSc Thesis, The University of Edinburgh, Aug. 2006.
Available from http://www.inf.ed.ac.uk/publications/thesis/msc.html.
|
|
|
|
|
Awards |
Top |
| • |
EPSRC Studentship funding for my PhD in Informatics.
|
| • |
2006 Jim Howe prize, awarded to "the best student in MSc Artificial Intelligence" at The University of Edinburgh.
|
| • |
EPSRC Studentship funding for my MSc in Artificial Intelligence.
|
|
|
|
|
Additional Skills and Experience |
Top |
| • |
Good knowledge of a number of programming languages, including C/C++, Java, Prolog, and standard HTML, along with the document typesetting language LaTeX.
|
| • |
Experience with the three main operating systems: Windows, Linux and OS X, as well as the Unix bash shell.
|
| • |
Regular member of local football team throughout High School.
|
| • |
Junior team member at Ratho Park Golf Club from 1997 to 2000.
|
| • |
Play golf on a regular basis — handicap is around 10.
|
| • |
Full, clean, UK driving licence held since April 1999.
|
|
|
Contact Information |
| The University of Edinburgh |
| Old College |
| South Bridge |
| Edinburgh |
| EH8 9YL |
|
| Tel: | +44 (0)131 650 1000 |
| Fax: | +44 (0)131 650 2147 |
| Web: | www.ed.ac.uk |
|
| The School of Informatics |
| Appleton Tower |
| Crichton Street |
| Edinburgh |
| EH8 9LE |
|
| Tel: | +44 (0)131 650 2690 |
| Fax: | +44 (0)131 651 1426 |
| Web: | www.inf.ed.ac.uk |
|
| ITC‑irst |
| Via Sommarive, 18 |
| 38050 Povo (Trento) |
| Italy |
|
| Tel: | +39 0461 31 44 44 |
| Fax: | +39 0461 30 20 40 |
| Web: | www.itc.it/irst |
|
|
|
