Computational Soundness of Formal Indistinguishability and Static Equivalence
In the research of the relationship between the formal and the computational view of cryptography, a recent approach uses static equivalence from cryptographic pi calculi as a notion of formal indistinguishability. Previous work has shown that this yields the soundness of natural interpretations of some interesting equational theories, such as certain cryptographic operations and a theory of XOR. In this paper however, we argue that static equivalence is too coarse for sound interpretations of equational theories in general. We show some explicit examples how static equivalence fails to work in interesting cases. To fix this problem, we propose a notion of formal indistinguishability that is more flexible than static equivalence. We provide a general framework along with general theorems, and then discuss how this new notion works for the explicit examples where static equivalence failed to ensure soundness. We also improve the treatment by using ordered sorts in the formal view, and by allowing arbitrary probability distributions of the interpretations.
Faugere's F5 Algorithm Revisited
We present and analyze the F5 algorithm for computing Groebner bases. On the practical side, we correct minor errors in Faugere's pseudo code, and report our experiences implementing the -- to our knowledge -- first working public version of F5. While not designed for efficiency, it will doubtless be useful to anybody implementing or experimenting with F5. In addition, we list some experimental results, hinting that the version of F5 presented in Faugere's original paper can be considered as more or less naive, and that Faugere's actual implementations are a lot more sophisticated. We also suggest further improvements to the F5 algorithm and point out some problems we encountered when attempting to merge F4 and F5 to an "F4.5" algorithm. On the theoretical side, we slightly refine Faugere's theorem that it suffices to consider all normalized critical pairs, and give the first full proof, completing his sketches. We strive to present a more accessible account of the termination and correctness proofs of F5. Unfortunately, we still rely on a conjecture about the correctness of certain optimizations. Finally, we suggest directions of future research on F5.