A Framework for the Rigorous Implementation of Security Protocols
Louise Robinson, NO Cook, SK Shrivastava · School of Computing Science Technical Report Series · 2005
The correct implementation of security protocols is a challenging task. Like any software, to gain high confidence in a given implementation, ideally one requires both: (i) a formal specification that has been subjected to verification; and (ii) tool support to generate an implementation from the verified specification. The former area has attracted considerable attention for security protocols, and significant advances have been made. In the latter area, the state of the art has not progressed beyond simple security protocols with a small number of steps. This paper presents an improved approach to protocol implementation. Starting with a formal protocol specification, a rigorous process with considerable tool support leads to the deployment of implementations in a flexible middleware framework for their execution. To illustrate the approach, the paper describes the implementation of a deterministic, fair non-repudiation protocol. Such protocols are quite complex, as they require both sub-protocols and trusted third party involvement in order to guarantee fairness. Therefore, it is reasonable to assume that we can extend the approach to a wide range of less complex, deterministic security protocols. © 2005 University of Newcastle upon Tyne. Printed and published by the University of Newcastle upon Tyne, Computing Science, Claremont Tower, Claremont Road, Newcastle upon Tyne, NE1 7RU, England. Bibliographical details ROBINSON, P., COOK, N., SHRIVASTAVA, S.. A Framework for the Rigorous Implementation of Security Protocols [By] P. Robinson, N. Cook and S. Shrivastava. Newcastle upon Tyne: University of Newcastle upon Tyne: Computing Science, 2005. (University of Newcastle upon Tyne, Computing Science, Technical Report Series, No. CS-TR-937)