Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation

Gu Yonggen; Fu Yuxi

Journal of Computer Research and Development > 2006 > 43(5): 953-958.

Gu Yonggen, Fu Yuxi. Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation[J]. Journal of Computer Research and Development, 2006, 43(5): 953-958.

Citation:

Gu Yonggen, Fu Yuxi. Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation[J]. Journal of Computer Research and Development, 2006, 43(5): 953-958.

Citation:

Gu Yonggen, Fu Yuxi. Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation[J]. Journal of Computer Research and Development, 2006, 43(5): 953-958.

PDF (331 KB)

Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation

Gu Yonggen^1,2,
Fu Yuxi²

1(Department of Computer Science and Technology, Huzhou Teachers College, Huzhou 313000) 2(Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200030)

More Information

Published Date: May 14, 2006

Graphical Abstract

Abstract

Abstract

Formal analysis of security protocols is becoming more and more important. It is desiderated to expand the existing methods to study more security properties and to form a unified framework to analyze various security properties. Process calculus is a powerful tool for modeling concurrent systems. The existing process calculi, however, are not very convenient to support data structure. In this paper, a generic model is proposed for the analysis of security protocols based on a process calculus with knowledge derivation. The model facilitates the formal definitions of some well known security properties. Using this model the Needham-Schroeder public-key protocol is analyzed as a case study. Some future directions are pointed out.
- process calculus,
- knowledge derivation,
- security protocol,
- formal analysis

FullText(HTML)

References (0)

[1]	Wang Jian, Zhao Guosheng, Zhao Zhongnan, Li Ke. Formal Modeling and Factor Analysis for Vulnerability Propagation Oriented to SDN[J]. Journal of Computer Research and Development, 2018, 55(10): 2256-2268. DOI: 10.7544/issn1000-1239.2018.20180447
[2]	Wang Yong, Fang Juan, Ren Xingtian, and Lin Li. Formal Verification of TCG Remote Attestation Protocols Based on Process Algebra[J]. Journal of Computer Research and Development, 2013, 50(2): 325-331.
[3]	Xu Shiwei, Zhang Huanguo. Formal Security Analysis on Trusted Platform Module Based on Applied π Calculus[J]. Journal of Computer Research and Development, 2011, 48(8): 1421-1429.
[4]	Han Jin, Cai Shengwen, Wang Chongjun, Lai Haiguang, Xie Junyuan. A New Security Protocol Modeling Approach Based on π/+t Calculus[J]. Journal of Computer Research and Development, 2010, 47(4): 613-620.
[5]	Shi Zhibin and Huang Houkuan. Reductive Data Cube Based on Formal Concept Analysis[J]. Journal of Computer Research and Development, 2009, 46(11): 1956-1962.
[6]	Wang Huanbao, Zhang Yousheng, and Li Yuan. A Diagram of Strand Spaces for Security Protocols[J]. Journal of Computer Research and Development, 2006, 43(12): 2062-2068.
[7]	Peng Hongyan, Li Xiaojian, Xia Chunhe, Deng Jianfeng, Zhou Xiaofa. A Non-Repudiation Protocol for E-Mail and Its Formal Analysis[J]. Journal of Computer Research and Development, 2006, 43(11): 1914-1919.
[8]	Li Xiaojian and Zhao Qinping. A Protocol of Bidirectional Authentication and Authorization for IP Multicast[J]. Journal of Computer Research and Development, 2006, 43(11): 1904-1913.
[9]	Li Botao and Luo Junzhou. Modeling and Analysis of Non-Repudiation Protocols by Using Petri Nets[J]. Journal of Computer Research and Development, 2005, 42(9): 1571-1577.
[10]	Zhuo Jiliang, Li Xianxian, Li Jianxin, and Huai Jinpeng. A New Taxonomy of Attacks on Security Protocols and Their Security Evaluation[J]. Journal of Computer Research and Development, 2005, 42(7): 1100-1107.