Security protocol notation

Last updated

In cryptography, security (engineering) protocol notation, also known as protocol narrations [1] and Alice & Bob notation, is a way of expressing a protocol of correspondence between entities of a dynamic system, such as a computer network. In the context of a formal model, it allows reasoning about the properties of such a system.

The standard notation consists of a set of principals (traditionally named Alice, Bob, Charlie, and so on) who wish to communicate. They may have access to a server S, shared keys K, timestamps T, and can generate nonces N for authentication purposes.

A simple example might be the following:

This states that Alice intends a message for Bob consisting of a plaintext X encrypted under shared key KA,B.

Another example might be the following:

This states that Bob intends a message for Alice consisting of a nonce NB encrypted using public key of Alice.

A key with two subscripts, KA,B, is a symmetric key shared by the two corresponding individuals. A key with one subscript, KA, is the public key of the corresponding individual. A private key is represented as the inverse of the public key.

The notation specifies only the operation and not its semantics for instance, private key encryption and signature are represented identically.

We can express more complicated protocols in such a fashion. See Kerberos as an example. Some sources refer to this notation as Kerberos Notation. [2] Some authors consider the notation used by Steiner, Neuman, & Schiller [3] as a notable reference. [4]

Several models exist to reason about security protocols in this way, one of which is BAN logic.

Security protocol notation inspired many of the programming languages used in choreographic programming.

Related Research Articles

<span class="mw-page-title-main">Diffie–Hellman key exchange</span> Method of exchanging cryptographic keys

Diffie–Hellman key exchange is a mathematical method of securely exchanging cryptographic keys over a public channel and was one of the first public-key protocols as conceived by Ralph Merkle and named after Whitfield Diffie and Martin Hellman. DH is one of the earliest practical examples of public key exchange implemented within the field of cryptography. Published in 1976 by Diffie and Hellman, this is the earliest publicly known work that proposed the idea of a private key and a corresponding public key.

Kerberos is a computer-network authentication protocol that works on the basis of tickets to allow nodes communicating over a non-secure network to prove their identity to one another in a secure manner. Its designers aimed it primarily at a client–server model, and it provides mutual authentication—both the user and the server verify each other's identity. Kerberos protocol messages are protected against eavesdropping and replay attacks.

In cryptography and computer security, a man-in-the-middle (MITM) attack is a cyberattack where the attacker secretly relays and possibly alters the communications between two parties who believe that they are directly communicating with each other, as the attacker has inserted themselves between the two parties. One example of a MITM attack is active eavesdropping, in which the attacker makes independent connections with the victims and relays messages between them to make them believe they are talking directly to each other over a private connection, when in fact the entire conversation is controlled by the attacker. The attacker must be able to intercept all relevant messages passing between the two victims and inject new ones. This is straightforward in many circumstances; for example, an attacker within the reception range of an unencrypted Wi-Fi access point could insert themselves as a man-in-the-middle. As it aims to circumvent mutual authentication, a MITM attack can succeed only when the attacker impersonates each endpoint sufficiently well to satisfy their expectations. Most cryptographic protocols include some form of endpoint authentication specifically to prevent MITM attacks. For example, TLS can authenticate one or both parties using a mutually trusted certificate authority.

In cryptography, a block cipher mode of operation is an algorithm that uses a block cipher to provide information security such as confidentiality or authenticity. A block cipher by itself is only suitable for the secure cryptographic transformation of one fixed-length group of bits called a block. A mode of operation describes how to repeatedly apply a cipher's single-block operation to securely transform amounts of data larger than a block.

Burrows–Abadi–Needham logic is a set of rules for defining and analyzing information exchange protocols. Specifically, BAN logic helps its users determine whether exchanged information is trustworthy, secured against eavesdropping, or both. BAN logic starts with the assumption that all information exchanges happen on media vulnerable to tampering and public monitoring. This has evolved into the popular security mantra, "Don't trust the network."

In computer security, challenge–response authentication is a family of protocols in which one party presents a question ("challenge") and another party must provide a valid answer ("response") to be authenticated.

<span class="mw-page-title-main">Needham–Schroeder protocol</span> Key transport protocol

The Needham–Schroeder protocol is one of the two key transport protocols intended for use over an insecure network, both proposed by Roger Needham and Michael Schroeder. These are:

The Otway–Rees protocol is a computer network authentication protocol designed for use on insecure networks. It allows individuals communicating over such a network to prove their identity to each other while also preventing eavesdropping or replay attacks and allowing for the detection of modification.

The Wide-Mouth Frog protocol is a computer network authentication protocol designed for use on insecure networks. It allows individuals communicating over a network to prove their identity to each other while also preventing eavesdropping or replay attacks, and provides for detection of modification and the prevention of unauthorized reading. This can be proven using Degano.

A cryptographic protocol is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol describes how the algorithms should be used and includes details about data structures and representations, at which point it can be used to implement multiple, interoperable versions of a program.

A replay attack is a form of network attack in which valid data transmission is maliciously or fraudulently repeated or delayed. This is carried out either by the originator or by an adversary who intercepts the data and re-transmits it, possibly as part of a spoofing attack by IP packet substitution. This is one of the lower-tier versions of a man-in-the-middle attack. Replay attacks are usually passive in nature.

MQV (Menezes–Qu–Vanstone) is an authenticated protocol for key agreement based on the Diffie–Hellman scheme. Like other authenticated Diffie–Hellman schemes, MQV provides protection against an active attacker. The protocol can be modified to work in an arbitrary finite group, and, in particular, elliptic curve groups, where it is known as elliptic curve MQV (ECMQV).

In cryptography, the interlock protocol, as described by Ron Rivest and Adi Shamir, is a protocol designed to frustrate eavesdropper attack against two parties that use an anonymous key exchange protocol to secure their conversation. A further paper proposed using it as an authentication protocol, which was subsequently broken.

Elliptic-curve Diffie–Hellman (ECDH) is a key agreement protocol that allows two parties, each having an elliptic-curve public–private key pair, to establish a shared secret over an insecure channel. This shared secret may be directly used as a key, or to derive another key. The key, or the derived key, can then be used to encrypt subsequent communications using a symmetric-key cipher. It is a variant of the Diffie–Hellman protocol using elliptic-curve cryptography.

The Password Authenticated Key Exchange by Juggling is a password-authenticated key agreement protocol, proposed by Feng Hao and Peter Ryan. This protocol allows two parties to establish private and authenticated communication solely based on their shared (low-entropy) password without requiring a Public Key Infrastructure. It provides mutual authentication to the key exchange, a feature that is lacking in the Diffie–Hellman key exchange protocol.

Yahalom is an authentication and secure key-sharing protocol designed for use on an insecure network such as the Internet. Yahalom uses a trusted arbitrator to distribute a shared key between two people. This protocol can be considered as an improved version of Wide Mouth Frog protocol, but less secure than the Needham–Schroeder protocol.

The Neuman–Stubblebine protocol is a computer network authentication protocol designed for use on insecure networks. It allows individuals communicating over such a network to prove their identity to each other. This protocol utilizes time stamps, but does not depend on synchronized clocks.

The YAK is a public-key authenticated key-agreement protocol, proposed by Feng Hao in 2010. It is claimed to be the simplest authenticated key exchange protocol among the related schemes, including MQV, HMQV, Station-to-Station protocol, SSL/TLS etc. The authentication is based on public key pairs. As with other protocols, YAK normally requires a Public Key Infrastructure to distribute authentic public keys to the communicating parties. The security of YAK is disputed.

In cryptography, Woo–Lam refers to various computer network authentication protocols designed by Simon S. Lam and Thomas Woo. The protocols enable two communicating parties to authenticate each other's identity and to exchange session keys, and involve the use of a trusted key distribution center (KDC) to negotiate between the parties. Both symmetric-key and public-key variants have been described. However, the protocols suffer from various security flaws, and in part have been described as being inefficient compared to alternative authentication protocols.

References

  1. Briais, Sébastien; Nestmann, Uwe (2005). "A Formal Semantics for Protocol Narrations" (PDF). Trustworthy Global Computing. Lecture Notes in Computer Science. Vol. 3705. pp. 163–181. Bibcode:2005LNCS.3705..163B. doi:10.1007/11580850_10. ISBN   978-3-540-30007-6.
  2. Chappell, David (1999). "Exploring Kerberos, the Protocol for Distributed Security in Windows 2000". Microsoft Systems Journal. Archived from the original on 2017-08-15.
  3. Steiner, J. G.; Neuman, B. C.; Schiller, J. I. (February 1988). "Kerberos: An Authentication Service for Open Network Systems" (PDF). Proceedings of the Winter 1988 Usenix Conference. Usenix. Berkeley, CA: USENIX Association. pp. 191–201. Retrieved 2009-06-10.
  4. Davis, Don; Swick, Ralph (1989-03-17). Workstation Services and Kerberos Authentication at Project Athena (PS). p. 1. Retrieved 2009-06-10. …our notation follows Steiner, Neuman, & Schiller,…