Security Protocol Design

Jayasinghe, D., Markantonakis, K., Mayes, K.: Optimistic Fair-Exchange with Anonymity for Bitcoin Users. To appear in the 11th IEEE International Conference on e-Business Engineering (IEEE ICEBE-14). IEEE Computer Society, Guangzhou, China (2014).Abstract
Fair-exchange and anonymity are two important attributes in e-commerce. It is much more difficult to expect fairness in e-commerce transactions using Bitcoin due to anonymity and transaction irreversibility. Genuine consumers and merchants who would like to make and receive payments using Bitcoin may be reluctant to do so due to this uncertainty. The proposed protocol guarantees strong-fairness while preserving anonymity of the consumer and the merchant, using Bitcoin as a payment method which addresses the aforementioned concern. The involvement of the trusted third party (TTP) is kept to a minimum, which makes the protocol optimistic and the exchanged product is not revealed to TTP. It achieves dispute resolution within the protocol run without any intervention of an external judge. Finally we show how the protocol can be easily adapted to use other digital cash systems designed using public ledgers such as Zerocoin/Zerocash.
Abughazalah, S., Markantonakis, K., Mayes, K.: Secure Mobile Payment on NFC-Enabled Mobile Phones Formally Analysed Using CasperFDR. Trust, Security and Privacy in Computing and Communications (TrustCom), 2014 13th IEEE International Conference on. IEEE Computer Society (2014).Abstract
Near Field Communication (NFC) mobile phones can be used as payment devices and can emulate credit cards. Although NFC mobile services promise a fruitful future, several issues have been raised by academics and researchers. Among the main concerns for the use and deployment of NFC-enabled mobile phones is the potential loss of security and privacy. More specifically, mobile phone users involved in a payment transaction conducted over a mobile handset require that such a system does not reveal their identity or any sensitive data. Furthermore, that all entities participating in the transaction are legitimate. To this end, we proposed a protocol that meets the mobile user' requirements. The proposed protocol attempts to address the main security concerns and protects the customer privacy from any third party involved in the transaction. We formally analysed the protocol using CasperFDR and did not find any feasible attacks.
Abughazalah, S., Markantonakis, K., Mayes, K.: A Mutual Authentication Protocol for Low-Cost RFID Tags Formally Verified Using CasperFDR and AVISPA. The 5th International Workshop on RFID Security and Cryptography 2013 (RISC'13), Internet Technology and Secured Transactions. 50-55 (2013).Abstract
Although Radio Frequency IDentification (RFID) systems offer many remarkable characteristics, security and privacy concerns are not easy to address. In this paper, we aim to overcome some of the significant privacy and security concerns by proposing a simple and lightweight RFID mutual authentication protocol. Our protocol is utilising hash functions and simple bitwise operations in an attempt to extract the strengths found in previous protocols and avoid their deficiencies. We found that the majority of the proposed protocols fail to resist DoS attacks when the attacker blocks the messages exchanged between the reader and tag more than once. Moreover, recent research focused on the security side and ignored performance. Our proposed protocol aims to solve these issues. We provide an informal analysis along with automated formal analysis using CasperFDR and AVISPA. The results show that the proposed protocol guarantees secret data secrecy and authentication under the presence of a passive adversary.
Abughazalah, S., Markantonakis, K., Mayes, K.: A Vulnerability in the Song Authentication Protocol for Low-Cost RFID Tags. In: Janczewski, L.J., Wolfe, H.B., and Shenoi, S. The 25th IFIP International Information Security Conference (SEC 2013). p. 102-110. Springer Berlin Heidelberg, Auckland, New Zealand (2013).Abstract
In this paper, we describe a vulnerability against one of the most efficient authentication protocols for low-cost RFID tags proposed by Song. The protocol defines a weak attacker as an intruder which can manipulate the communication between a reader and tag without accessing the internal data of a tag. It has been claimed that the Song protocol is able to resist weak attacks, such as denial of service (DoS) attack. However, we found that a weak attacker is able to desynchronise a tag, which is one kind of DoS attack. Moreover, the database in the Song protocol must use a brute force search to retrieve the tag's records affecting the operational performance of the server. Finally, we propose an improved protocol which can prevent the security problems in Song protocol and enhance the server's scalability performance.
Rantos, K., Markantonakis, K.: An Asymmetric Cryptography Secure Channel Protocol for Smart Cards. In: Deswarte, Y., Cuppens, F., Jajodia, S., and Wang, L. Security and Protection in Information Processing Systems. p. 350-365. Springer US, Toulouse, France (2004). WebsiteAbstract
Smart card secure channel protocols based on public key cryptography are not widely utilised mainly due to processing overheads introduced in the underlying smart card microprocessors and the complexities introduced by the operation of a PKI infrastructure. In this paper we analyse the significance of public key secure channel protocols in multi application smart cards. We believe that multi application smart card technology (e.g. the GlobalPlatform smart card specification) should benefit more from the advantages of public key cryptography specifically for the initiation and maintenance of a secure channel. This paper introduces a public key based cryptographic protocol for secure entity authentication, data integrity and data confidentiality. The proposed secure channel protocol uses a combination of public key, secret key and the main idea behind the Diffie-Hellmann key establishment protocols in order to achieve the desired goals.
Markantonakis, K., Mayes, K.: A Secure Channel Protocol for Multi-Application Smart Cards Based on Public Key Cryptography. In: Chadwick, D. and Preneel, B. Communications and Multimedia Security. p. 79-95. Springer US (2004). WebsiteAbstract
Smart card secure channel protocols based on public key cryptography are not widely utilised mainly due to processing overheads introduced in the underlying smart card microprocessors and the complexities introduced by the operation of a PKI infrastructure. In this paper we analyse the significance of public key secure channel protocols in multi-application smart cards. We believe that multi-application smart card technology (e.g. the GlobalPlatform smart card specification) should benefit more from the advantages of public key cryptography specifically for the initiation and maintenance of a secure channel. This paper introduces a public key based cryptographic protocol for secure entity authentication, data integrity and data confidentiality. The proposed secure channel protocol uses a combination of public key, secret key and the main idea behind the Diffie-Hellman key establishment protocols in order to achieve the desired goals.
Markantonakis, C.: Boundary Conditions that Influence Decisions about Log File Formats in Multi-application Smart Cards. In: Varadharajan, V. and Mu, Y. Information and Communication Security. p. 230-243. Springer Berlin Heidelberg, Sydney, Australia (1999). WebsiteAbstract
In real world smart card applications, smart card log files are mainly used for storing receipts for the successful or otherwise completion of certain events. In traditional single application smart card environments, the decision on which events to be logged was made by the application developer. We believe that in today's multi-application environments the situation is rather more complicated. If more than one application shares the same smart card, a whole range of new events require logging. In this paper we provide suggestions as to the new events to be logged. Furthermore, we propose a standard format for smart card log files in order to make dispute reconciliation procedures easier and faster, and also to efficiently manage the valuable log file space. Finally, we provide some results from an implementation of the proposed standard format in a Java Card.
Markantonakis, C.: Secure Log File Download Mechanisms for Smart Cards. In: Quisquater, J.-J. and Schneier, B. Smart Card Research and Applications. p. 285-304. Springer Berlin Heidelberg, UCL Louvain-La-Neuve-Belgium (2000). WebsiteAbstract
The necessity of auditing mechanisms for smart cards is currently under thorough investigation. Both current and future real world applications impose requirements which suggest the storage of sensitive information in log files. In this paper we present various applications that demonstrate the use of audit logs, justifying their practical advantages and disadvantages. We propose computationally practical methods for creating and maintaining such log files in the light of the limited memory of smart cards. We conclude with a brief discussion of design principles for future implementations and guidelines for further research.
Akram, R.N., Markantonakis, K., Mayes, K.: A Privacy Preserving Application Acquisition Protocol. In: Geyong Min, F.G.M. 11th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (IEEE TrustCom'12). p. 383-392. IEEE Computer Society, Liverpool, United Kingdom (2012).Abstract
In the smart card industry, the application acquisition process involves the card issuers and application providers. During this process, the respective card issuer reveals the identity of the smart card user to the individual application providers. In certain application scenarios it might be necessary (e.g. banking and identity applications). However, with introduction of the Trusted Service Manager (TSM) architecture there might be valid cases where revealing the card user's identity is not necessary. At the moment, the secure channel protocols for traditional smart card architecture including the TSM does not preserve the privacy of the card users. In this paper, we propose a secure and trusted channel protocol that provide such feature along with satisfying the requirements of an open and dynamic environment referred as User Centric Smart Card Ownership Model (UCOM). A comparison is provided between the proposed protocol and selected smart card protocols. In addition, we provide an informal analysis along with mechanical formal analysis using CasperFDR. Finally, we provide the test implementation and performance results.
Akram, R.N., Markantonakis, K., Mayes, K.: Application-Binding Protocol in the User Centric Smart Card Ownership Model. In: Parampalli, U. and Hawkes, P. The 16th Australasian Conference on Information Security and Privacy (ACISP). p. 208-225. Springer Berlin Heidelberg, Melbourne, Australia (2011).Abstract
The control of the application choice is delegated to the smart card users in the User Centric Smart Card Ownership Model (UCOM). There is no centralised authority that controls the card environment, and it is difficult to have implicit trust on applications installed on a smart card. The application sharing mechanism in smart cards facilitates corroborative and interrelated applications to co-exist and augment each other's functionality. The already established application sharing mechanisms (e.g. in Java Card and Multos) do not fully satisfy the security requirements of the UCOM. Therefore, the application sharing mechanism in the UCOM requires a security framework that provides runtime authentication, and verification of an application. Such a framework is the focus of this paper. To support the framework, we propose a protocol that is verified using CasperFDR. In addition, we implemented the protocol and provide a performance comparison with existing protocols.