TY - GEN
T1 - On modelling security protocols for logic-based verification
AU - Dojen, Reiner
AU - Chen, Jinyong
AU - Coffey, Tom
PY - 2014
Y1 - 2014
N2 - Formal verification is an imperative step in the design cycle of security protocols. One of the most critical steps in formal verification is the formalisation of the security protocol in the language of the verification technique, as any mistakes in the formalisation can invalidate the outcome of the verification. However, security protocols are constantly evolving. Hence, verification techniques need to be adjusted to facilitate appropriate formalisations of newly arising features or operations of security protocols. This paper concerns modelling security protocols for formal verification. Different ways to model lightweight operations in a logic-based verification tool are discussed. An extension of the verification tool, that facilitates direct modelling of lightweight operations in security protocols, is then described. Finally, a remote authentication scheme is formalised and verified using the extended tool.
AB - Formal verification is an imperative step in the design cycle of security protocols. One of the most critical steps in formal verification is the formalisation of the security protocol in the language of the verification technique, as any mistakes in the formalisation can invalidate the outcome of the verification. However, security protocols are constantly evolving. Hence, verification techniques need to be adjusted to facilitate appropriate formalisations of newly arising features or operations of security protocols. This paper concerns modelling security protocols for formal verification. Different ways to model lightweight operations in a logic-based verification tool are discussed. An extension of the verification tool, that facilitates direct modelling of lightweight operations in security protocols, is then described. Finally, a remote authentication scheme is formalised and verified using the extended tool.
KW - Exclusive-or operation
KW - Formal verification
KW - Logic based verification tool
KW - Remote user authentication protocol
UR - http://www.scopus.com/inward/record.url?scp=84946042115&partnerID=8YFLogxK
U2 - 10.1049/cp.2014.0663
DO - 10.1049/cp.2014.0663
M3 - Conference contribution
AN - SCOPUS:84946042115
SN - 9781849199247
T3 - IET Conference Publications
SP - 79
EP - 84
BT - IET Conference Publications
PB - Institution of Engineering and Technology
T2 - 25th IET Irish Signals and Systems Conference, ISSC 2014 and China-Ireland International Conference on Information and Communications Technologies, CIICT 2014
Y2 - 26 June 2014 through 27 June 2014
ER -