In the first part of the thesis we present a generic framework called Logos that may serve as a formal basis for investigations of authorisation issues in applications of groupware systems. Logos has been formalised within HOL - a well-known higher-order logic which is supported by a number of wide-spread theorem provers as e.g. Isabelle/HOL.In the second part we present two applications of Logos. First we show, how it can be used to formalise the key authorisation concept of Lotus Notes - the groupware system currently dominating the market of commercial groupware solutions. Second we develop a case study (namely discussion bboards shared by a number of independent teams) demonstrating the usage of Logos as specification and verification environment for concrete safety critical applications.     «

In the first part of the thesis we present a generic framework called Logos that may serve as a formal basis for investigations of authorisation issues in applications of groupware systems. Logos has been formalised within HOL - a well-known higher-order logic which is supported by a number of wide-spread theorem provers as e.g. Isabelle/HOL.In the second part we present two applications of Logos. First we show, how it can be used to formalise the key authorisation concept of Lotus Notes - the g...     »

Im ersten Teil der Arbeit stellen wir einen generischen Rahmen namens " Logos" vor, der als formale Grundlage zur Untersuchung von Autorisierungsfragen in Groupwareanwendungen dienen kann. Logos wurde in HOL formalisiert - einer weit verbreiteten Logik höherer Ordnung, die von einer Reihe von bekannten Theorembeweisern (wie z.B. Isabelle/HOL) unterstützt wird.Im zweiten Teil der Arbeit präsentieren wir zwei Anwendungen von Logos. Zunächst zeigen wir, wie Logos verwendet werden kann, um das Kernautorisierungskonzept von Lotus Notes (dem Marktführer bei kommerziellen Groupwarelösungen) zu formalisieren. In einem weiteren Schritt entwickeln wir eine Fallstudie (nämlich Diskussionsforen, die von einer Reihe von unabhängigen Teams geteilt wird) und zeigen den Nutzen von Logos als Spezifikations- und Verifikationsumgebung für konkrete, sicherheitskritische Anwendungen.     «

Im ersten Teil der Arbeit stellen wir einen generischen Rahmen namens " Logos" vor, der als formale Grundlage zur Untersuchung von Autorisierungsfragen in Groupwareanwendungen dienen kann. Logos wurde in HOL formalisiert - einer weit verbreiteten Logik höherer Ordnung, die von einer Reihe von bekannten Theorembeweisern (wie z.B. Isabelle/HOL) unterstützt wird.Im zweiten Teil der Arbeit präsentieren wir zwei Anwendungen von Logos. Zunächst zeigen wir, wie Logos verwendet werden kann, um das Kern...     »