Nominal models and resource usage control

Two classes of nominal automata, namely Usage Automata (UAs) and
Variable Finite Automata (VFAs) are considered to express resource con-
trol policies over program execution traces expressed by a nominal calcu-
lus (Usages). We ?rst analyse closure properties of UAs, and then show
UAs less expressive than VFAs. We ?nally carry over VFAs the symbolic
technique for model checking Usages against UAs, so making it possi-
ble to verify the compliance of a program with a larger class of security
properties.