Automatic authorization analysis

Today many companies use an ERP (Enterprise Resource Planning) system such as the SAP system to run their daily business ranging from financial issues down to the actual control of a production line. These systems are very complex from the view of administration of authorizations and include a high potential for errors. The administrators need support to verify their decisions on changes in the authorization setup of such systems and also assistance to implement planned changes error-free. First-order theorem proving is a reliable and correct method to offer this support to administrators at work. But it needs on the one hand a corresponding formalization of an SAP ERP system instance in first-order logic, and on the other hand, a sound and terminating calculus that can deal with the complexity of such systems. Since first-order logic is well-known to be undecidable in general, current research deals with the challenge of finding suitable and decidable sub-classes of first-order logic which are then usable for the mapping of such systems. This thesis presents a (general) new decidable first-order clause class, named BDI (Bounded Depth Increase), which naturally arose from the requirement to assist administrators at work with real-world authorization structures in the SAP system and the automatic proof of properties in these systems. The new class strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI as it is for many other classes. Instead the shape of cycles in resolution inferences is restricted such that the depth of generated clauses may increase but is still finitely bound. This thesis shows that the Hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Further, it employs this result to the Ordered Resolution calculus which is also proved to terminate on BDI, and thus yielding a more efficient decision procedure which is able to solve real-world SAP authorization instances. The test of conditions of BDI have been implemented into the state-of-the art theorem prover SPASS in order to be able to detect decidability for any given problem automatically. The implementation has been applied to the problems of the TPTP Library in order to detect potential new decidable problems satisfying the BDI class properties and further to find non-terminating problems close to the BDI class having only a few clauses which are responsible for the undecidability of the problem.Viele Unternehmen verwenden heutzutage ERP (Enterprise Resource Planning) Systeme wie das SAP System zur Unterstützung des täglichen Geschäfts angefangen vom Rechnungswesen bis hin zur Steuerung einer Fertigungslinie. Diese Systeme sind hinsichtlich der Verwaltung von Berechtigungen sehr komplex und besitzen deswegen eine hohe Fehleranfälligkeit. Administratoren benötigen deswegen sowohl Unterstützung, um ihre Entscheidungen bei Änderungen im Berechtigungs-Setup zu verifizieren und auch Hilfe, um geplante Änderungen an Berechtigungen fehlerfrei umsetzen zu können. Theorembeweisen in Prädikatenlogik ist eine zuverlässige und korrekte Methode, um Administratoren die notwendige Unterstützung bei der Arbeit zu bieten. Sie benötigt jedoch auf der einen Seite eine entsprechende Formalisierung einer SAP ERP System Instanz in Prädikatenlogik, und auf der anderen Seite einen korrekten und terminierenden Kalkül der mit der Komplexität solcher Systeme umgehen kann. Da Prädikatenlogik bekanntlicherweise im Allgemeinen unentscheidbar ist, beschäftigt sich die aktuelle Forschung mit der Herausforderung, geeignete und entscheidbare Teilklassen der Prädikatenlogik zu finden, die dann für die Abbildung solcher Systeme benutzbar sind. Diese Arbeit stellt eine (allgemeine) neue entscheidbare Klauselklasse in Prädikatenlogik mit dem Namen BDI (Bounded Depth Increase) vor, die auf natürlichem Wege aus der Anforderung zur Unterstützung der Administratoren bei der praxisorientierten Arbeit mit Berechtigungsstrukturen im SAP System und dem automatischen Nachweis von Eigenschaften in solchen Systemen entstand. Die neue Klasse enthält bereits bekannte Klassen wie PVD. Die Stelligkeit von Funktions- und Prädikatssymbolen wie auch die Gestalt der Atome ist in BDI nicht beschränkt, wie es bei vielen anderen Klassen der Fall ist. Stattdessen wird die Gestalt von Zyklen in Resolutionsinferenzen derart beschränkt, dass die Tiefe von generierten Klauseln zwar ansteigen kann, aber letztendlich begrenzt ist. Diese Arbeit zeigt, dass der Hyperresolutions-Kalkül zusammen mit der Eliminierung von Redundanzen auf BDI Klauselmengen terminiert. Zusätzlich wird das Ergebnis übertragen auf den Kalkül der geordneten Resolution, für die ebenfalls die Terminierung auf BDI bewiesen wird und damit eine effizientere Enscheidungsprozedur liefert, die für praxisorientierte SAP Instanzen anwendbar ist. Der Test der Bedingungen für BDI wurde im aktuellen Theorembeweiser SPASS implementiert, um die Entscheidbarkeit für ein beliebiges Problem automatisch feststellen zu können. Die Implementierung wurde auf die aktuelle TPTP-Problem-Bibliothek angewendet, um neue entscheidbare Probleme zu finden, die den Anforderungen der BDI Klasse genügen und weiterhin nicht terminierende "beinahe"-BDI Probleme zu ermitteln, bei denen nur wenige Klauseln verantwortlich für die Unentscheidbarkeit des Problems sind