SeVe: automatic tool for verification of security protocols

doi:10.1007/s11704-012-2903-3

Front Comput Sci

0, Vol.

Issue () : 57-75 https://doi.org/10.1007/s11704-012-2903-3

RESEARCH ARTICLE

SeVe: automatic tool for verification of security protocols

Anh Tuan LUU¹(

), Jun SUN², Yang LIU¹, Jin Song DONG¹, Xiaohong LI³, Thanh Tho QUAN⁴

1. School of Computing, National University of Singapore, Singapore 119077, Singapore; 2. School of Computing, Singapore University of Technology and Design, Singapore 138682, Singapore; 3. Department of Computer Science, Tianjin University, Tianjin 300222, China; 4. Department of Computer Science, HoChiMinhCity University of Technology, HoChiMinh City 162903, Vietnam

Download: PDF(515 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Security protocols play more and more important roles with wide use in many applications nowadays. Currently, there are many tools for specifying and verifying security protocols such as Casper/FDR, ProVerif, or AVISPA. In these tools, the intruder’s ability, which either needs to be specified explicitly or set by default, is not flexible in some circumstances. Moreover, whereas most of the existing tools focus on secrecy and authentication properties, few supports privacy properties like anonymity, receipt freeness, and coercion resistance, which are crucial in many applications such as in electronic voting systems or anonymous online transactions.

In this paper, we introduce a framework for specifying security protocols in the labeled transition system (LTS) semantics model, which embeds the knowledge of the participants and parameterizes the ability of an attacker. Using this model, we give the formal definitions for three types of privacy properties based on trace equivalence and knowledge reasoning. The formal definitions for some other security properties, such as secrecy and authentication, are introduced under this framework, and the verification algorithms are also given. The results of this paper are embodied in the implementation of a SeVe module in a process analysis toolkit (PAT) model checker, which supports specifying, simulating, and verifying security protocols. The experimental results show that a SeVe module is capable of verifying many types of security protocols and complements the state-of-the-art security verifiers in several aspects. Moreover, it also proves the ability in building an automatic verifier for security protocols related to privacy type, which are mostly verified by hand now.

Keywords security protocols model checking process analysis toolkit (PAT) authentication secrecy privacy

Corresponding Author(s): LUU Anh Tuan,Email:tuanluu@comp.nus.edu.sg

Issue Date: 01 February 2012

Cite this article:

Anh Tuan LUU,Jun SUN,Yang LIU, et al. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 0, (): 57-75.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-012-2903-3
https://academic.hep.com.cn/fcs/EN/Y0/V/I/57

1	Burrows M, Abadi M, Needham R. A logic of authentication. ACM Transactions on Computer Systems , 1990, 8(1): 18-36 doi: 10.1145/77648.77649
2	Syverson P F, van Oorschot P C. On unifying some cryptographic protocol logics. In: Proceedings of 1994 IEEE Symposium on Security and Privacy . 1994, 14-28
3	Paulson L C. The inductive approach to verifying cryptographic protocols. Journal of Computer Security , 1998, 6(1-2): 85-128
4	Bella G, Paulson L C. Kerberos version IV: inductive analysis of the secrecy goals. In: Proceedings of 5th European Symposium on Research in Computer Security . 1999, 361-375
5	Mitchell J C, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Murphi. In: Proceedings of 1997 IEEE Symposium on Security and Privacy . 1997, 141-151
6	Lowe G. Casper: a compiler for the analysis of security protocols. Journal of Computer Security , 1998, 6(1-2): 53-84
7	Blanchet B. Automatic verification of correspondences for security protocols. Journal of Computer Security , 2009, 17(4): 363-434
8	Armando A, Basin D A, Boichut Y, Chevalier Y, Compagna L, Cuéllar J, Drielsma P H, Héam P, Kouchnarenko O, Mantovani J, M?dersheim S, von Oheimb D, Rusinowitch M, Santiago J, Turuani M, Viganò L, Vigneron L. The AVISPA tool for the automated validation of Internet security protocols and applications. In: Proceedings of 17th International Conference on Computer Aided Verification . 2005, 281-285 doi: 10.1007/11513988_27
9	Delaune S, Kremer S, Ryan M. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security , 2009, 17(4): 435-487
10	Mauw S, Verschuren J, de Vink E P. A formalization of anonymity and onion routing. In: Proceedings of 9th European Symposium on Research Computer Security . 2004, 109-124
11	Halpern J Y, O’Neil K R. Anonymity and information hiding in multiagent systems. Journal of Computer Security , 2005, 13(3): 483-512
12	Jonker H J, de Vink E P. Formalising receipt-freeness. In: Proceedings of 9th International Conference on Information Security . 2006, 476-488
13	Hoare C A R. Communicating Sequential Processes. Upper Saddle River: Prentice-Hall , 1985
14	Schneider S. Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering , 1998, 24(9): 741-758 doi: 10.1109/32.713329
15	Shahriari H R, Jalili R. Using CSP to model and analyze transmission control protocol vulnerabilities within the broadcast network. In: Proceedings of 2004 International Networking and Communication Conference . 2004, 42-47
16	Schneider S, Delicata R. Verifying security protocols: an application of CSP. In: Proceedings of Symposium on the Occasion of 25 Years of CSP . 2004, 246-263
17	Basin D A, M?dersheim S, Viganò L. An on-the-fly model-checker for security protocol analysis. In: Proceedings of 8th European Symposium on Research in Computer Security . 2003, 253-270
18	Turuani M. The CL-Atse protocol analyser. In: Proceedings of 17th International Conference Term Rewriting and Applications . 2006, 277-286 doi: 10.1007/11805618_21
19	AVISPA project. HLPSL tutorial. http://www.avispa-project.org/ package/tutorial.pdf
20	Abadi M, Fournet C. Mobile values, new names, and secure Communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . 2001, 104-115 doi: 10.1145/360204.360213
21	Schneider S, Sidiropoulos A. CSP and anonymity. In: Proceedings of 4th European Symposium on Research in Computer Security . 1996, 198-218
22	Fournet C, Abadi M. Hiding names: private authentication in the applied Pi calculus. In: Proceedings of 2002 International Symposium on Software Security . 2002, 317-338
23	Kremer S, Ryan M. Analysis of an electronic voting protocol in the applied Pi calculus. In: Proceedings of 14th European Symposium on Programming . 2005, 186-200
24	Backes M, Hritcu C, Maffei M. Automated verification of remote electronic voting protocols in the applied Pi-calculus. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium . 2008, 195-209 doi: 10.1109/CSF.2008.26
25	Dong N, Jonker H L, Pang J. Analysis of a receipt-free auction protocol in the applied Pi calculus. In: Proceedings of 7th International Workshop on Formal Aspects of Security and Trust . 2010, 223-238
26	Pang J, Zhang C. How to work with honest but curious judges? (preliminary report). In: Proceedings of 7th International Workshop on Security Issues in Concurrency . 2009, 31-45
27	Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory , 1983, 29(2): 198-208 doi: 10.1109/TIT.1983.1056650
28	Ryan P, Schneider S. The Modelling and Analysis of Security Protocols: The CSP Approach. New York: Addison-Wesley, 2000
29	Liu Y, Chen W, Liu Y, Sun J. Model checking lineariability via refinement. In: Proceedings of 2nd World Congress on Formal Methods . 2009, 321-337
30	Roscoe A W. Model-checking CSP. In: Roscoe A W, eds. A Classical Mind: Essays in Honour of C. A. R. Hoare. Hertfordshire: Prentice Hall International (UK) Ltd , 1994, 353-378
31	Sun J, Liu Y, Dong J S, Wang H. Specifying and verifying eventbased Fairness enhanced systems. In: Proceedings of 10th International Conference on Formal Engineering Methods and Software Engineering . 2008, 5-24
32	Sun J, Liu Y, Dong J S, Pang J. PAT: towards flexible verification under Fairness. In: Proceedings of 21st International Conference on Computer Aided Verification . 2009, 709-714 doi: 10.1007/978-3-642-02658-4_59
33	Mahony B, Dong J S. Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of 20th International Conference on Software Engineering . 1998, 95-104 doi: 10.1109/ICSE.1998.671106
34	Mahony B, Dong J S. Timed communicating object Z. IEEE Transactions on Software Engineering , 2000, 26(2): 150-177 doi: 10.1109/32.841115
35	Liu S, Offutt A J, Ho-Stuart C, Sun Y, Ohba M. SOFL: a formal engineering methodology for industrial applications. IEEE Transactions on Software Engineering , 1998, 24(1): 24-45 doi: 10.1109/32.663996
36	Dong J S, Liu S. An object semantic model of SOFL. In: Proceedings of 1st International Conference on Integrated Formal Methods . 1999, 189-208
37	Needham R M, Schroeder M D. Using encryption for authentication in large networks of computers. Communications of the ACM , 1978, 21(12): 993-999 doi: 10.1145/359657.359659
38	Fujioka A, Okamoto T, Ohta K. A practical secret voting scheme for large scale elections. In: Proceedings of 1992 Workshop on the Theory and Application of Cryptographic Techniques . 1992, 244-251
39	Zhou J, Gollmann D. A fair non-repudiation protocol. In: Proceedings of 15th IEEE Symposium on Security and Privacy . 1996, 55-61
40	Abadi M, Blanchet B. Computer-assisted verification of a protocol for certified email. In: Proceedings of 10th International Symposium on Static Analysis . 2005, 316-335
41	Okamoto T. An electronic voting scheme. In: Proceedings of IFIP World Conference on IT Tools . 1996, 21-30
42	Lee B, Boyd C, Dawson E, Kim K, Yang J, Yoo S. Providing receiptfreeness in mixnet-based voting protocols. In: Proceedings of 6th International Conference on Information Security and Cryptology . 2003, 245-258
43	Luu A T. Formal modeling and verifying privacy types properties of security protocols. Technical report, National University of Singapore , 2010, http://www.comp.nus.edu.sg/～ pat/fm/security/

[1]	Yupei ZHANG, Yuxin LI, Yifei WANG, Shuangshuang WEI, Yunan XU, Xuequn SHANG. Federated learning-outcome prediction with multi-layer privacy protection[J]. Front. Comput. Sci., 2024, 18(6): 186604-.
[2]	Xingxing CHEN, Qingfeng CHENG, Weidong YANG, Xiangyang LUO. An anonymous authentication and secure data transmission scheme for the Internet of Things based on blockchain[J]. Front. Comput. Sci., 2024, 18(3): 183807-.
[3]	Min HAO, Beihai TAN, Siming WANG, Rong YU, Ryan Wen LIU, Lisu YU. Exploiting blockchain for dependable services in zero-trust vehicular networks[J]. Front. Comput. Sci., 2024, 18(2): 182805-.
[4]	Shiwei LU, Ruihu LI, Wenbin LIU. FedDAA: a robust federated learning framework to protect privacy and defend against adversarial attack[J]. Front. Comput. Sci., 2024, 18(2): 182307-.
[5]	Fengxia LIU, Zhiming ZHENG, Yexuan SHI, Yongxin TONG, Yi ZHANG. A survey on federated learning: a perspective from multi-party computation[J]. Front. Comput. Sci., 2024, 18(1): 181336-.
[6]	Long LI, Jianbo HUANG, Liang CHANG, Jian WENG, Jia CHEN, Jingjing LI. DPPS: A novel dual privacy-preserving scheme for enhancing query privacy in continuous location-based services[J]. Front. Comput. Sci., 2023, 17(5): 175814-.
[7]	Qian CHEN, Zhiwei NI, Xuhui ZHU, Pingfan XIA. Differential privacy histogram publishing method based on dynamic sliding window[J]. Front. Comput. Sci., 2023, 17(4): 174809-.
[8]	Hongyang LI, Xinghua LI, Qingfeng CHENG. A fine-grained privacy protection data aggregation scheme for outsourcing smart grid[J]. Front. Comput. Sci., 2023, 17(3): 173806-.
[9]	Shuang LIU, Fan ZHANG, Baiyang ZHAO, Renjie GUO, Tao CHEN, Meishan ZHANG. APPCorp: a corpus for Android privacy policy document structure analysis[J]. Front. Comput. Sci., 2023, 17(3): 173320-.
[10]	Changbo KE, Fu XIAO, Zhiqiu HUANG, Fangxiong XIAO. A user requirements-oriented privacy policy self-adaption scheme in cloud computing[J]. Front. Comput. Sci., 2023, 17(2): 172203-.
[11]	Peng LI, Junzuo LAI, Yongdong WU. Accountable attribute-based authentication with fine-grained access control and its application to crowdsourcing[J]. Front. Comput. Sci., 2023, 17(1): 171802-.
[12]	Dan ZHAO, Suyun ZHAO, Hong CHEN, Ruixuan LIU, Cuiping LI, Wenjuan LIANG. Efficient protocols for heavy hitter identification with local differential privacy[J]. Front. Comput. Sci., 2022, 16(5): 165825-.
[13]	Kaiyue ZHANG, Xuan SONG, Chenhan ZHANG, Shui YU. Challenges and future directions of secure federated learning: a survey[J]. Front. Comput. Sci., 2022, 16(5): 165817-.
[14]	Elisabetta DE MARIA, Abdorrahim BAHRAMI, Thibaud L’YVONNET, Amy FELTY, Daniel GAFFÉ, Annie RESSOUCHE, Franck GRAMMONT. On the use of formal methods to model and verify neuronal archetypes[J]. Front. Comput. Sci., 2022, 16(3): 163404-.
[15]	Qiao XUE, Youwen ZHU, Jian WANG. Mean estimation over numeric data with personalized local differential privacy[J]. Front. Comput. Sci., 2022, 16(3): 163806-.

Viewed

Full text

Abstract

Cited

Shared

Discussed