Design and Validation of Extended CSP Model

Abstract:

CSP method is very effective for analyzing security protocol, find security attack. But because of the limitation of limited resources, only limited instance verification can be completed. To make up for the inadequacy of CSP protocol model, the CSP mode lis extended to solve the problem of limited detecting in this paper. And then it is proved that the correctness of the extended model based on the related definitions and propositions by using the method of theoretical proof, from several aspects, such as data type of the model, process of trusted agent, process of intruder, process of manager.

• Periodical: Applied Mechanics and Materials (Volumes 635-637)
• Pages: 1544-1550
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.635-637.1544
• Online since: September 2014
• Authors: Jing An*, Lei Zhang, Chun Lan You
• Keywords: Limited Detection, Protocol Verification

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] A. Aldini,M. Bernardo and F. Corradini: A Process Algebraic Approach to Software Architecure Design. Springer(2010).

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

[4] 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).

[5] R. Milner: The Space and Motion of Communicating Agents. Cambridge University Press (2009).