A trusted execution environment (TEE) provides security-sensitive applications with an isolated execution environment based on hardware isolation mechanisms to protect sensitive data. The memory isolation mechanism is one of the key mechanisms of TEE, which is used to isolate the secure memory from the non-secure memory and to control the access to the secure memory. If the security of the memory isolation mechanism can not be guaranteed, sensitive data stored in the secure memory may be leaked. To verify the security of the TEE memory isolation mechanism, a refinement-based security verification method of the memory isolation mechanism is propose for ARM TrustZone-based TEE. An abstract model and a concrete model are established, a refinement relation between these two models is defined, and the information flow security of the concrete model is verified on the premise of proving that the refinement relation is held and the abstract model satisfies the information flow security properties. The proposed concrete model consists of key hardware and software of the TEE memory isolation mechanism, including TrustZone address space controller, MMU, and TrustZone monitor, and using the theorem prover Isabelle/HOL, it is verified that the concrete model satisfies the information flow security properties, such as noninterference, nonleakage, and noninfluence.