ABSTRACT. Symbolic verification of security protocols typically relies on an attacker model called the Dolev-Yao model, which does not model adequately various algebraic properties of cryptographic operators used in many real-world protocols. In this work we describe an integration of a state-of-the-art protocol verifier ProVerif, with automated first order theorem provers (ATP). The integration allows one to model directly algebraic properties of cryptographic operators as a first-order equational theory and the specified protocol can exported to a first-order logic specification in the standard TPTP format for ATP. An attack on a protocol corresponds to a refutation using the encoded first order clauses. We implement a tool that analyses this refutation and extracts an attack trace from it, and visualises the deduction steps performed by the attacker. We show that the combination of ProVerif and ATP can find attacks that cannot be found by ProVerif when algebraic properties are taken into account in the protocol verification.

ABSTRACT. On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes implementations inherently error prone. As a remedy, we provide a formally verified certifier for ordered completion based techniques. This certifier is code generated from an accompanying Isabelle/HOL formalization of ordered rewriting and ordered completion incorporating an advanced ground joinability criterion. It allows us to rigorously validate generated proof certificates from several domains: ordered completion, satisfiability in equational logic, and confluence of conditional term rewriting.

ABSTRACT. Decision procedures for various list theories has been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

ABSTRACT. We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.

ABSTRACT. Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for for manipulating proof terms.