Theory IFC
section ‹Definitions›
text ‹
This section contains all necessary definitions of this development. Section~\ref{sec:pm} contains
the structural definition of our program model which includes the security specification as well
as abstractions of control flow and data. Executions of our program model are defined in
section~\ref{sec:ex}. Additional well-formedness properties are defined in section~\ref{sec:wf}.
Our security property is defined in section~\ref{sec:sec}. Our characterisation of how information
is propagated by executions of our program model is defined in section~\ref{sec:char-cp}, for which
the correctness result can be found in section~\ref{sec:cor-cp}. Section~\ref{sec:char-scp} contains
an additional approximation of this characterisation whose correctness result can be found in
section~\ref{sec:cor-scp}.
›
theory IFC
imports Main
begin
subsection ‹Program Model›
text_raw ‹\label{sec:pm}›
text ‹Our program model contains all necessary components for the remaining development and consists of:›