HOME

Verification of Stale-Safe Security Properties:

Unsafe model:
We use the NuSMV model checker to show that the vanilla g-SIS archicture is not stale-safe.
The complete code of the model can be found here.

Here are the results from NuSMV showing that it does not satify weak stale-safety.
The results additionally prove the unenforceablity theorem (that authzCC is not enforceable on the TRM machine) and enforceability theorem (that authzTRM is enforcebale on the TRM machine).
The corresponding counter-examples generated by NuSMV are shown.

Weak Stale-Safety:
We modify this model so as to satisfy the weak stale-safe security proerty.
The complete code of the model can be found here.
Here are the results from NuSMV showing that it does not satify weak stale-safety.
The results prove that the model satisfies weak stale-safety.
However, NuSMV generates counter-example proving that strong stale-safety is not satisfied.

Strong Stale-Safety:
We further modify this model so as to satisfy the strong stale-safe security proerty.
The complete code of the model can be found here.
Here are the results from NuSMV showing that it does not satify weak stale-safety.
Finally, the reults prove that this model satisfies strong stale-safety.