Modal Specifications of Trace-Based Security Properties