Verification of Timed Opacity Applied to An English Online Auction System
Internet plays an important role in today business activities such as electronic commerce. One challenge concern is the verification of security problem. More specifically, it’s to verify that secret information remain hidden from any possible intruder (Opacity property). The English online auction system is one of systems that uses the E-commerce in the business process. Therefore, the system requires securing some information. Moreover, the time is a critical parameter in the auction system where the buyer and the auctioneer exchange information. The parameter will increase the difficulty of the verification of the opacity properties. In this paper, we model the system using the timed automaton and we verify the timed opacity properties based on the Space Ex tool.
Keywords - Timed Automata, Timed Opacity, English Online Auction System, Space Ex.