LSV Security Protocols Open Repository EVA LSV
Protocols format
How to submit
Contact us
Search the pages

Format of the protocol pages

Every security protocol of the repository is described in an individual html page, all the protocol pages are accessible from this index.

We describe below the different parts of a typical protocol page, a example of such a page can be found here.


The link send a comment let you send an email to the maintainer of the repository about the current protocol. The comment can be added to the page, in a specific section, with the name of the author and the date. We will always ask your authorisation before adding your comment to the page. Please let us know in the mail if you do not want to see your comment to figure in the public page.

Navigation links

The links Prev and Next leads to the other protocols immediately preceding and following the current protocol, with respect to the order in which the protocols are sorted in the protocols Index.

Download links

The protocol is available to download in many formats, accessible through the header links:
  • protocol specification in plain text: a text file containing only the protocol specification. See the remarks about the syntax.
  • page in compressed postscript: a postscript version of the contents of the page, compressed with gzip.
  • page in pdf: a pdf version of the contents of the page.
  • page source in latex the latex source file which has been used to generated all the other versions. This file can be useful e.g. if you are looking for examples in order to write a contribution (see the submission page).
  • bibTeX references: a bibtex file with the references concerning the protocol.

Title, authors, abstract

Following the title of the protocol come in this order:
  • the name(s) of the original authors of the protocol,
  • the date of the first publication of the protocol,
  • (optionally) the name of the person who has submitted the protocol to the repository,
  • and the date of submission.
Then follows a short description (abstract) of the protocol goals and, optionally, of the protocol needs in term of cryptographic functionalities.

The protocol title and abstract are found in the repository index and (in comments) in the text version of the protocol specification.

Protocol specification

The messages of the protocol can be specified in one of the two form:
  • following the common syntax defined below (in this case, the fact that the specification follows this syntax is mentioned in the title of the section).
  • in a free syntax, in particular when some particularities of the protocol do not fit in the proposed syntax.
In both cases, the specification of the protocol messages can be preceded by some type declarations.

The comments are preceded by '//' in the protocol specifications.

Common syntax

We propose a common syntax for the specification of protocol messages which is close to the one of the BAN paper [BAN89], which has been adopted in many latter theoretical works about cryptographic protocols.

For instance, most of the the authentication protocols in the famous Clark and Jacob survey [CJ97] follow this syntax (except fot the notation of the encryption operator). However, has mentioned above, not all the specifications of the protocols repository shall necessarily follow this syntax.

Of course, such a very general syntax cannot avoid imprecisions and ambiguities concerning the actions taken by the principals following the protocol. Some actions can be added between two protocol messages to describe some actions of the receiver of the first message. The syntax for these actions is free.

The common syntax for protocol messages is defined by the following context free grammar, where (exp)* denotes 0 or more times exp, (exp)+ denotes 1 or more times exp, (exp)? denotes 0 or 1 time exp:
messages   :=    (message (action)? )+
message := label'.' id '->' id':' tuple
label := id
id := non empty sequence of alphanumeric characters, or '-', '_'
tuple := atom (',' atom)*
atom := cipher
    | clearterm
clearterm := id
    | apply
    | '(' (tuple)? ')'
cipher := { tuple }clearterm
apply := id'('tuple')'
action := arbitrary text
The identifiers (n.t. id) are protocol variables of a primitive types or functions, like one-way (hash) functions or functions which associate keys to principal names for instance. A primitive is proposed for encryption, with the usual notation using brackets. However, special identifier can also be used for encryption, when more details are needed.

The identifiers can be declared before the protocol messages. The form of the type declaration of primitive or functional identifiers is free. In particular, in case of public key cryptography, a particular notation can be used to associate the public and private of a keypair.

Note that tuples can be written with or without parentheses. We assume by default that a tuple a0, a1, ..., an written without parentheses is left-associated.


Since many semantics exist for cryptographic protocols given in the above syntax, we have chosen not to impose one for the repository. The semantical aspects of a protocol can be discussed in the following section.


This section contains some additional information about the protocol variables, the initial conditions, the treatment of received messages and the construction of new message by principals, the flow control of the protocol execution... and in general anything that can explain that is not explicit in the protocol specification.

Some equational axioms for functional identifiers can also be given here.


Some properties that the protocol is supposed to ensure are written here in natural language.


This section cites the papers in which the protocol has been published and also tutorials or surveys in which the protocol is described.

This section does not cite the papers studying the protocol, this is the purpose of the two next sections.

Claimed proofs

This sections cites the works providing a formal proof of correctness of the protocol, or at least of one of the requirements cited above.

Important remark: We do not check the correctness of the claims presented in protocols pages. Rather, the purpose of this section (and of the next one ``claimed attacks'') is to cite accurately some published works found about the protocols presented. This repository is an open and collective work, that we hope to update permanently. So if you see some possible improvements or correction, let us know, in particular:
  • If a proof (or an attack) cited appears to be incorrect, please let us know by clicking the link send a comment in the page's header. Your comment will be added on the page, after the section concerned (see the description of the section comment).

  • If you think that the presentation of some work is not accurate, please let us know also. We will make the necessary correction.

  • At last, if you know some work concerning a cryptographic protocol of the repository that is not cited in the protocole's page, please send us a pointer to this work (again using the link send a comment). It will be added to the page.

Claimed attacks

This sections cites the works which claim to have demonstrated a vulnerability of the protocol, with respect to the requirements cited above.

Sometimes, one (or several) scenario of attack can be found here. A scenario is a sequence of messages, possibly involving 2 or more interlaced sessions of the protocol, written in the same syntax as the protocol specification.

Following the syntax in use in the Clark and Jacob survey [CJ97] we use two special constructors for the sender and receiver names in order to describe a specific action of a malicious agent (the intruder I):
  • the eaves dropping by the intruder I of a message:
    label.   sender -> I(receiver) :   message contents
  • the sending of a message by the intruder I, with impersonation of another principal sender:
    label.   I(sender) -> receiver :   message contents


This section cites a comment that as been sent by a reader, his name and the date are given in the title. The comments are moderated.


This optional section contains additional remarks.

See also

Cross references to other protocols of the repository.


The last section of every protocol page contains a list of the bibliographical references cited in the page.


The footer repeats the links home and send a comment of the header, as well as the navigation links.


John Clark and Jeremy Jacob. A survey of authentication protocol literature : Version 1.0., November 1997. jac/papers/

Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. Technical Report 39, Digital Systems Research Center, february 1989.

This document was translated from LATEX by HEVEA.