David Williams

Dr David Williams

Lecturer in Secure Systems
+44 (0)1483 682646
16 BB 02



Dr David M. Williams is Lecturer in Secure Systems at the Department of Computer Science, University of Surrey. David returned to Surrey in May 2016, having previously studied for his PhD here between 2007 and 2011.

Prior to his current appointment he worked as Principal Research Engineer at Thales UK, where he worked on the design and implementation of products conforming to emerging industry standards for trust and key management. Between 2011 and 2014, David worked as Postdoctoral Researcher within the Theoretical Computer Science group at VU University Amsterdam on and NWO funded project entitled "Design and Analysis of Secure Distributed Protocols (DASDiP)".

Dr David M. Williams' PhD focused on the Formal Modelling and Analysis of Buyer-Seller Watermarking protocols. The success of his approach was evident from the number of flaws identified in published protocols proposed for copyright protection of digital content.

Dr David M. Williams is an (ISC)^2 Certified Information Systems Information Systems Security Professional.

Research interests

His research interests include protocol verification, process algebra, formal methods, distributed systems, concurrency, cyber security, trusted execution environments and federated identity management.


  • COM3017/COMM037 - Information Security Management (2016/17)

My publications


Hoang TS, Schneider SA, Treharne H, Williams DM (2016) Foundations for using Linear Temporal Logic in Event-B refinement, Formal Aspects of Computing 28 (6) pp. 909-935 Springer London
In this paper we present a new way of reconciling Event-B refinement with linear temporal logic
(LTL) properties. In particular, the results presented in this paper allow properties to be established for
abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to
hold as those models are developed through refinement. There are several novel elements to this achievement:
(1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide
translations of LTL predicates to reflect the introduction through refinement of new events and the renaming
and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B,
including state predicates and enabledness of events, which can be model-checked at the abstract level. Our
results are more general than any previous work in this area, covering liveness in the context of anticipated
events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case
study. This enables designers to develop event based models and to consider their execution patterns so that
liveness and fairness properties can be verified for Event-B systems.
Lockefeer L, Williams DM, Fokkink W (2016) Formal specification and verification of TCP extended with the Window Scale Option, Science of Computer Programming 118 pp. 3-23 Elsevier
We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With the aid of our ¼CRL specification and the LTSmin toolset, we verify that our specification of unidirectional TCP Data Transfer extended with the Window Scale Option does not deadlock, and that its external behaviour is branching bisimilar to a FIFO queue for a significantly large instance. Separately, we verify that a connection may only be closed if both entities accept the CLOSE call from the Application Layer. Finally, we recommend a rewording of the specification regarding how a zero window is probed, ensuring deadlocks do not arise as a result of misinterpretation.