Also backports cdbf51 generator bugfix.
Attempts to verify all the properties defined in the security model, while also being portable and able to run on many platforms.