Abstract: With the growing popularity of the Internet, more and more protocols run concurrently. In this paper, time is added to the FR protocol, and timed automata is used to model Franklin/Reiter protocol. Then UPPAAL is used to verify some properties of the prot

Key words: E-commerce protocol, Formal verification, Timed automata, UPPAAL, Multiple runs