security protocol notation

{{Short description|Notation for communication protocols}}

In cryptography, security (engineering) protocol notation, also known as protocol narrations{{cite book|last1=Briais|first1=Sébastien|last2=Nestmann|first2=Uwe|title=Trustworthy Global Computing |chapter=A Formal Semantics for Protocol Narrations |series=Lecture Notes in Computer Science |date=2005|volume=3705|pages=163–181|doi=10.1007/11580850_10|bibcode=2005LNCS.3705..163B|isbn=978-3-540-30007-6|chapter-url=http://sbriais.online.fr/papers/A_Formal_Semantics_For_Protocol_Narrations_TGC05-final.pdf}} 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:

:$A\backslash rightarrow\; B:\backslash \{X\backslash \}\_\{K\_\{A,B\}\}$

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

Another example might be the following:

:$B\backslash rightarrow\; A:\backslash \{N\_B\backslash \}\_\{K\_A\}$

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

A key with two subscripts, K_A,B, is a symmetric key shared by the two corresponding individuals. A key with one subscript, K_A, 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.

{{ cite journal

| last=Chappell

| first=David

| year=1999

| title=Exploring Kerberos, the Protocol for Distributed Security in Windows 2000

| journal=Microsoft Systems Journal

| url=https://www.microsoft.com/msj/0899/kerberos/kerberos.aspx

| archive-url=https://web.archive.org/web/20170815043157/https://www.microsoft.com/msj/0899/kerberos/kerberos.aspx

| url-status=dead

| archive-date=2017-08-15

}} Some authors consider the notation used by Steiner, Neuman, & Schiller

{{cite conference

| last1 = Steiner

| first1 = J. G.

| last2 = Neuman

| first2 = B. C.

| last3 = Schiller

| first3 = J. I.

|date=February 1988

| title = Kerberos: An Authentication Service for Open Network Systems

| conference = Usenix

| book-title = Proceedings of the Winter 1988 Usenix Conference

| publisher = USENIX Association

| location = Berkeley, CA

| pages = 191–201

| url = http://clifford.neuman.name/publications/1988/198802-Usenix-Kerberos/198802-Usenix-Steiner-Neuman-Schiller-Kerberos.pdf

| access-date = 2009-06-10

}} as a notable reference.

{{cite book

|author1=Davis, Don |author2=Swick, Ralph | title=Workstation Services and Kerberos Authentication at Project Athena

| date = 1989-03-17

| url = ftp://athena-dist.mit.edu/pub/ATHENA/kerberos/doc/user2user.ps

| format = PS

| access-date = 2009-06-10

| quote = …our notation follows Steiner, Neuman, & Schiller,…

| page = 1

}}

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.