- 期刊
Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol
並列摘要
We demonstrate the application of formal methods to the verification of intrusion-tolerant agreement protocols that have a distributed leadership and can tolerate Byzantine faults. As an interesting case study, the Enclaves group-membership protocol has been verified using two techniques: model checking and theorem proving. We use the model checker Murphi to prove the correctness of authentication, and the interactive theorem prover PVS to formally specify and verify Byzantine agreement, termination of agreement, and integrity.
被引用紀錄
Guo, J. W. (2012). 在行動裝置上基於排隊理論之動態入侵防禦機制 [master's thesis, National Chiao Tung University]. Airiti Library. https://doi.org/10.6842/NCTU.2012.00484
延伸閱讀
- Yadlapati, A., & Kakarla, H. K. (2016). Validating Advanced Extensible Interface Protocol Using Randomized Verification Environment. Research Journal of Applied Sciences, Engineering and Technology, 13(1), 42-47. https://doi.org/10.19026/rjaset.13.2888
- Choi, E. H., Nishihara, H., Ando, T., Tang, N. V., Aoki, M., Yoshisaka, K., Mizuno, O., & Ohsaki, H. (2014). Formal Specification Based Automatic Test Generation for Embedded Network Systems. Journal of Applied Mathematics, 2014(), 97-117-908. https://doi.org/10.1155/2014/909762
- Wang, S. Y. (2004). Abstraction of Formal Models in Real-Time System Verification [master's thesis, National Taiwan University]. Airiti Library. https://doi.org/10.6342/NTU.2004.02251
- Lin, C. T., Wang, N. J., Xiao, H., & Eckert, C. (2015). Feature Selection and Extraction for Malware Classification. Journal of Information Science and Engineering, 31(3), 965-992. https://doi.org/10.6688/JISE.2015.31.3.11
- 王建銘（2004）。Formal modeling and verification of a Third Generation Mobile Communication Protocol〔碩士論文，國立臺灣大學〕。華藝線上圖書館。https://doi.org/10.6342/NTU.2004.00096