University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Robustness Modelling and Verification of a Mix Net Protocol

Stathakidis, S, Schneider, SA and Heather, J (2014) Robustness Modelling and Verification of a Mix Net Protocol In: SSR 2014: Security Standardisation Research, 2014-12-16 - 2014-12-17.

revised_SSR_paper_Sept_2014.pdf - ["content_typename_UNSPECIFIED" not defined]
Available under License : See the attached licence file.

Download (694kB) | Preview
PDF (licence)
Available under License : See the attached licence file.

Download (33kB) | Preview


Re-encryption Mix Nets are used to provide anonymity by passing encrypted messages through a collection of servers which each permute and re-encrypt messages. They are used in secure electronic voting protocols because they provide a combination of anonymity and verifiability. The use of several peers also provides for robustness, since a Mix Net can run even in the presence of a minority of dishonest or incorrectly behaving peers. However, in practice the protocols for peers to decide when to exclude a peer are complex distributed algorithms, and it is non-trivial to gain confidence that the Mix Net will be robust and live in the presence of faulty or malicious peers. In this paper we model and analyse the algorithm used by Ximix, a particular Mix Net implementation, using the CSP process algebra and the FDR model checker. We model and analyse the protocol in the presence of a realistic intruder based on Roscoe and Goldsmith’s perfect Spy. We show that in the current implementation the protocol does not satisfy the robustness requirement. Finally, we propose a method of making it robust, and verify in FDR that the proposed solution is sound and provides this robustness. Along the way, we highlight the omissions and deviations from the original RPC proposal; Mix Net protocols are extremely fragile, and small and seemingly benign changes may result in security flaws. Our experimental results show that, with our modification, Ximix guarantees termination and produces a correct output in the presence of an intruder who can corrupt a minority of mix servers.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Date : 16 December 2014
Identification Number : 10.1007/978-3-319-14054-4_9
Additional Information : The original publication is available at
Depositing User : Symplectic Elements
Date Deposited : 21 Nov 2014 15:40
Last Modified : 17 Feb 2015 18:14

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800