During message exchanges of security protocols, critical points are reached where certain security services are assured. The reception of a well-formed message can trigger a principal into a state where he trusts some facts. This behaviour needs to be formalized. We must translate the human idea that the required security service is satisfied into a precise definition of principals state.
In order to determine these critical points in the specification, we introduce some special events. Each time a critical point is reached by a trusted principal, he informs the environment by sending a specific message that gives information about its internal state. The environment of the LOTOS specification is responsible for the reception of these messages. By executing a special event, a principal declares that he is confident in a fact.
If we consider an authentication protocol between two principals. The prover
must be authenticated by the verifier. There are two critical points in this
protocol. The first one is when the prover starts his authentication and the
second one is when the verifier is sure of the prover's identity. Thus we
introduce two special events PROVER_START_AUTHENTICATION and
VERIFIER_AUTHENTICATION_SUCCESSFUL. A common property required is that
``the prover must have started an authentication with the verifier before the
verifier successfully authenticates the prover''. Otherwise, an intruder has been
able to be authenticated with the prover's identity. This property will be
captured by our special events regardless of the particular authentication
mechanisms used. We just state that ``No
VERIFIER_AUTHENTICATION_SUCCESSFUL event must occur before a PROVER_START_AUTHENTICATION''.
This technique can be applied to a wide range of security properties. Some refinements are sometimes needed to define more precisely critical points. A special event can be expressed with parameters that determine the context where the associated critical point occurs. A parameter can be a principal's identity, an authentication token, a particular key or any other relevant data.
This method allows one to abstract away from all the details of security mechanisms. We can only focus on the security services achieved. One of the major difficulties is to gain the assurance that the critical points are well defined and the security properties are translated correctly into properties on special events. So we need to find the right abstraction level between the simplicity of the global view of the security services and the complexity of the underlying protocols. Method to automate the process would be desirable. Some researchs in this direction can be found in [AG97].