Analyzing a security specification. An embodiment can include identifying a downgrader in a computer program under test. Via a processor, testing on the downgrader can be performed in a first level of analysis. Responsive to the downgrader not passing the testing performed in the first level of analysis, a counter example for the downgrader can be automatically synthesized. Further, a test unit can be created for the downgrader using the counter example as an input parameter to the downgrader. The test unit can be executed to perform testing on the downgrader in a second level of analysis. Responsive to the downgrader passing the testing performed in the second level of analysis, a user can be prompted to simplify a model of the downgrader.