Using bisimulation proof techniques for the analysis of distributed abstract machines