Model checking security protocols using a logic of belief