A Model for Verification of Data Security in Operating Systems. - Gerald J. Popek; David A. Farber (Commun. ACM, 1978)