We have previously shown how the distillation program transformation algorithm can be used to prove inductive theorems in which there is no explicit quantification, and all variables are assumed to be implicitly universally quantified. These techniques were implemented in the theorem prover Poitin. In this paper, we show how Poitin can be extended to prove inductive theorems which contain explicit universal and existential quantifiers, and give a proof of the soundness of this extension. This extension has also been implemented and added to Poitin; we give the results of applying the resulting theorem prover to a number of example conjectures.
We have previously shown how the inductive theorem prover Poitin can be extended to prove inductive theorems which contain explicit universal and existential quantifiers, and have given a proof of soundness of this extension. In this paper, we present a novel program construction method to construct recursive functional programs from metasystem transition proofs of existential theorems. This use of metasystem transition in our program construction technique is similar to Turchin's use of metasystem transition in conjunction with supercompilation to prove inductive theorems which contain explicit universal and existential quantifiers. We give a proof of correctness of the program construction method. We also argue that as programs are constructed using distillation, they are likely to be more efficient than programs constructed using other techniques. As far we know, this is the first technique which has been developed for the construction of programs from metasystem transition proofs. This extension has also been implemented and added to Poitin; we give the results of applying the resulting theorem prover to a number of input specifications.
We present a generic approach to overcoming key escrow in Identity-Based Signatures by using auditable signatures with strong non-repudiation properties. We also describe a concrete signature scheme and give an outline proof for the security of this scheme in the Random Oracle and Generic Group Models.