  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.
