BS ISO IEC 29128:2011 pdf – lnformation technology-Security techniques ——Verification of cryptographic protocols.
The atiacker’s initial knowledge: a set of messages.
How roles (and more generally composed processes) are composed.
In typical examples. the roles can run concurrently. Hence a parallel composition operator is used. But other situations might be relevant: there can be some phases’modes as in E-voting Protocols, or contract signing, in which case sequential compositions or even conditional composition might be required.
How roles (and more generally composed processes) can be replicated or dynamically created,
By —replication of l we mean that an unbounded number of copies of may run concurrently. This may, or not, be allowed in the considered scenario and has to be precised. Similar constraints on the number of dishnct identities must be specified.
The hiding or sharing of names.
This part specifies where the data are generated and how they are inherited. For instance, assume that a role depend on a parameter (a key), There is a big difference between generate (replicate ()) and replicate (generate (J)). In the former case, each replicated copy of I holds the same key . In the tatter case, each copy of generates its own key . The name generation construction not only provides with a name scoping. but also acts as a binder: within that scope. the name can be substituted with a new one. This Is necessary In distinguishing Instances that generate locally the names.
Later, for the specification of security properties, we will need to distinguish between honest agents, dishonest agents. agents that can be corrupted and so on. The corruption ability may also be specified ii the scenario. but also right from the beginning in the categories of names and the different role executions, depending on whether they are played by a corrupted agent or not,
5.5 The specIfication of security properties
5.5.1 General
In view of the huge variety of security properties cat all levels of abstractions), it seems not possible at the time being to give a general way of describing security properties. Furthermore, there is currently no way to specify (even smp4e) security properties, independently of the protocol specification language.
Two classes of properties seem mature enough for a formal specification:
Trace properties: they basically express that, in any possible execution, nothing bad can happen. This is the classical case of model checking linear time properties.
Equivalence properties: they state that the attacker cannot get any relevant information on a given data. Such properties are formalised using two experiments, each 01 whIch corresponds to the same roles, but to a different scenario. The attacicer should be unable to distinguish between the two expeflments. Such an indistinguishability properly corresponds to the classical notion of observational equivalence In concurrency theory.
We investigate briefly for trace properties some of the main features and relevant information for the specification.
53.2 Trace propertIes
At any time, the global state of the network can be described using the collection of configurations of each role instance, the current scenario, and the sequence ff1 of all messages that have been sent so far on channels that can be eavesdropped.
An instantaneous property is a predicate on such global states. For instance, ( ); —a specific message is computable from by the attackerl. Such propetlies may be referred to as events.
A temporal property is a combination of instantaneous properties, using temporal modalities. For instance Ø( ): — ( ) never happensll, or -Each time ( ) happens, then there was before an event ()I.
A trace property is defined by a quantified temporal property: -for any names t( )ll. More complex quantifications might be necessary.
Specifying trace properties require then to
1. Specify one or several (parameterized) events;
2. Specify a set of schedules of such events:
3. Specify for which values of the parameters the temporal property must hold.
EXAMPLE Let us specify first inlormaly and then more formally en agreement property. We wish to say that In any instance of the responder role in the Needharn-Shroeder protocol, if the variable of thai instance is set to ai some point, and if both identities that are parameters of that role are honest, then, before that event.