A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic

XIAO Meihua; MA Chenglin; DENG Chunyan; ZHU Ke

Article Contents

Article Navigation > Chinese Journal of Electronics > 2015 > 24(1): 187-192

XIAO Meihua, MA Chenglin, DENG Chunyan, et al., “A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic,” Chinese Journal of Electronics, vol. 24, no. 1, pp. 187-192, 2015,

Citation:

XIAO Meihua, MA Chenglin, DENG Chunyan, et al., “A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic,” Chinese Journal of Electronics, vol. 24, no. 1, pp. 187-192, 2015,

Citation:

PDF( 459 KB)

A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic

School of Software, East China Jiaotong University, Nanchang 330013, China

Funds: This work was supported by Natural Science Foundation of China (No.61163005), Natural Science Foundation of Jiangxi, China (No.2007GZS1884, No.2010GZS0150, No.20132BAB201033), State Key Laboratory for Novel Software Technology Open Project (No.KFKT2012B18), Science and Technology College in Jiangxi Province Ground Project (No.KJLD13038), and Project of Innovation Funds for Postgraduates in Jiangxi Province (No.YC2013-S173).

Received Date: 2013-12-01
Rev Recd Date: 2014-05-01
Publish Date: 2015-01-10

Abstract

Abstract

Since security protocols form the cornerstones of modern secure networked systems, it is important to develop informative, accurate, and deployable approach for finding errors and proving that protocols meet their security requirements. We propose a novel approach to check security properties of cryptographic protocols using authentication event logic. Compared with logic of algorithm knowledge, authentication event logic guarantees that any well-typed protocol is robustly safe under attack while reasoning only about the actions of honest principals in the protocol. It puts no bound on the size of the principal and requires no state space enumeration and it is decidable. The types for protocol data provide some intuitive explanation of how the protocol works. Our approach has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.
- Security protocols,
- Formal analysis,
- Authentication event logic

FullText(HTML)

References(19)

References

S.F. Allen, M. Bickford, R.L. Constable, et al., "Innovations in computational type theory using Nuprl", Journal of Applied Logic, Vol.4, No.4, pp.428-469, 2006.

M. Bickford and R.L. Constable, "A logic of events", Technical Report TR2003-1893, Cornell University, 2003.

M. Bickford and R.L. Constable, "Automated proof of authentication protocols in a logic of events", Proceedings of the 6th International Verification Workshop, pp.13-30, 2010.

Chien, Hung-Yu, Tzong-Chen Wu and Ming-Kuei Yew, "Provably secure gateway-oriented password-based authenticated key exchange protocol resistant to password guessing attacks", Journal of Information Science & Engineering, Vol.29, No.2, pp.249-265, 2013.

Berg M, "Formal verification of cryptographic security proofs", Ph.D. Thesis, Faculty of Natural Sciences and Technology, Department of Computer Science Saarland University, 2013.

Mark Bickford, "Unguessable atoms: A logical foundation for security", N. Shankar and J. Woodcock (Eds.): VSTTE 2008, Vol.5295, pp.30-53, 2008.

Mark Bickford and Robert Constable, "Formal foundations of computer security", NATO Science for Peace and Security Series, D: Information & communication Security, Vol.14, pp.29- 52, 2008.

Xiao Meihua and Xue Jinyun, "Modeling and verifying cryptographic protocols using SPIN/Promela", International Journal of Computer and Information Science, Vol.6, No.1, pp.1-12, 2005.

XiaoMeihua and Xue Jinyun, "Formal analysis of cryptographic protocols in a knowledge algorithm logic framework", Chinese Journal of Electronics, Vol.16, No.4, pp.701-706, 2007.

Xiao Meihua, Jiang Yun and Liu Qiaowei, "On formal analysis of cryptographic protocols and supporting tool", Chinese Journal of Electronics, Vol.19, No.2, pp.223-228, 2010.

A. Datta, A. Derek, J. Mitchell and A. Roy, "Protocol composition logic (PCL)", Electronic Notes in Theororetical Computer Science, Vol.172, pp311-358, 2007.

C. He, M. Sundararajan, A. Datta, A. Derek and J. Mitchell, "A Modular correctness proof of IEEE 802.11i and TLS", CCS’05: Proceedings of the 12th ACM Conference on Computer and Communications Security, pp.2-15, ACM Press, 2005.

C. Cremers, "On the protocol composition logic PCL". ASIACCS’ 08, pp.66-76, Tokyo, Japan, 2008.

M. Abadi, "Secrecy by typing in security protocols", Journal of the ACM, Vol.46, No.5, pp.749-786, 1999.

A.D. Gordon and A. Jeffrey, "Authenticity by typing for security protocols", Journal of Computer Security, Vol.11, No.4, pp.451-519, 2003.

F.B. Schneider, K. Walsh and E.G. Sirer, "Nexus authorization logic: Design rationale and application", ACM Transactions on Information and System Security, Vol.14, No.1, pp.128-136, 2011.

N. Doshi and D. Jinwala, "Hidden access structure ciphertext policy attribute based encryption with constant length ciphertext", P.S. Thilagam(ed.), Advanced Computing, Networking and Security, LNCS, Vol.7135, Springer, Heidelberg, pp.515- 523, 2012.

N. Attrapadung, B. Libert and E.d. Panafieu, "Expressive key-policy attribute-based encryption with constant-size ciphertexts", D. Catalano (ed.), Public Key Cryptography-PKC 2011, LNCS, Vol.6571, Springer, Heidelberg, pp.90-108, 2011.

J. Lai, R.H. Deng and Y. Li, "Fully secure ciphertext-policy hidding CP-ABE", F. Bao and J. Weng (eds.), Information Security Practice and Experience, LNCS, Vol.6672, Springer, Heidelberg, pp.24-39, 2011.

Relative Articles

Supplements(0)

Cited By

Proportional views