Today many companies use an ERP (Enterprise Resource Planning) system such as
SAP R/3 to run their daily business ranging from financial issues down to the
actual control of a production line. Already due to their sheer size, these
systems are very complex. In particular, developing and maintaining the
authorization setup is a challenge. The goal of our effort is to automatically
analyze the authorization setup of an SAP R/3 system against business policies.
To this end we formalize the processes, authorization setup as well as the
business policies in first-order logic. Then, properties can be (dis)proven
fully automatically with our theorem prover Spass. We exemplify our approach
on the purchase process, a typical constituent of any SAP R/3 installation.