Enforcement of security and privacy policy specifications in first order temporal logic

In distributed systems, attribute staleness is inevitable which leads to stale authorization decisions. While it may not be possible to eliminate staleness, this thesis shows that it is possible to limit what type of authorization decisions are made when using stale attributes. Two stale-safety properties, one strictly stronger than the other, are introduced in the context of g-SIS (Group-Centric Secure Information Sharing): Weak Stale-Safety property and Strong Stale-Safety property. Three versions of g-SIS are modeled: a stale-unsafe version, a weakly stale-safe version, and a strongly stale-safe version. Model checking is used to formally verify which stale-safety property/properties, if any, each g-SIS model exhibits. A small model theorem is discussed to extend the results of model checking to first order temporal logic. Finally general stale-safety is discussed along with a notion of minimal stale-safety and shown to be broadly applicable to domains other than g-SIS.