Cited By
View all- Xiao MZhong YLi ZChen F(2024)Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of EventsApplied Sciences10.3390/app1405180414:5(1804)Online publication date: 22-Feb-2024
Verification of Verifiability of Voting Protocols by Strand Space Analysis
Pages 363 - 368
Abstract
With the widespread adoption of electronic voting, various voting protocols have been proposed. Voting protocols need to satisfy security requirements, including privacy protection and the prevention of illegal voting (e.g., double voting). Our research focuses on the most important property of voting protocols, namely whether all votes are reflected in the voting results accurately. We formalized and verified this for one voting protocol using strand space analysis. We can also consider multiple security requirements depending on the extent to which the voting result is reflected accurately. These properties are discussed.
References
[1]
Abadi, M., and Fournet, C. Mobile values, new names, and secure communication. SIGPLAN Not. 36, 3 (2001), 104--115.
[2]
Abadi, M., and Gordon, A. D. A calculus for cryptographic protocols: The spi calculus. In Fourth ACM Conference on Computer and Communications Security (1997), ACM Press, pp. 36--47.
[3]
Baskar, A., Ramanujam, R., and Suresh, S. P. Knowledge-based modelling of voting protocols. In Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (2007), TARK '07, ACM, pp. 62--71.
[4]
Burrows, M., Abadi, M., and Needham, R. M. A logic of authentication. In Proceedings of the Royal Society of London (1989), vol. A 426, pp. 233--271.
[5]
Datta, A., Derek, A., Mitchell, J. C., and Roy, A. Protocol composition logic (PCL). In Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin (2007), vol. 172 of Electronic Notes in Theoretical Computer Science, pp. 311--358.
[6]
Fabrega, F. J. T., Herzog, J. C., and Guttman, J. D. Strand spaces: Proving security protocols correct. Journal of Computer Security 7 (1999), 191--230.
[7]
Fujioka, A., Okamoto, T., and Ohta, K. A practical secret voting scheme for large scale elections. In Advances in Cryptology - AUSCRYPTO'92 (1993), vol. 718 of Lecture Notes in Computer Science, pp. 244--251.
[8]
Garcia, F. D., Hasuo, I., Pieters, W., and van Rossum, P. Provable anonymity. In FMSE '05: Proceedings of the 2005 ACM workshop on Formal methods in security engineering (2005), ACM, pp. 63--72.
[9]
Gordon, A. D., and Jeffrey, A. Authenticity by typing for security protocols. J. Comput. Secur. 11, 4 (2003), 451--519.
[10]
Hagihara, S., Oguro, H., and Yonezaki, N. Completeness of a deduction system for relational information between ciphertexts based on probabilistic computational semantics. In Theory and Practice of Computation (2012), vol. 5 of Proceedings in Information and Communications Technology, Springer, pp. 116--132.
[11]
Hagihara, S., Oguro, H., and Yonezaki, N. Kripke semantics for epistemic logic of relational information between ciphertexts. Philippine Computing Journal 7, 2 (2012), 23--32.
[12]
Hagihara, S., Sato, N., and Yonezaki, N. Towards a synthesis of security protocols for data transmission. In Proceedings of the 16th Philippine Computing Science Congress (2016).
[13]
Hagiya, M., Takemura, R., Takahashi, K., and Saito, T. Verification of authentication protocols based on the binding relation. In Proceedings of the 2002 Mext-NSF-JSPS international conference on Software security: theories and systems (2003), ISSS'02, Springer-Verlag, pp. 299--316.
[14]
Hagiya, M., Toda, Y., and Fukuda, Y. Implementation and verification of authentication protocols using proof procedures in HOL.In 2nd IMC Enterprise Security Workshop (November 1999), Information Media Center, Science University of Tokyo. http://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/ssr99/protoveri.ps.
[15]
Halpern, J., and O'Neill, K. Anonymity and information hiding in multiagent systems. In Computer Security Foundations Workshop, 2003. Proceedings. 16th IEEE (2003), pp. 75--88.
[16]
Lowe, G. Breaking and fixing the needham-schroeder public-key protocol using fdr. In Tools and Algorithms for Construction and Analysis of Systems (TACAS 1996) (1996), vol. 1055 of Lecture Notes in Computer Science, Springer, pp. 147--166.
[17]
Lowe, G. A hierarchy of authentication specifications. In PCSFW: Proceedings of The 10th Computer Security Foundations Workshop (1997).
[18]
Mano, K., Kawabe, Y., Sakurada, H., and Tsukada, Y. Role interchange for anonymity and privacy of voting. J. Log. and Comput. 20, 6 (2010), 1251--1288.
[19]
Meadows, C. The NRL protocol analyzer: An overview. Journal of Logic Programming 26, 2 (1996), 113--131.
[20]
Meadows, C. Formal framework and evaluation method for denial of service, 1999.
[21]
Negishi, K., and Yonezaki, N. Verification method for possibility of parallel attack on multiple sessions with the same principals in a security protocol. In International Workshop on Formal Methods and Computer Security (2000), pp. 109--120.
[22]
Paulson, L. C. The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 1 (1998), 85--128.
[23]
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., and Roscoe, B. Modelling & Analysis of Security Protocols. Addison-Wesley Professional, 2000.
[24]
S.Berezin, D., and A.Perrig. Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9, 1 (2001), 47--74.
[25]
Sureshkumar, V., and Anitha, R. Analysis of electronic voting protocol using strand space model. In Recent Trends in Computer Networks and Distributed Systems Security (2014), G. Martinez Perez, S. M. Thampi, R. Ko, and L. Shu, Eds., Springer Berlin Heidelberg, pp. 416--427.
[26]
Talbi, M., Morin, B., Viet Triem Tong, V., Bouhoula, A., and Mejri, M. Specification of electronic voting protocol properties using adm logic: Foo case study. In Proceedings of the 10th International Conference on Information and Communications Security (Berlin, Heidelberg, 2008), ICICS'08, Springer-Verlag, pp. 403--418.
[27]
Tomioka, D., Nishizaki, S., and Ikeda, R. A cost estimation calculus for analyzing the resistance to denial-of-service attack. In Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers (2003), pp. 25--44.
Index Terms
- Verification of Verifiability of Voting Protocols by Strand Space Analysis
Recommendations
Verifying privacy-type properties of electronic voting protocols
Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying ...
Split-ballot voting: Everlasting privacy with distributed trust
In this article, we propose a new voting protocol with several desirable security properties. The voting stage of the protocol can be performed by humans without computers; it provides every voter with the means to verify that all the votes were counted ...
Three voting protocols: ThreeBallot, VAV, and twin
EVT'07: Proceedings of the USENIX Workshop on Accurate Electronic Voting TechnologyWe present three new paper-based voting methods with interesting security properties. Our goal is to achieve the same security properties as recently proposed cryptographic voting protocols, but using only paper ballots and no cryptography. From a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 2019
611 pages
ISBN:9781450365734
DOI:10.1145/3316615
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
- University of New Brunswick: University of New Brunswick
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 February 2019
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
ICSCA '19
ICSCA '19: 2019 8th International Conference on Software and Computer Applications
February 19 - 21, 2019
Penang, Malaysia
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 57Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 28 Sep 2024
Other Metrics
Citations
Cited By
View all- Xiao MZhong YLi ZChen F(2024)Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of EventsApplied Sciences10.3390/app1405180414:5(1804)Online publication date: 22-Feb-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in