What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
There were a lot of publication on extending and or formalizing RBAC/SOD with LTL or other flavors of temporal logics, not sure of other AC models. Google Scholar (or simple google) search with yield a bunch of articles. Most of them might be not sufficiently formal for somebody like yourself, yet might be of some interest. Not sure is LTL the best way. Yet for a hammers everything is a nail, so if temporal logic is your specialty you might be more successful with it than without.. Consider also traditional programming language semantics approaches such as Z and alike, Game Theoretical/Modular/HyperProperties, dedicated logics. Totally depends on your AC.
Check example articles and see what you feel is the way https://www.sciencedirect.com/science/article/pii/S1571066109003107