An intruder model with message inspection for model checking security protocols