Computationally Sound Mechanized Proofs for Electronic Payment Protocol in a Probabilistic Polynomial Calculus with CryptoVerif
Bo Meng -, Lin Li, Fei Shao - · International Journal of Digital Content Technology and its Applications · 2011
During the past few decades electronic payment protocols has been studied. A lot of electronic payment protocols have been proposed which claimed that have the security properties, for example, accountability, atomicity, anonymity, non-repudiation and fairness. To our best knowledge, these security properties and electronic payment protocols are analyzed with informal method, or with symbolic method, or with computational model by hand, which depends on experts’ knowledge and skill and is prone to make mistakes. So analysis of security properties and electronic payment protocols with automatic tool in computational model plays an important role in security protocol world and is a significant work .Especially analysis with automatic tool in computational model is a changeling issue. Recently owning to the contribution of Meng et al., SOCPT electronic payment protocol can be analyzed with automatic tool in computational model. In this study firstly the state-ofart of electronic payment protocol and the proof including in symbolic model and in computational model are presented. We found that there does not existing that analysis of electronic payment protocols and its security properties with automatic tool in computational model until Meng et al. propose the first automatic framework of accountability based on Blanchet calculus. Then the term, process and correspondence assertion in Blanchet calculus are used to model the security properties including money accountability and goods accountability and SOCPT electronic payment protocol with Meng et al. mechanized framework of electronic payment protocols in computational model with active adversary. Finally SOCPT electronic payment protocol is analyzed with mechanized tool CryptoVerif. The result shows that SOCPT electronic payment protocol has money accountability and goods accountability, which is consistent with its claim. To our knowledge, we are conducting the first automatic analysis of SOCPT electronic payment protocol in computational model.