Research on Formal Analysis Method of Computational Soundness Based on Strand Space
Meng-meng Yao, Zhu Ye, Li Chuan Tang · 2019
In recent years, the formal analysis and computational soundness analysis of security protocols has been a research hotspot. The formal analysis method based on strand space theory has been widely studied and applied because of its intuitive and concise characteristics. Due to the abstraction of the security protocols by the strand space theory model, the computational soundness of security protocols is potentially sacrificed. So, in this paper, based on the strand space theory model and the Canetti-Krawczyk (CK) model, an improved spCK model is proposed, which enables the strand space to analyze authentication properties and computational soundness of the security protocols. This paper proves the validity and correctness of the spCK model by analyzing the improved ECDH(elliptic curves Diffie-Hellman) protocol.