[ Last changed: 27th January 1997 ]
The purpose of this talk is to give a formal definition of the term "Confidentiality Property". On the way, formal definitions will be given of related terms such as "Functionality property", "Cheapness property" and "Prestige property" (the last two being pedagogic toys).
The definitions of those terms is given in terms of a "refinement relation". Refinement relations are of interest as they capture the proof obligations for showing program correctness; and so our definitions are directly related to correctness concerns. The space of refinement relations is modelled as a set of pre-orders (quasi-orders).