XIAO Meihua and JIANG Yun and LIU Qiaowei, “On Formal Analysis of Cryptographic Protocolsand Supporting Tool,” Chinese Journal of Electronics, vol. 19, no. 2, pp. 223-228, 2010,
Citation:
XIAO Meihua and JIANG Yun and LIU Qiaowei, “On Formal Analysis of Cryptographic Protocolsand Supporting Tool,” Chinese Journal of Electronics, vol. 19, no. 2, pp. 223-228, 2010,
XIAO Meihua and JIANG Yun and LIU Qiaowei, “On Formal Analysis of Cryptographic Protocolsand Supporting Tool,” Chinese Journal of Electronics, vol. 19, no. 2, pp. 223-228, 2010,
Citation:
XIAO Meihua and JIANG Yun and LIU Qiaowei, “On Formal Analysis of Cryptographic Protocolsand Supporting Tool,” Chinese Journal of Electronics, vol. 19, no. 2, pp. 223-228, 2010,
Cryptographic protocols are crucial for se- cure communications and networks, distribution systems and electronic commerce. Model checking technique and supporting tool for analyzing cryptographic protocols are discussed. A model checking technique based on logic of algorithm knowledge for cryptographic protocols is pro- posed, which can specify explicitly the intruder model ca- pabilities. The knowledge completeness of intruder abili- ties is proved. An e±cient veri¯cation model generating system is developed based on PDL (Protocols description language) and SPIN/Promela for cryptographic protocols. Some optimization strategies are implemented in the sys- tem to reduce the state explosion complexity, such as par- tial order reduction, syntactic reorder and static analysis. More than ten cryptographic protocols are analyzed and published °aws are rediscovered successfully with the sys- tem. The veri¯cation system can be used as an e±cient and reliable tool for evaluation of the network security.
DownLoad: