Constructing and verifying a robust Mix Net using CSP

Efstathios Stathakidis, David Williams, James Heather

Research output: Contribution to journalArticlepeer-review


A Mix Net is a cryptographic protocol that unlinks the correspondence between its inputs and its outputs. In this paper, we formally analyse a Mix Net using the process algebra CSP and its associated model checker FDR. The protocol that we verify removes the reliance on a Web Bulletin Board: rather than communicating via a Web Bulletin Board, the protocol allows the mix servers to communicate directly, exchanging signed messages and maintaining their own records of the messages they have received. Mix Net analyses in the literature are invariably focused on safety properties; important liveness properties, such as deadlock freedom, are wholly neglected. This is an unhappy omission, however, since a Mix Net that produces no results is of little use. In contrast, we verify here that the Mix Net is guaranteed to terminate, with each honest mix server outputting the decrypted vector of plaintexts alongside a chain proving that each re-encryption/permutation and partial decryption operation was performed correctly, under the assumption that there is an honest majority of them acting according to the protocol.
Original languageEnglish
Pages (from-to)1063-1089
Number of pages27
JournalSoftware and Systems Modeling
Issue number4
Early online date17 Jun 2015
Publication statusPublished - Oct 2016
Externally publishedYes


  • Mix Nets
  • Formal Methods
  • Model checking
  • CSP
  • FDR


Dive into the research topics of 'Constructing and verifying a robust Mix Net using CSP'. Together they form a unique fingerprint.

Cite this