next up previous
Next: The IETF Protocols Up: D6.1 - List of Previous: Coverage and Relevance Assessment


Properties (Goals)

The usual properties referred to as security properties (or security goals) in IETF documents are the following (see [160,,201,3], and also [87,118]).

  1. Authentication (unicast): Verifying an identity (distinguishing identifier) claimed by or for a system entity, which may be a peer in a communication or the source of some data. This assured Identity may be well known (a real name, telephone number, mailing address, phone number, social security number, IP- or email address) or it can be an unlinkable identifier (like a pseudonym). The verification is achieved presenting authentication information (credentials) that corroborates the binding between the entity and the identifier. Authentication is usually divided into entity and message (or data) authentication. The main difference between the two is that message authentication provides no timeliness guarantee (the authenticated message may be old), while entity authentication implies actual communication with an associated verifier during execution of the current run of the protocol. Authentication is usually unilateral (``Alice authenticates Bob''). Mutual Authentication refers to Authentication in both directions.
    1. (G1) Entity authentication (Peer Entity Authentication):

      Assuring one party, through presentation of evidence and/or credentials of the identity of a second party involved in a protocol, and that the second has actually participated during execution of the current run of the protocol. Usually this is done by presenting a piece of data that could only have been generated by the second party in question (as a response to a challenge, for instance). Thus, usually entity authentication implies that some data can be unequivocally traced back to a certain entity, which implies Data Origin Authentication.

    2. (G2) Message authentication (Data Origin Authentication): The protocol must provide means to ensure confidence that a received message or piece of data has been created by a certain party at some (typically unspecified) time in the past, and that this data has not been corrupted or tampered with, but without giving uniqueness or timeliness guarantees. The confidence that data has been created by a certain party, but without the assurance that it has not been modified, is of no interest for us. Thus Message authentication implies integrity. See also [174] ``Relationship between data integrity service and authentication services''. Only very few Internet protocols offer Data Origin Authentication without providing Entity Authentication (IPsec AH or PKI Signatures would be examples, both relatively trivial to verify). In our list of candidate protocols for AVISPA we have no protocol in this category.
    3. (G3) Replay Protection: Some IETF documents define Replay Protection as ``The protocol must provide means to ensure confidence that a received message has not been recorded and played back by an adversary''. As such, this property is not verifiable. We define it rather as: Assuring one party that an authenticated message is not old. Depending on the context, this could have different meanings:
      • that the message was generated during this session, or
      • that the message was generated during a known recent time window, or
      • that the message has not been accepted before.

  2. Authentication in Multicast or via a Subscribe / Notify Service: These are the authentication requirements for groups with a single source and a very large number of potential recipients (multicast), or a source and a service which posts the information to subscribed (and authorized) users. The basic requirements for the solution are:
    1. (G4) Implicit Destination Authentication The protocol must provide means to ensure that a sent message is only readable by entities that the sender allows. That is, only legitimate authorized members will have access to the current information, multicast message or group communication. This includes groups with highly dynamic membership.
    2. (G5) Source Authentication Legitimate group members will be able to authenticate the source and contents of the information or group communication. This includes cases where group members do not trust each other.

  3. (G6) Authorization (by a Trusted Third Party): In some protocols, a Trusted Third Party T3P introduces one principal B to another principal A and A is assured that B is ``trusted'' by the T3P and is ``authorized'', in the required sense of the protocol. When the protocol is run between A, B and T3P, then A is perhaps not able to use local access control lists or other mechanisms to authorize B, (because the name of B is unknown to A, or may even be a pseudonym), but A is assured that B is authorized by T3P.

  4. Key Agreement Properties:
    1. (G7) Key authentication is the property whereby one party is assured that no other party aside from a specifically identified second party (and possibly additional identified trusted parties) may gain access to a particular secret key.
    2. (G8) Key confirmation (Key Proof of Possession): one party is assured that a second (possibly unidentified) party actually has possession of a particular secret key (or of all keying material needed to calculate it).
    3. (G9) Perfect Forward Secrecy (PFS): A protocol has this property if compromise of long-term keys does not compromise past session keys.
    4. (G10) Fresh Key Derivation The protocol uses dynamic key management in order to derive fresh session keys.
    5. (G11) Secure capabilities negotiation (Resistance against Downgrading and Negotiation Attacks). When a key agreement protocol also discovers the cryptographic capabilities and preferences of the peers and negotiates the security parameters (such as security association identifiers, key strength, and ciphersuites), it is important to ensure that the announced capabilities and negotiated parameters have not been forged by an attacker.

  5. (G12) Confidentiality (Secrecy): The property that a particular data item or information (usually sent or received as part of the content of a ``secured'' message, or else constructed on the basis of exchanged data) is not made available or disclosed to unauthorized individuals, entities, or processes, and remains unknown to the intruder. We choose the convention that the secrecy of a session key generated during a key agreement is not considered here but in Goal ``Key authentication'' above. Also the secrecy of a long-term key used within a protocol is not part considered as a secrecy goal of the protocol.

  6. Anonymity Many protocols do not provide anonymity, since the peer has to know with whom he is speaking in order to determine which cryptographic key to use. But some protocols do hide the Identities:
    1. (G13) Identity Protection against Eavesdroppers: An attacker (eavesdropper) should not be able to link the communication exchanged by one party to the real identity of the party.

    2. (G14) Identity Protection against Peer: The peer in a communication should not be able to link the communication exchanged by one party to the real identity of the party, but rather to an unlinked pseudonym or private identifier.

  7. (G15) (Limited) Denial-of-Service (DoS) Resistance: It is difficult to verify DoS Resistance. One reason is that a protocol may be subject to DoS attacks for many different reasons, the most common being that it consumes too many resources (memory, computational power), before the peer authenticates itself. But there are many other reasons: among others, protocols may be vulnerable to
    1. DoS on memory allocation,
    2. DoS on computational power, and
    3. Bombing Attacks on third parties. (This is inducing one or several hosts to send large amounts of packets to a victim).
    [117] shows how some principles that have already been used to make protocols more resistant to denial of service can be formalized.

  8. (G16) Sender Invariance: A party is assured that the source of the communication has remained the same as the one that started the communication, although the actual identity of the source is not important to the recipient.

  9. Non-repudiation Prevention of a user wrongly denying having performed an action, in particular:
    1. (G17) ``Accountability'': The property of a system (including all of its system resources) that ensures that the actions of a system entity may be traced uniquely to that entity, which can be held responsible for its actions.
    2. (G18) Proof of Origin Undeniable evidence of having sent a message.
    3. (G19) Proof of Delivery Undeniable evidence of having received a message.

  10. (G20) Safety Temporal Property: Using two temporal-logic operators (for linear temporal logic), the ``Always'' and the ``Sometime in the Past'' operators, it is possible to formalize properties of the form: in any reachable state that has a property $p$, there was in the past a state with property $q$. Formulaically: $\Box (p \Rightarrow \overline{\Diamond} q)$. Properties of this kind, which are not directly seen as standard security properties, are: if a user has to pay for a service, then he must have obtained the service, or if a host receives a large amount of packets in streaming mode, then he must have asked for them. Notice also that the security properties discussed above are all expressible in the form of a Safety Temporal Property.

In the last few months, a new set of properties have been discussed in some IETF drafts (in particular, at the Extensible Authentication Protocol (EAP) Working Group, see [37]) and Section 4.13). The properties are:

We are optimistic that we will be able to formalize and verify these properties in AVISPA, but it is still not fully clear how to do it.

Other properties that are sometimes discussed as relevant security properties at the IETF (see in particular [37]) include:

The last two are not really new security properties, they relate directly to the Authentication properties discussed above.

The first seven properties are not model-checking properties, but are verified by other methods, outside of the scope of AVISPA.

next up previous
Next: The IETF Protocols Up: D6.1 - List of Previous: Coverage and Relevance Assessment
AVISPA Project -- Deliverable 6.1 'List of Selected Problems'