References:
A: for every path.
E: there exists a path.
\boldsymbol{X}_p: p holds next time.
\boldsymbol{F}_p: p holds sometime in the future.
\boldsymbol{G}_p: p holds globally in the future.
p\boldsymbol{U}q: p holds until q holds.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?