Formal Analysis of SET Registration Protocol Based on Strand Space

In this paper, we focus on formal analysis of SET Registration protocol and in order to prove it satisfies two security properties, that is, authentication and secrecy, reasonable method Strand Space is used. First, we describe SET Registration protocol in strand space formula and construct their bundles in graph mode. Second, we formalize the goals to be proved. Third, we use minimal element to prove the protocols meet the above secure requirements. It shows that Strand space approach can be used formal analysis on complicated e-commerce protocol visually.