The ASW protocol is one of the prominent optimistic fair exchange protocols that is used for contract signing between two participants, the originator and the responder, with the aid of a trusted third party in case of a dispute. In this paper, the key security objectives of ASW protocol-fairness, effectiveness and timeliness-have been verified using a probabilistic model checking tool, PRISM. First, the security objectives of ASW protocol have been defined with probabilistic equations. The roles of the participants (i.e., the originator and the responder) and the trusted third party have been modeled in PRISM code. The security objectives of ASW protocol have been expressed using a temporal logic, PCTL. The PCTL expressions are analogous to the probabilistic equations that we have developed to define the security objectives. Next, the model is analyzed using these PCTL expressions, and different outputs have been observed. The outputs confirm the fairness of the ASW protocol. Moreover, the effectiveness and the timeliness of the protocol are also established. Hence, the key security properties of ASW protocol have been verified.
為了持續優化網站功能與使用者體驗,本網站將Cookies分析技術用於網站營運、分析和個人化服務之目的。
若您繼續瀏覽本網站,即表示您同意本網站使用Cookies。