How to Work with Honest but Curious Judges? (Preliminary Report)

TL;DR

This paper explores protocols for securely computing majority votes among judges with honest but curious behavior, extending existing methods with new approaches and analyzing their privacy guarantees using model checking.

Contribution

It introduces two extended protocols for secure majority voting among judges, analyzing their privacy properties with a new notion of conditional anonymity.

Findings

Both protocols are verified in the MCMAS model checker.

The first protocol is centralized, requiring a leader judge.

The second protocol modifies the dining cryptographers protocol to reveal only the final verdict.

Abstract

The three-judges protocol, recently advocated by Mclver and Morgan as an example of stepwise refinement of security protocols, studies how to securely compute the majority function to reach a final verdict without revealing each individual judge's decision. We extend their protocol in two different ways for an arbitrary number of 2n+1 judges. The first generalisation is inherently centralised, in the sense that it requires a judge as a leader who collects information from others, computes the majority function, and announces the final result. A different approach can be obtained by slightly modifying the well-known dining cryptographers protocol, however it reveals the number of votes rather than the final verdict. We define a notion of conditional anonymity in order to analyse these two solutions. Both of them have been checked in the model checker MCMAS.