Abstract. Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism. 							
						
							
					 															
					Benjamin W. Long, Colin J. Fidge, Antonio Cerone