The Design and Implementation of Data Independence in the CSP Model of Security Protocol

Abstract:

The CSP method has been extremely effective in checking for, and finding, attacks on security protocol. On the other hand, it has been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources, is free of attacks. In order to resolve this problem, the data independence has been developed by Roscoe. This paper first introduce the new process to expand the CSP model on the base of data independence, and present the whole CSP model of Yahalom and its formalization description. At last, the checking is accomplished by writing in script language CSP_M.

• Periodical: Advanced Materials Research (Volumes 915-916)
• Pages: 1386-1392
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.915-916.1386
• Online since: April 2014
• Authors: Jing An*, Lei Zhang, Chun Lan You
• Keywords: CSP, Data Independence, Mapping, Process

References

[1] A. W. Roscoe. Proving security protocols with model checkers by data independence techniques. In 11th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, (1998).

DOI: 10.1109/csfw.1998.683158

[2] R .S. Lazić. A semantic study of data-independence with applications to the mechanical verification of concurrent systems. D. Phil. Thesis, University of Oxford, (1999).

[3] Failures-Divergence Refinement—FDR2 User Manual. Formal Systems（Europe）Ltd〈http: /www. fsel. com/〉(2003).

[4] R .S. Lazić and A. W. Roscoe, Verifying determinism of data- independence systems with labellings, arrays and constants, Submitted for publication, (1998).

[5] C. Zhang, L.Q. Qian, Y.F. Wang, research of automatic selection of test input data based on extended finite state machine, Journal of Computers, 2003, Vol10.

[6] M. Ebner, TTCN3 test case generation form message sequence charts, ISSRE04 Workshop on integrated ws-reliability with Telecommunications and UML Languages (ISSRE04: WITUL) , 2004-1-17.

[7] Y. Xiao, Automatic Generation Method Research and Realization of Test Cases, Modern Electronic Technology, (2008).

[8] X. Yin, etc. a protocol testing system based on TTCN - 3 and its extension research. (2008).

[9] L. Tang, H. Lei, the generation method of test sequence based on time Petri net, the fourth China academic conference of test.

[10] W.H. Hu, Y.S. Wei, TTCN3 test cases generation study based on MSC, computer engineering and debugging, 2008. 1, Vol29.

[11] S.Y. Liu, Formal Engineering of Industrial Software Development, ISBN 3-540-20602-7.

[12] Y.M. Lu, the design and implementation of the mutation testing method based on algebra specification, computer application and software, 2009. 2, Vol. 26.

[13] H.Q. Zhao, J. Zhao, J. Sun, SIP Protocol Software Testing Method Research based on TTCH-3, Computer Engineering and Design, (2009).

[14] J. Zhao, Automatic Testing Method of Modbus Protocol Consistance, Modern Electronic Technology, (2011).