Security patterns aim to be best practices for avoiding security-related design flaws in software. There is a potential demand for model-driven software tools processing security patterns automatically to support designers, developers, and auditors. Automatically generating or detecting security pattern instances in source code requires a formal specification of instructions how to implement secure software, instead of a description form that is designed for humans. We present a formal definition of security patterns more suitable for automated processes of code generation or code verification. We demonstrate that security patterns theoretically lead to formal constraints that range over all Chomsky types and show how formal security patterns of Chomsky type 3 can be reduced to particular expressions under some assumptions. Finally, we formalize abstractions of security patterns and give a mathematical model as a basis for a data structure for security patterns to be processed by software tools.