Informal analysis of authenticated key establishment (ake) protocols was commonly accepted as the valid argument for their security in the past. Although it can provide some confidence in protocol correctness, experience has shown time and again that ake protocols are likely to contain flaws even after an informal analysis is completed. Therefore, it has become increasingly common to expect a formal analysis, and preferably a mathematical proof, of any published ake protocol in order to obtain increased confidence in its security. In this research we use an appropriate model for analysing ake protocols based on its features and properties. The model allows us to design ake protocols modularly and reuse existing protocol components. We provide a detailed description of its formalisation, operations and usage. This description also includes ways of extracting new protocol components from existing ake protocols. Following the description of the model, we propose a new unauthenticated key establishment protocol for two-party communications. By composing this protocol with authentication protocols, we can construct several new secure ake protocols. These new protocols are compared with existing protocols for their computational efficiency. The comparison shows that our new proven secure protocols are as efficient as the existing protocols with an informal security analysis. We then propose a three-party key establishment protocol which involves a trusted server and two users. We also propose a non-interactive authentication protocol and discuss it and a variant of it. These components are used to construct a secure three-party ake protocol that supports a privacy framework. This framework allows users to remain anonymous while conducting electronic transactions with an independent service provider. A new password-based authentication protocol is proposed to address the problem of authentication using passwords. This protocol carries a proof of security and satisfies a slightly relaxed definition of security. We demonstrate its application by composing it with existing key establishment protocols. To maximise its use, we modified a two-party key establishment protocol to become three-party server based. By using the server for authentication, two users within a common network domain can establish a secure session key. Only a small number of ake protocols are demonstrated in this thesis. There exist many more provably secure ake protocols that can be constructed using the protocol components presented by applying the approach of "mix and match". That is, each new component results in a number of new ake protocols depending on the number of existing components.

The Near Field Communication (NFC) technology is a short-range radio communication channel which enables users to exchange data between devices. NFC provides a contactless technology for data transmission between smart phones, Personal Computers (PCs), Personal Digital Assistants (PDAs) and such devices. It enables the mobile phone to act as identification and a credit card for customers. However, the NFC chip can act as a reader as well as a card, and also be used to design symmetric protocols. Having several parties involved in NFC ecosystem and not having a common standard affects the security of this technology where all the parties are claiming to have access to client’s information (e.g. bank account details). The dynamic relationships of the parties in an NFC transaction process make them partners in a way that sometimes they share their access permissions on the applications that are running in the service environment. These parties can only access their part of involvement as they are not fully aware of each other’s rights and access permissions. The lack of knowledge between involved parties makes the management and ownership of the NFC ecosystem very puzzling. To solve this issue, a security module that is called Secure Element (SE) is designed to be the base of the security for NFC. However, there are still some security issues with SE personalization, management, ownership and architecture that can be exploitable by attackers and delay the adaption of NFC payment technology. Reorganizing and describing what is required for the success of this technology have motivated us to extend the current NFC ecosystem models to accelerate the development of this business area. One of the technologies that can be used to ensure secure NFC transactions is cloud computing which offers wide range advantages compared to the use of SE as a single entity in an NFC enabled mobile phone. We believe cloud computing can solve many issues in regards to NFC application management. Therefore, in the first contribution of part of this thesis we propose a new payment model called “NFC Cloud Wallet". This model demonstrates a reliable structure of an NFC ecosystem which satisfies the requirements of an NFC payment during the development process in a systematic, manageable, and effective way.

Tendering is a method for entering into a sales contract. Numerous electronic tendering systems have been established with the intent of improving the efficiency of the tendering process. Although providing adequate security services is a desired feature in an e-tendering system, current e-tendering systems are usually designed with little consideration of security and legal compliance. This research focuses on designing secure protocols for e-tendering systems. It involves developing methodologies for establishing security requirements, constructing security protocols and using formal methods in protocol security verification. The implication is that it may prove suitable for developing secure protocols in other electronic business domains. In depth investigations are conducted into a range of issues in relation to establishing generic security requirements for e-tendering systems. The outcomes are presented in a form of basic and advanced security requirements for e-tendering process. This analysis shows that advanced security services are required to secure e-tender negotiation integrity and the submission process. Two generic issues discovered in the course of this research, functional difference and functional limitations, are fundamental in constructing secure protocols for tender negotiation and submission processes. Functional difference identification derives advanced security requirements. Functional limitation assessment defines how the logic of generic security mechanisms should be constructed. These principles form a proactive analysis applied prior to the construction of security protocols. Security protocols have been successfully constructed using generic cryptographic security mechanisms. These protocols are secure e-tender negotiation integrity protocol suite, and secure e-tender submission protocols. Their security has been verified progressively during the design. Verification results show that protocols are secure against common threat scenarios. The primary contribution of this stage are the procedures developed for the complex e-business protocol analysis using formal methods. The research shows that proactive analysis has made this formal security verification possible and practical for complex protocols. These primary outcomes have raised awareness of security issues in e-tendering. The security solutions proposed in the protocol format are the first in e-tendering with verifiable security against common threat scenarios, and which are also practical for implementation. The procedures developed for securing the e-tendering process are generic and can be applied to other business domains. The study has made improvements in: establishing adequate security for a business process; applying proactive analysis prior to secure protocol construction; and verifying security of complex e-business protocols using tool aided formal methods.