Abstract
The need for secure communication has prompted the development of security protocols---prescribed sequences of interaction designed to establish some security related goal (typically in a hostile environment). Security protocols are deceptively simple objects that often harbour subtle errors. As such, recent years have witnessed the development of a large number of techniques for their formal analysis; some aim at the discovery of attacks, others at establishing correctness. Schneider's approach, based on rank functions, provided a framework within which the correctness of authentication protocols can be rigorously established. This work was subsequently carried forward by Heather and Evans who touched upon, but did not fully address, the use of the approach in establishing secrecy properties. This thesis fills that gap by tailoring the central concept of a rank function for the verification of secrecy properties. We also describe how low-level properties of an underlying cryptosystem may be incorporated into analyses, yielding stronger proofs of correctness than those based on the perfect encryption assumption. In addition, we provide the first general approach for reasoning about forward secrecy; describe how the rank function approach fails when we attempt to reason about this property; and develop the concept of a temporal rank to address this problem.