Abstract: In characterizing security, the information flow security models capture more essence than the access control security models. Within the unified framework of security process algebra, this paper describes and formally defines six types of information flow security models and analyzes their relationship of logical implication based on trace semantics. Furthermore, both the verification algorithm and the verification tools are developed for the six information flow security models based on security process algebra. Finally, several examples are presented for their utilization.