BACK TO INDEX

Publications of year 2000

Books and proceedings

  1. I. Attali and T. Jensen, editors. Proceedings of the International Workshop on Java Card (Java Card 2000), Cannes, France, Septembre 2000. Inria. 
    @Proceedings{Jensen:00:JavaCard,
Title={Proceedings of the International Workshop on Java Card (Java Card 2000)},
Year={2000},
Editor={I. Attali and T. Jensen},
Publisher={Inria},
Address={Cannes, France},
Month={Septembre} 
}


Thesis

  1. Pascal Fradet. Approches langages pour la conception et la mise en oeuvre de programmes. document d'habilitation à diriger des recherches, Université de Rennes 1, novembre 2000. 
    @PhDThesis{HDR-PF,
Author={Pascal Fradet},
Title={Approches langages pour la conception et la mise en {\oe}uvre de programmes},
School = {Université de Rennes 1},
Type = "document d'habilitation à diriger des recherches",
Month={novembre},
Year={2000} 
}


  2. Michaël Périn. Spécifications graphiques multi-vues : formalisation et vérification de cohérence. PhD thesis, IFSIC, October 2000. 
    @PhdThesis{ThesePerin,
author = {Périn, Michaël},
title = "{Spécifications graphiques multi-vues : formalisation et vérification de cohérence}",
school = {IFSIC},
year = 2000,
month = oct,

}


Conference articles

  1. E. Denney and T. Jensen. Correctness of Java Card method lookup via logical relations. In Proc. of European Symp. on Programming (ESOP 2000), Lecture Notes in Computer Science, pages 104-118, 2000. Springer. 
    @InProceedings{Denney:00:Correctness,
author = {E. Denney and T. Jensen},
title = {Correctness of {J}ava {C}ard method lookup via logical relations},
booktitle = {Proc.~of European Symp. on Programming (ESOP 2000)},
year = {2000},
pages="104--118",
SERIES = {Lecture Notes in Computer Science},
publisher = {Springer} 
}


  2. T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification. In Proceedings 17th International Conference on Automated Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, 2000. Springer-Verlag. [WWW] Keyword(s): Cryptographic Protocol, Verification, Term Rewriting, Reachability, Approximation, Timbuk.
    On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation.

    @INPROCEEDINGS{GenetKlay-CADE00,
AUTHOR = {Genet, T. and Klay, F.},
TITLE = {{R}ewriting for {C}ryptographic {P}rotocol {V}erification},
BOOKTITLE = {Proceedings 17th International Conference on Automated Deduction},
SERIES = {Lecture Notes in Artificial Intelligence},
PUBLISHER = {Springer-Verlag},
YEAR = {2000},
VOLUME= 1831,
KEYWORDS= {Cryptographic Protocol, Verification, Term Rewriting, Reachability, Approximation, Timbuk},
url = "ftp://ftp.irisa.fr/local/lande/tg-fk-cade00.ps.gz",
abstract= "On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation." 
}


Internal reports

  1. T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification (extended version). Technical Report 3921, INRIA, 2000. [WWW]
    On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation.

    @TECHREPORT{GenetK-CNET99,
AUTHOR = {Genet, T. and Klay, F.},
TITLE = {{R}ewriting for {C}ryptographic {P}rotocol {V}erification (extended version)},
INSTITUTION = {INRIA},
YEAR = {2000},
TYPE = {Technical Report},
NUMBER = {3921},
url = "ftp://ftp.irisa.fr/local/lande/tg-fk-inria00.ps.gz",
abstract= "On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation." 
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html