Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Certificates for Tree Automata Completion
Roberto Zunino
abstract:
We consider the problem of certifying the correctness of a protocol or security API through a formal, machine-checkable proof. To this aim, we re-examine the completion algorithm for tree automata and term rewriting systems, that computes an over-approximation of regular sets of terms up to rewriting. We then define a procedure to certify, via a proof, that the result of the completion is indeed correct. Hence, with our procedure, a program verification tool that uses the completion algorithm can certify its results. As a consequence, we do not need to regard the tool as a trusted component of the verification process. We discuss on our experiments in which we automatically generated security proofs for some selected protocols.
