2015/11/03 by Efstathios Stathakidis, David Williams, Stathakidis, Efstathios +3
Computer Science · #Cryptography and Data Security #Distributed systems and fault tolerance #Security and Verification in Computing
paper · doi:10.14279/tuj.eceasst.66.896
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
A Mix Net is a cryptographic protocol that tries to unlink 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 during the mixing process: 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. Here we verify that the Mix Net is guaranteed to terminate, outputting a provably valid mix agreed upon by a majority of mix servers, under the assumption that a majority of them act according to the protocol.