Most security properties rely on the fact that the intruder does not know some secret information or is not able to construct the expected message. They can be characterize as safety properties. Informally, safety properties are properties stating ``nothing bad will happen''. Authentication, access control, confidentiality, integrity and non-repudiation are safety properties. Each of these security services require that a particular situation cannot occur.
The only liveness property is the non-denial of service, which current cryptographic protocols do not guarantee. Intuitively, liveness properties are properties stating ``something good will happen''. A denial of service happens if an intruder succeeds to get a protocol stuck or make it fail. Thus when a denial of service arises, the liveness property stating that the protocol will succeed is not satisfied.
In order to provide these security services, protocols implement particular mechanisms. The LOTOS specification of trusted principals apply them while the intruder process tries to defeat them. A way to verify the robustness against intruder's attacks during the execution of the specification is needed. Thus a formal translation of the properties to be achieved by security services is required in order to perform the verification.