Spécification et vérification des protocoles de sécurité probabilistes

Abstract : The concept of anonymity comes into play in those cases in which we want to keep secret the identity of the agents participating to a certain event. There is a wide range of situations in which this property may be needed or desirable; for instance: voting, web surfing, anonymous donations, and posting on bulletin boards. Anonymity is often formulated in more general way as an information-hiding property, namely the property that a part of information relative to a certain event is kept secret. One should be careful, though, not to confuse anonymity with other properties that the same description, notably confidentiality (aka secrecy). Let us emphasize the difference between the two concepts with respect to sending messages: confidentiality refers to situations in which the content of the message is to be kept secret; in the case of anonymity, on the other hand, it is the identity of the originator, or of the recipient, that has to be kept secret. Analogously, in voting, anonymity means that the identity of the voter associated with each vote must be hidden, and not the vote itself or the candidate voted for. Other notable properties in this class are privacy and noninterference. Privacy refers to he protection of certain data, such as the credit card number of a user. Noninterference means that a low user will not be able to acquire information about the activities of a high user. A discussion about the difference between anonymity and other information-hiding properties can be found in [HO03, HO05]. An important characteristic of anonymity is that it is usually relative to the capabilities of the observer. In general the activity of a protocol can be observed by diverse range of observers, di?ering in the information they have access to. The anonymity property depends critically on what we consider as observables. For example, in the case of an anonymous bulletin board, a posting by one member of the group is kept anonymous to the other members; however, it may be possible that the administrator of the board has access to some privileged information that may allow him to infer the identity of the member who posted it. In general anonymity may be required for a subset of the agents only. In order to completely define anonymity for a protocol it is therefore necessary to specify which se (s) of members have to be kept anonymous. A further generalization is the concept of anonymity with respect to a group: the members are divided into a number of sets, and we are allowed to reveal to which group the user responsible for the action belongs, but not the identity of the user himself. Various formal definitions and frameworks for analyzing anonymity have been developed in literature. They can be classied into approaches based on process-calculi ([SS96, RS01]), epistemic logic ([SS99, HO03]), and function views ([HS04]). Most of these approaches are based on the so-called principle of confusion : a system is anonymous if the set of possible observable outcomes is saturated with respect to the intended anonymous users. More precisely, if in one computation the culprit (the user who performs the action) is i and the observable outcome is o, then for every other agent j there must be a computation where j is the culprit and the observable is still o. This approach is also called possibilistic, and relies on nondeterminism. In particular, probabilistic choices are interpreted as nondeterministic. We refer to RS01] for more details about the relation of this approach to the notion of anonymity.
Document type :
Informatique [cs]. Ecole Polytechnique X, 2007. Français

Contributor : Ecole Polytechnique <>
Submitted on : Tuesday, July 27, 2010 - 2:07:11 PM
Last modification on : Wednesday, July 28, 2010 - 9:50:16 AM
Document(s) archivé(s) le : Tuesday, October 23, 2012 - 11:15:24 AM


  • HAL Id : pastel-00003950, version 1



Konstantinos Chatzikokolakis. Spécification et vérification des protocoles de sécurité probabilistes. Informatique [cs]. Ecole Polytechnique X, 2007. Français. <pastel-00003950>




Record views


Document downloads