Probabilistic Analysis and Verification of the ASW Protocol using PRISM

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. M...

• Type: Journal
• Year: 2008
• Where: IJNSEC
• Authors: Salekul Islam, Mohammad Abu Zaid
• Keywords: ASW Protocol, IJNSEC 2008, Key Security Objectives, Security Objectives