|
|
|
|
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.
Header
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.
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.
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 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.
Semantics
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.Explanations
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.
Requirements
Some properties that the protocol is supposed to ensure are written here in natural language.References
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
Comment
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.Remarks
This optional section contains additional remarks.See also
Cross references to other protocols of the repository.Citations
The last section of every protocol page contains a list of the bibliographical references cited in the page.Footer
The footer repeats the links home and send a comment of the header, as well as the navigation links.Citations
- [CJ97]
-
John Clark and Jeremy Jacob.
A survey of authentication protocol literature : Version 1.0.,
November 1997.
http://www-users.cs.york.ac.uk/ jac/papers/drareview.ps.gz
- [BAN89]
- Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. Technical Report 39, Digital Systems Research Center, february 1989.