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 its 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 244C251, 1992.

2.       T. Okamoto. An Electronic Voting Scheme. In Proceedings of IFIP World Conference on IT Tools, pages 21C30, 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 245C258, 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 435C487, 2009.