Chaum's dining cryptographers and Fujioka-Okamota-Ohta electronic voting scheme

Organisation:	CWI (THE NETHERLANDS) UiL OTS, Utrecht University (THE NETHERLANDS) Eindhoven University of Technology (THE NETHERLANDS)
Method:	Dynamic epistemic logic Kripke structures Propositional dynamic logic μ-calculus
Tools used:	CADP (Construction and Analysis of Distributed Processes) μCRL toolset LYS
Domain:	Cryptography.
Period:	2007
Size:	n/a
Description:	Anonymity is essential for communication protocols involving sensitive personal information, such as electronic voting, web browsing, forum posting, file sharing or auctions. Contrary to secrecy and authentication, anonymity is not a trace-based property; thus, applying automata-based model checking is not straightforward. Another approach, epistemic logic (or logics of knowledge) is well-suited to represent anonymity properties, but logic-based treatments are complex and modeling of protocols is tedious. In order to tackle these issues, the authors propose to use dynamic epistemic logic: The semantics of this logic is given by Kripke structures, which enables, with a suitable encoding through the ".aut" file format, to use finite-state model checking as provided by the CADP toolbox. This logic introduces action models to describe information updates (public announcement, passing messages, sharing secrets, telling lies...) whose strong operational flavor eases the modeling of protocol steps. The authors developed a tool called LYS, which, starting from an initial epistemic model, computes each step of the analyzed protocol as the product of the epistemic model and an action model. The required anonymity properties, expressed as PDL (Propositional Dynamic Logic) formulas, can then be verified by model checking on the resulting final epistemic model. The approach has been applied to two protocols with a strong anonymity requirement. The first one is Chaum's dining cryptographers protocol: someone paid for the diner of the cryptographers, so they would like to know if it was one of them; however, if it was one of them, they do not want to know which one. The proposed protocol is modeled for 3, 4, and 5 cryptographers. Using the EVALUATOR tool of CADP, it is then shown that when one cryptographer pays, the other ones cannot deduce who he was. It is even verified that the payer himself knows he is anonymous, and that everyone can know that the payer knows he is anonymous. The second one is the Fujioka-Okamota-Ohta electronic voting scheme: it is a complex protocol involving an administrator, a collector, external parties, symmetric keys, a nonce, and a special property of the digital signing scheme. It could be shown with LYS and EVALUATOR that if the phases of the protocol are not correctly ordered then the collector can deduce the vote of some voters.
Conclusions:	This work shows how verification of the challenging anonymity property can be done in the traditional and successful automated setting of model checking with CADP. The author's tool, LYS, relies on CADP considered as "state-of-the-art tool support for automata-based verification." This work also shows that the μ-calculus, the input language of the EVALUATOR tool, is expressive enough to represent PDL formulas of anonymity properties in the context of dynamic epistemic logic.
Publications:	[Eijck-Orzan-07] Jan van Eijck and Simona Orzan. "Epistemic Verification of Anonymity". In Proceedings of the 2nd International Workshop on Views on Designing Complex Architectures VODCA'06 (Bertinoro, Italy), ENTCS vol. 168, pp. 159-174, Elsevier, February 2007 Available on-line from http://www.win.tue.nl/~sorzan/papers/lys.pdf or from the CADP Web site in PDF or PostScript
Contact:	Jan van Eijck CWI, P.O. Box 94079 1090 GB Amsterdam Tel: + 31 20 592 4052 E-mail: jve@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page