Abstract: Many facts indicate most criminalities correlated computer are executed by insiders in an organization, fraudulence is one of the main menaces. The fraudulent activities are difficultly detected due to viciously executed by insiders. The fraudulent activities performed by insiders often take place in workflow systems. Separation of duties is an efficient mechanism to prevent fraud within organizations. Isolating the task and executive object physically and logically is a effective way to eliminate the fraudulent behavior. Discussed in this paper is the problem of security policy on the executions of workflows. Workflows are intuitively specified with Petri nets. Petri net is a formal description tool, especially adapt to describe discrete event dynamic system. Furthermore, Petri net, a graphical description tool, can describe dynamic actions in a system by the way of token moving. Specially, the tasks in workflow systems and the relationship between the tasks and the roles are distinctly specified with Petri nets. The security rules are formally represented in Prolog. Based on the formal specification, the security rules are analyzed using logical reasoning to find all valid execution chains of a workflow. Through analysis, all valid execution chains are found, which satisfy the security rules.