| The wide spread of distributed systems, where resources and data are shared among users located almost everywhere in the world, has enormously increased the interest in security issues. It is important to precisely define security properties in order to have formal statements of the correctness of a security mechanism. As a consequence, in recent years, many formal definitions of security properties have been proposed. Among these theories, the information flow approach which aims at characterizing the complete absence of any causal flow from high level entities to low level ones, is very natural. However this requirement is too strong. Indeed, complete absence of any information flow can hardly be achieved in real systems. In order to deal with real applications, it is often necessary to admit mechanisms for downgrading or declassifying information. Also, in this thesis we deal with a particular class of admissible information flow security systems, namely cryptographic protocols.;Our contribution concerns several issues. We have first, proposed new characterizations of admissible information flow security properties and proved that they are general enough to capture most of security properties of cryptographic protocols. Indeed security properties such as confidentialy, authentication, non-repudiation [E,A,B] as well as the anonymity of customers in a recent extension of Visa and MasterCard e-commerce security payment protocol SET that we proposed [A,B], are some instances of admissible information flow security properties. Our approach is mechanized in a tool for symbolic analysis of crypto-protocols based on interference checking, called ASPiC [E]. This tool allowed us, in particular, to detect a new security flaw in the industrial e-commerce SET protocol [C,D]. The fact that the article [C] was rated number one in the TOP25 Hottest Articles - downloaded during January-March 2006- within the journal IPL, and continues to appear in this prize list almost two years after its publication, illustrates the importance of such formal approaches for the international scientific community.;However, our calculus and most of the formal approaches to analysis of cryptographic protocols are based on the possibilistic approach for modelling behaviors resulting from interactions between the protocol's agents and the perfect cryptography assumption for modelling the intruder. In the possibilistic approach, non-determinism is used as a mechanism for the random generation of all possible behaviors while the perfect cryptography assumption considers the encryption scheme as black boxes and assumes that an intruder cannot learn anything from a cypher text if she does not know the key. The possibilistic approach is not expressive enough to model probabilistic behaviors and so, to prevent attacks based on probabilistic distribution able to infer a secret from its observations.;Also, we proposed a probabilistic extension, a la Mitchell et al. 2006, of our model, extended with probabilistic polynomial time cryptographic primitives and probabilistic semantics. But when modelling cryto-protocols by means of process calculi which express both nondeterininistic and probabilistic behavior, it is customary to view the scheduler as an intruder. It has been established that the traditional scheduler needs to be carefully calibrated in order to more accurately reflect the intruder's capabilities for controlling communication channels. We have proposed such a class of schedulers through our probabilistic semantic extention [F,G,H]. Along these lines, we have defined a new characterization of Mitchell et al.'s asymptotic observational equivalence more suited for taking into account any observable traces instead of just a single observable as required in the analysis of many security protocols. However, as most contextual equivalences for cryptographic process calculi, our asymptotic equivalences suffer from quantification over all possible intruders. To overcome this problem, we have defined a context-sensitive semantics [I] allowing an implicit representation of the intruder. We have also defined a probabilistic bisimulation and showed that it refines the asymptotic equivalences. Finally, to illustrate the usefullness of our approach, we have proposed extensive case studies, the analysis of the Chaum's Dining Cryptographers protocol and the Ruben and Reiter's Crowds protocol. |
