Thesis Topic Details

Topic ID:
157
Title:
Interpreting a formal security protocol language in an epistemic model checker
Supervisor:
Ron van der Meyden
Research Area:
Associated Staff
Assessor:
Kai Engelhardt
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
Pre-requisites:
Understanding of cryptographic protocols, excellence in formal methods, Haskell and C programming
Description:
CAPSL is a formal language that enables a cryptographic protocol to be formally
represented in a language that closely resembles the way that protocol
designers like to think about such protocols. It has been of interest to provide formal verification tools to analyze such protocols for correctness. One approach to this works with model checkers, of which epistemic model checkers are a special type, dealing with properties of the information possessed by agents in a system.

A translation from CAPSL to the epistemic model checker MCMAS,
enabling epistemic properties to be checked on CAPSL programs,
has been carried out in the thesis:

http://infoscience.epfl.ch/record/174319/files/Boureanu-IC-2011-PhD-Thesis.pdf

However, there are reasons to believe that the model checker MCK,
that we have developed at UNSW (http://www.cse.unsw.edu.au/~mck)
would be a better target for such a translation, since it provides native support an more efficient algorithms for a "perfect recall" interpretation
of knowledge.

The project would be to develop a tool translating CAPSL programs to
the MCK input format, enabling such programs to be checked using MCK,
and to conduct a comparative performance study with the translation to MCMAS. (This project may produce a publishable scientific paper.)
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.