Skip to main content

Formal threat and vulnerability analysis of a distributed ledger model


Sadie Creese
(World Economic Forum Cyber Security Centre, Strategic Advisory Board Member World Economic Forum Cyber Security Centre, Strategic Advisory Board Member)

Suitable for

MSc in Computer Science
Computer Science, Part B
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C


This project would utilise the process algebra CSP and associated model checker FDR to explore various types of threat and how they might successfully compromise a distributed ledger. This type of modelling would indicate possible attacks on a distributed ledger, and could guide subsequent review of actual designs and testing strategies for implementations. The modelling approach would be based on the crypto-protocol analysis techniques already developed for this modelling and analysis environment, and would seek to replicate the approach for a distributed ledger system. Novel work would include developing the model of the distributed ledger, considering which components are important, formulating various attacker models and also formulating the security requirements / properties to be assessed using this model-checking based approach.

Requirements: In order to succeed in this project students would need to have a working knowledge of the machine readable semantics of CSP and also the model checker FDR. An appreciation of threat models and capability will need to be developed.