Specification of security formal models

Summary
The report defines the specifications of the formalism to be used for formal specification of security properties We will investigate mainly timed automata and TCTL but we will adapt and extend them to serve the needs of the project