G. Barthe and L. Prensa-Nieto.
Formally verifying information flow type systems for concurrent and
thread systems.
In M. Backes, D. Basin, and M. Waidner, editors, Proceedings of
FMSE'04, pages 13-22, Washington D.C., USA, October 2004. ACM Press.
[ bib |
.ps.gz ]
M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet.
Enforcing high-level security properties for applets.
In P. Paradinas and J.-J. Quisquater, editors, Proceedings of
CARDIS'04, Toulouse, France, August 2004. Kluwer Academic Publishers.
[ bib |
.pdf ]
G. Barthe, J. Cederquist, and S. Tarento.
A Machine-Checked Formalization of the Generic Model and the Random
Oracle Model.
In D. Basin and M. Rusinowitch, editors, Proceedings of
IJCAR'04, volume 3097 of Lecture Notes in Computer Science, pages
385-399, Cork, Ireland, July 2004. Springer-Verlag.
[ bib |
.ps.gz ]
G. Barthe, P. D'Argenio, and T. Rezk.
Secure Information Flow by Self-Composition.
In R. Foccardi, editor, Proceedings of CSFW'04, pages 100-114,
Pacific Grove,USA, June 2004. IEEE Press.
[ bib |
.ps.gz ]
G. Barthe and G. Dufay.
A Tool-Assisted Framework for Certified Bytecode Verification.
In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings
of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages
99-113, Barcelona, Spain, March 2004. Springer-Verlag.
[ bib |
.ps.gz ]
M. Huisman, D. Gurov, C. Sprenger, and G. Chugunov.
Checking absence of illicit applet interactions: a case study.
In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings
of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages
84-98, Barcelona, Spain, March 2004. Springer-Verlag.
[ bib |
.ps.gz ]
C. Sprenger, D. Gurov, and M. Huisman.
Compositional verification for secure loading of smart card applets.
In C. Heitmeyer and J.-P. Talpin, editors, Memocode'04, pages
211-222. IEEE Computer Society, 2004.
An earlier version appeared as INRIA Technical Report RR-4890.
[ bib |
.ps.gz ]
G. Barthe.
De la théorie des types à la vérification formelles des
petits objets portables de sécurité.
Habilitation à diriger des recherches, Université de Nice
Sophia-Antipolis, 2004.
[ bib ]
F. Bellegarde, J. Groslambert, M. Huisman, O. Kouchnarenko, and J. Julliand.
Verification of liveness properties with JML.
Technical Report RR-5331, INRIA, 2004.
[ bib |
.ps.gz ]