The paper presents the use of states of explosionproof method for analyzing the behavior of systems that provide smart contract technology. The selected example system is ShadowEth, whose main task is to ensure sufficient confidentiality of information stored in the Ethereum blockchain currency. The Petri network model for the ShadowEth system has been presented. The system properties according to the specifications have been defined. Properties described in a certain extension of the TCTL logic and verification have been carried out.
[1] Boucheneb, H., Gardey, G., & Roux, O. H. (2009). TCTL model checking of time Petri nets. Journal of Logic and Computation, 19(6), 1509-1540. Christidis, K., & Devetsikiotis, M. (2016). Blockchains and smart contracts for the internet of things. Ieee Access, 4, 2292-2303.
https://doi.org/10.1093/logcom/exp036
[2] Luu, L., Chu, D. H., Olickel, H., Saxena, P., & Hobor, A. (2016, October). Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security (pp. 254-269). ACM.
https://doi.org/10.1145/2976749.2978309
[3] Kosba, A., Miller, A., Shi, E., Wen, Z., & Papamanthou, C. (2016, May). Hawk: The blockchain model of cryptography and privacy-preserving smart contracts. In 2016 IEEE symposium on security and privacy (SP) (pp. 839-858). IEEE.
https://doi.org/10.1109/SP.2016.55
[4] Atzei, N., Bartoletti, M., & Cimoli, T. (2017, April). A survey of attacks on ethereum smart contracts (sok). In International Conference on Principles of Security and Trust (pp. 164-186). Springer, Berlin, Heidelberg.
https://doi.org/10.1007/978-3-662-54455-6_8
[5] Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., ... & Zanella-Béguelin, S. (2016, October). Formal verification of smart contracts: Short paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (pp. 91-96). ACM.
https://doi.org/10.1145/2993600.2993611
[6] Cong, L. W., & He, Z. (2019). Blockchain disruption and smart contracts. The Review of Financial Studies, 32(5), 1754-1797.
https://doi.org/10.1093/rfs/hhz007
[7] Cuccuru, P. (2017). Beyond bitcoin: an early overview on smart contracts. International Journal of Law and Information Technology, 25(3), 179-195.
https://doi.org/10.1093/ijlit/eax003
[8] Zhang, F., Cecchetti, E., Croman, K., Juels, A., & Shi, E. (2016, October). Town crier: An authenticated data feed for smart contracts. In Proceedings of the 2016 aCM sIGSAC conference on computer and communications security (pp. 270-282). ACM.
https://doi.org/10.1145/2976749.2978326
[9] Szabo, N. (1994). Smart contracts, 1994. Virtual School.
[10] Yuan, R., Xia, Y. B., Chen, H. B., Zang, B. Y., & Xie, J. (2018). Shadoweth: Private smart contract on public blockchain. Journal of Computer Science and Technology, 33(3), 542-556.
https://doi.org/10.1007/s11390-018-1839-y
[11] Akshay, S., Genest, B., & Hélouët, L. (2014). Timed Petri Nets with (restricted) Urgency.
[12] Behrmann, G., Bouyer, P., Larsen, K. G., & Pelánek, R. (2006). Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer, 8(3), 204-215.
https://doi.org/10.1007/s10009-005-0190-0
[13] David, A., Jacobsen, L., Jacobsen, M., & Srba, J. (2012). A forward reachability algorithm for bounded timed-arc Petri nets. arXiv preprint arXiv:1211.6194.
https://doi.org/10.4204/EPTCS.102.12
[14] Li X., Jiang P., Chen T., Luo X., Wen Q., A survey on the security of blockchain systems, Future Generation Computer Systems, 2017, p. 2.
https://doi.org/10.1016/j.future.2017.08.020
[15] Conti M., Kumar E. S., Lal C., Ruj S., A survey on security and privacy issues of bitcoin, IEEE Communications Surveys & Tutorials, 20(4), 2018, pp. 3416-3452.
https://doi.org/10.1109/COMST.2018.2842460