Background, aim and scope

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. However, proofs in this model are difficult and less successful for large, complex protocols. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs of complex protocols. However, the guarantees that it offers with respect to a deployed protocol have been quite unclear. The workshop focuses on the relation between the symbolic (Dolev-Yao) model and the computational (complexity-theoretic) model. Recent results have shown that in some cases the symbolic analysis is sound with respect to the computational model. A more direct approach which is also investigated considers symbolic proofs in the computational model. The workshop seeks results in any of these areas, and more generally, in the area of system and program verification for security and cryptography.

FCC’07 will be held in Venice, Italy on July 4-5th preceding CSF’07, the 20th IEEE Computer Security Foundations Symposium (previously CSFW). We invite submissions that present original results on the topics of the workshop. We also encourage submissions that describe work in progress or that further publicise interesting results published elsewhere. The main goal of the workshop is to stimulate discussions and new collaborations.

Réalisation Axome - Création de sites Internet