Title: Security properties analysis in a TPM-based protocol

Authors: Y. Seifi; S. Suriadi; E. Foo; C. Boyd

Addresses: Science and Engineering Faculty, Queensland University of Technology, Brisbane, Australia; Engineering Faculty, Bu-Ali Sina University, Hamedan, Iran ' Science and Engineering Faculty, Queensland University of Technology (QUT), Brisbane, Australia ' Science and Engineering Faculty, Queensland University of Technology (QUT), Brisbane, Australia ' NTNU, Department of Telematics, O.S. Bragstads plass 2A, NO-7491 Trondheim, Norway

Abstract: Security protocols are designed in order to provide security properties (goals). They achieve their goals using cryptographic primitives such as key agreement or hash functions. Security analysis tools are used in order to verify whether a security protocol achieves its goals or not. The analysed property by specific purpose tools are predefined properties such as secrecy (confidentiality), authentication or non-repudiation. There are security goals that are defined by the user in systems with security requirements. Analysis of these properties is possible with general purpose analysis tools such as coloured petri nets (CPN). This research analyses two security properties that are defined in a protocol that is based on trusted platform module (TPM). The analysed protocol is proposed by Delaune to use TPM capabilities and secrets in order to open only one secret from two submitted secrets to a recipient.

Keywords: CPN; coloured Petri nets; security analysis; security properties; TPM; trusted platform module; ASK-CTL; cryptography.

DOI: 10.1504/IJSN.2014.060742

International Journal of Security and Networks, 2014 Vol.9 No.2, pp.85 - 103

Received: 07 May 2013
Accepted: 02 Oct 2013
Published online: 02 May 2015 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article