Roscoe [25] has recently considered the difference between intensional and extensional specifications of cryptographic protocols. Although no formal definition of these terms is given, the general principle is whether specifications take into account the details of how the operates rather than what each protocol principal gains from the protocol. An extensional property is defined by Roscoe as one which is:
...independent of the details of the protocol and would apply to any other protocol designed to achieve the same effect.Thus extensional properties cannot refer to any specific protocol messages. An example of an extensional property would be that user A wishes to communicate with a user B using a shared key.
In contrast, Roscoe defines an intensional property as one:
...whose primary purpose is to assert a property of the way, in terms of communications within the protocol, a particular state is reached.
Thus an example of an intensional property would be that user A has responded to a specific message from user B using a shared key. This intensional property could be used to provide the extensional property mentioned above. However there are other methods that can be used to achieve the extensional property; for example, a trusted server might inform B that user A has the key and wishes to use it to communicate with B .
Roscoe showed with examples that analysis of a protocol from an intensional specification is often more useful in finding protocol flaws than one from an extensional specification. He defines the canonical intensional specification as follows.
Canonical intensional specification is that an entity will believe a protocol run has completed only if a correct series of messages has occured up to and including the last message that entity communicates.The canonical specification is a very strong requirement that fails for many protocols which are believed secure by different measures. It essentially says that if the protocol completes in the view of its participants then the protocol must have run as specified. Notice that this specification says nothing about what the protocol achieves, and in particular is satisfied by the (admittedly very secure) null protocol.