Format of the protocol pagesEvery 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.
HeaderThe 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 linksThe 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 linksThe protocol is available to download in many formats, accessible through the header links:
Title, authors, abstractFollowing the title of the protocol come in this order:
The protocol title and abstract are found in the repository index and (in comments) in the text version of the protocol specification.
Protocol specificationThe messages of the protocol can be specified in one of the two form:
The comments are preceded by '//' in the protocol specifications.
Common syntaxWe 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:
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.
SemanticsSince 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.
ExplanationsThis 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.
RequirementsSome properties that the protocol is supposed to ensure are written here in natural language.
ReferencesThis 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 proofsThis 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:
Claimed attacksThis 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):
CommentThis 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.
RemarksThis optional section contains additional remarks.
See alsoCross references to other protocols of the repository.
CitationsThe last section of every protocol page contains a list of the bibliographical references cited in the page.
FooterThe footer repeats the links home and send a comment of the header, as well as the navigation links.
This document was translated from LATEX by HEVEA.