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




Bennatt, Jared F.

Journal Title

Journal ISSN

Volume Title



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.


This item is available only to currently enrolled UTSA students, faculty or staff. To download, navigate to Log In in the top right-hand corner of this screen, then select Log in with my UTSA ID.
The join-before-add.zip supplementary zip file contains SMV files for model when join occurs before add (as in paper) including make script. The add-before-join.zip supplementary zip file contains SMV files for model when add occurs before join (alluded to in section about minimal clock size--the minimum size here is 3).


first order logic, formal methods, privacy, security, temporal logic



Computer Science