Formal Modeling and Verifying Privacy Types Properties of Security Protocols

---

This webpage is used to give more details on the SeVe tool, an automatic tool used to specify and verify privacy type security protocols.

The tool can be downloaded from here.

The technical report can be downloaded from here.

The explanation of SeVe language as well as it’s syntax can be download from here.

The operational semantics and LTS model semantic of system, as well as formal definition of three types of privacy properties are described here.

All specifications of the case studies are available here. We use our tool to automatically specify and verify three electronic voting protocols in literature:

· Protocol of Fujioka et al. [1]

· Protocol of Okamoto et al. [2]

· Protocol of Lee et al. [3]

This page is maintained by Luu Anh Tuan. Please contact us if you have any question about this webpage or these experiments. We will reply your enquiries as soon as possible.

---

Experiment results

As stated in the paper, the motivation of this tool is to create an automatic tool for specifying and verifying security protocols related with privacy type properties.

These protocols were demonstrated in [4]. However in that paper, the reasoning task is mainly carried out by hand. We prove that we can verify these protocols in an automatic way: the user only needs to specify the protocol in SeVe language; the reasoning will automatically run and return the verification result. This make the proving process is more reliable and avoiding errors. Moreover, by using automatic ways, we can verify larger system, which is crucial in practical use.

Protocol	Property	#States	#Transition	Time(s)	Result
Fujioka et al.	Simple privacy	356	360	0.117s	true
	Receipt freeness	138	141	0.053s	false
	Coercion resistance	97	104	0.040s	false
Okamoto et al.	Simple privacy	484	492	0.133s	true
	Receipt freeness	606	611	0.158s	true
	Coercion resistance	131	136	0.068s	false
Lee et al.	Simple privacy	1744	1810	0.715s	true
	Receipt freeness	2107	2265	0.849s	true
	Coercion resistance	2594	2673	0.930s	true

---

References

1. T. O. Atsushi Fujioka and K. Ohta. A Practical Secret Voting Scheme for Large Scale Elections. In Advances in Cryptology AUSCRYPT 92, volume 718, pages 244–251, 1992.

2. T. Okamoto. An Electronic Voting Scheme. In Proceedings of IFIP World Conference on IT Tools, pages 21–30, 1996.

3. B. Lee, C. Boyd, E. Dawson, K. Kim, J. Yang, and S. Yoo. Providing Receipt-Freeness in Mixnet-based Voting Protocols. In Information Security and Cryptology (ICISC03), volume 2971, pages 245–258, 2004.

4. S. Delaune, S. Kremer, and M. Ryan. Verifying privacy-type properties of electronic voting protocols. In Journal of Computer Security, volume 17, pages 435–487, 2009.