In order to demonstrate and verify Keel security, I suggest we create a series of unit and functional tests that exercise Keel security, one each for component, instance and invokation security. This would then act as a "howto" example to see how to use it as well.