- 期刊
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. Moreover, the effectiveness and the timeliness of the protocol are also established. Hence, the key security properties of ASW protocol have been verified.
被引用紀錄
延伸閱讀
- 廖海崴（2007）。Application and Design of an Algorithm for Probabilistic Artificial Immune of Classification〔碩士論文，元智大學〕。華藝線上圖書館。https://www.airitilibrary.com/Article/Detail?DocID=U0009-0207200701184700
- Hsiao, S. W. (2012). Service Behavior Profiling and Probabilistic Inference for Anomaly Detection [doctoral dissertation, National Taiwan University]. Airiti Library. https://doi.org/10.6342/NTU.2012.02744
- Wong, T. Y., Lui, J. C. S., & Wong, M. H. (2007). Markov Chain Modelling of the Probabilistic Packet Marking Algorithm. International Journal of Network Security, 5(1), 32-40. https://doi.org/10.6633/IJNS.200707.5(1).04
- Lin, H. Y. (2017). A Precise Program Phase Identification Method Based on Frequency Domain Analysis [master's thesis, National Tsing Hua University]. Airiti Library. https://www.airitilibrary.com/Article/Detail?DocID=U0016-0401201816042169
- Yu, Z. S. (2013). A Scalable Approach to Correctness Analysis and Optimization for Probabilistic Boolean Circuits [master's thesis, National Tsing Hua University]. Airiti Library. https://www.airitilibrary.com/Article/Detail?DocID=U0016-2511201311364476