In the paper [A logic for abstract state machines, J.UCS Vol.7(11) 2001, 
pp. 981-1006] we presented a logic for Abstract State Machines (ASMs).
In this technical report, we present an interactive theorem prover
called ASMKEY where we implemented this logic. We also present a small case
study to show the effectiveness of our approach.