  Smart contracts have recently been adopted by many security protocols.
However, existing studies lack satisfactory theoretical support on how
contracts benefit security protocols. This paper aims to give a systematic
analysis of smart contract (SC)-based security protocols to fulfill the gap of
unclear arguments and statements. We firstly investigate \textit{state of the
art studies} and establish a formalized model of smart contract protocols with
well-defined syntax and assumptions. Then, we apply our formal framework to two
concrete instructions to explore corresponding advantages and desirable
properties. Through our analysis, we abstract three generic properties
(\textit{non-repudiation, non-equivocation, and non-frameability}) and
accordingly identify two patterns. (1) a smart contract can be as an autonomous
subscriber to assist the trusted third party (TTP); (2) a smart contract can
replace traditional TTP. To the best of our knowledge, this is the first study
to provide in-depth discussions of SC-based security protocols from a strictly
theoretical perspective.
