Abstract This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that such proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra we use isμCRL, ACPτaugmented with data, which is expressive enough for the specification of real-life protocols. The proof checker we use is Coq, which is based on the Calculus of Constructions, an extension of simply typed lambda calculus. The focus is on the translation of the proof theory ofμCRL andμCRL-specifications to Coq. As a case study, we verified the Alternating Bit Protocol.

We present a general theory for the use of negative premises in the rules of Transition System Specifications (TSS's). We formulate a criterion that should be satisfied by a TSS in order to be meaningful, i.e. to unequivocally define a transition relation. We also provide powerful techniques for proving that a TSS satisfies this criterion, meanwhile constructing this transition relation. Both the criterion and the techniques originate from logic programming [8, 7] to which TSS's are close. As in [10], we show that the bisimulation relation induced by a TSS is a congruence, provided that it is in ntyft/ntyxt -format and can be proved meaningful using our techniques. As a running example, we study the combined addition of priorities and abstraction to Basic Process Algebra (BPA). Under some reasonable conditions we show that this TSS is indeed meaningful, which could not be shown by other methods [2, 10]. Finally, we provide a sound and complete axiomatization for this example. We have omitted most proofs here; they can be found in [3]. The first author is partly supported by the European Communities under ESPRIT Basic Research Action 3020 (Integration). The second author is supported by the European Communities under RACE project no. 1046 (SPECS) and ESPRIT Basic Research Action 3006 (CONCUR). These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.