Proving Time Bounds for Randomized Distributed Algorithms