Manfred Kerber

Florian Kammüller, Manfred Kerber

Avionics is one of the fields in which verification methods have been pioneered and brought a new level of reliability to systems used in safety critical environments. Tragedies, like the 2015 insider attack on a German airplane, in which all 150 people on board died, show that safety and security crucially depend not only on the well functioning of systems but also on the way how humans interact with the systems. Policies are a way to describe how humans should behave in their interactions with technical systems, formal reasoning about such policies requires integrating the human factor into the verification process. In this paper, we report on our work on using logical modelling and analysis of infrastructure models and policies with actors to scrutinize security policies in the presence of insiders. We model insider attacks on airplanes in the Isabelle Insider framework. This application motivates the use of an extension of the framework with Kripke structures and the temporal logic CTL to enable reasoning on dynamic system states. Furthermore, we illustrate that Isabelle modelling and invariant reasoning reveal subtle security assumptions. We summarize by providing a methodology for the development of policies that satisfy stated properties.

Marco B. Caminati, Manfred Kerber, Colin Rowat

We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.