Biblio

We conduct formal verification of the divide and conquer key distribution scheme (DC DHKE)-a contributory group key agreement that uses a quasilinear amount of exponentiations with respect to the number of communicating parties. The verification is conducted using both ProVerif and TLA+ as tools. ProVerif is used to verify the protocol correctness as well as its security against passive attacker; while TLA+ is utilized to verify whether all participants in the protocol retrieve the mutual key simultaneously. We also verify the ING and GDH.3 protocol for comparative purposes. The verification results show that the ING, GDH.3, and DC DHKE protocols satisfy the pre-meditated correctness, security, and liveness properties. However, the GDH.3 protocol does not satisfy the liveness property stating that all participants obtain the mutual key at the same time.

Creating and implementing fault-tolerant distributed algorithms is a challenging task in highly safety-critical industries. Using formal methods supports design and development of complex algorithms. However, formal methods are often perceived as an unjustifiable overhead. This paper presents the experience and insights when using TLA+ and PlusCal to model and develop fault-tolerant and safety-critical modules for TAS Control Platform, a platform for railway control applications up to safety integrity level (SIL) 4. We show how formal methods helped us improve the correctness of the algorithms, improved development efficiency and how part of the gap between model and implementation has been closed by translation to C code. Additionally, we describe how we gained trust in the formal model and tools by following a specific design process called property-driven design, which also implicitly addresses software quality metrics such as code coverage metrics.