Abstract
Recently, online shopping integrating third-party payment platforms (TPPs) introduces new security challenges due to complex interactions between Application Programming Interfaces (APIs) of Merchants and TPPs. Malicious clients may exploit security vulnerabilities by calling APIs in an arbitrary order or playing various roles. To deal with the security issue in the early stages of system development, this paper presents a formal method for modeling and verification of online shopping business processes with malicious behavior patterns considered based on Petri nets. We propose a formal model called E-commerce Business Process Net to model a normal online shopping business process that represent intended functions, and malicious behavior patterns representing a potential attack that violates the security goals at the requirement analysis phase. Then, we synthesize the normal business process and malicious behavior patterns by an incremental modeling method. According to the synthetic model, we analyze whether an online shopping business process is resistant to the known malicious behavior patterns. As a result, our approach can make the software design provably secured from the malicious attacks at process design time and, thus, reduces the difficulty and cost of modification for imperfect systems at the release phase. We demonstrate our approach through a case study.