Security requirements formalized with OCL in a model-driven approach

Security requirements are properties that have to be guaranteed for an application. Such guarantees can be given using verification. But there is a huge gap between security requirements expressed with human language and formal security properties that can be verified. This paper presents the use of OCL to formalize security requirements in a model-driven approach for security-critical applications. SecureMDD is such a model-driven approach. It uses UML to model the application and OCL to specify the security requirements. From the application model and the contained OCL constraints, a formal specification of the application including the security properties is generated automatically. This specification is used to verify application-specific security properties that matches a lot of security requirements much better than application-independent security properties like secrecy, integrity and confidentiality. We demonstrate how to concretize security requirements as well as the use of OCL constraints to specify security requirements, the transformation from OCL constraints into algebraic specifications and the use of those specifications to verify the security requirements using an electronic ticketing system as a case study.