Gilles Barthe - César Kunz
Abstract. A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. Since in general certificates cannot be generated automatically, there is an interest in developing methods to reuse certificates. This article studies methods that transform certificates of a program into certificates of another program derived from the initial one by a semantically justified program transformation. We also study the related problem to transform certificates of a program instrumented with the results of a semantically justified program analysis, into a certificate of the original program. The transformations are conveniently described in the setting of abstract interpretation. We illustrate applications of our results to certificate translation and to the justification of hybrid certificates.