Projet ROSSIGNOL
(ACI Sécurité Informatique)

Goal

Verification of Cryptographic Protocols

Teams

Events

Report on the project

  • Final Report
  • Middle term report

    Meetings

  • Palaiseau (2006, April 25th)
  • PARISTIC (Labri 2005, november 21-23 )
  • Cachan, 13 decembre 2004.
  • Grenoble, 2 decembre 2003.

    Publications

    (De)Compositions of Cryptographic Schemes and their Applications to Protocols. R. Janvier, Y. Lakhnech and L. Mazaré. PS

    Probabilistic Opacity for a Passive Adversary and its Application to Chaum's Voting Scheme. Y. Lakhnech and L. Mazaré. Research Report

    Véronique Cortier, Stéphanie Delaune and Pascal Lafourcade. A Survey of Algebraic Properties used in Cryptographic Protocols. PS Journal of Computer Security. To appear

    Intruder Detection in AC-like Equational Theories. P.Lafourcade, D.Lugiez, R. Treinen. To appear in Proc. RTA 05. Research Report PS

    Axiomatizations for probabilistic finite-state behaviors. By Yuxin Deng and Catuscia Palamidessi. In Proceedings of the ETAPS 2005 member conference on Foundations of Software Science and Computation Structures (FOSSACS 2005), Edinburgh, U.K., April 2005, LNCS. Springer.
    Report version: PDF, PS.

    Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus. Steve Kremer and Mark D. Ryan. In Proceedings of the 14th European Symposium on Programming (ESOP'05), Edinburgh, U.K., April 2005, LNCS. Springer.

    Using Unification For Opacity Properties, by Laurent Mazaré Workshop on Issues in the Theory of Security (WITS'04), Barcelona, Spain, 2004. PDF

    Satisfiability of Dolev-Yao Constraints, by Laurent Mazaré: Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA'04), Cork, Ireland, 2004. PDF

    Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries by R. Janvier, Y. Lakhnech and L. Mazare, Technical Report, October 2004. http://www-verimag.imag.fr/TR/TR-2004-19.ps PDF

    A symbolic decision procedure for cryptographic protocols with time stamps by L. Bozga, C. Ene and Y. Lakhnech Verimag Technical Report number TR-2004-2, Oct 2004. Accepted in the Journal of Logic and Algebraic Programming. PS

    A randomized encoding of the Pi-calculus with mixed choice by Catuscia Palamidessi, to appear to TCS. PDF

    A theory of Dictionary Attacks and its Complexity. S.Delaune and F. Jacquemard. Computer Security Workshop

    A decision procedure for the verification of security protocols with explicit destructors, by S. Delaune and F. Jacquemard. In Proc. 11th ACM Conf. on Computer and Communications Security (CCS 2004). PS

    A Proof Search Specification of the π-Calculus, by Alwen Tiu and Dale Miller. PDF

    Encryption as an abstract data-type: An extended abstract, by Dale Miller. FCS 2003: Foundations of Computer Security. Edited by Iliano Cervesato, pp. 3-14, June 2003.

    Members


    Denis Lugiez
    Last modified: Mon Nov 6 19:28:17 CET 2006