Formal analysis of security properties in trusted computing protocols

This research introduces a general methodology in order to create a Coloured Petri Net (CPN) model of a security protocol. Then standard or user-defined security properties of the created CPN model are identified. After adding an attacker model to the protocol model, the security property is verified using state space method. This approach is applied to analyse a number of trusted computing protocols. The results show the applicability of proposed method to analyse both standard and user-defined properties.

Security properties analysis in a TPM-based protocol

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

Reinforcing bad behaviour : the misuse of security indicators on popular websites

Before making a security or privacy decision, Internet users should evaluate several security indicators in their browser, such as the use of HTTPS (indicated via the lock icon), the domain name of the site, and information from extended validation certificates. However, studies have shown that human subjects infrequently employ these indicators, relying on other indicators that can be spoofed and convey no cryptographic assurances. We identify four simple security indicators that accurately represent security properties of the connection and then examine 125 popular websites to determine if the sites' designs result in correctly displayed security indicators during login. In the vast majority of cases, at least some security indicators are absent or suboptimal. This suggests users are becoming habituated to ignoring recommended security indicators.

Model-checking bisimulation-based information flow properties for infinite state sstems

Bisimulation-based information flow properties were introduced by Focardi and Gorrieri [1] as a way of specifying security properties for transition system models. These properties were shown to be decidable for finite-state systems. In this paper, we study the problem of verifying these properties for some well-known classes of infinite state systems. We show that all the properties are undecidable for each of these classes of systems.

A framework for merging inconsistent beliefs in security protocol analysis

This paper proposes a framework for merging inconsistent beliefs in the analysis of security protocols. The merge application is a procedure of computing the inferred beliefs of message sources and resolving the conflicts among the sources. Some security properties of secure messages are used to ensure the correctness of authentication of messages. Several instances are presented, and demonstrate our method is useful in resolving inconsistent beliefs in secure messages.

Mobile agents security protocols

Mobile agents are expected to run in partially unknown and untrustworthy environments. They transport from one host to another host through insecure channels and may execute on non-trusted hosts. Thus, they are vulnerable to direct security attacks of intruders and non-trusted hosts. The security of information the agents collect is a fundamental requirement for a trusted implementation of electronic business applications and trade negotiations. This chapter discusses the security protocols presented in the literature that aim to secure the data mobile agents gather while searching the Internet, and identifies the security flaws revealed in the protocols. The protocols are analyzed with respect to the security properties, and the security flaws are identified. Two recent promising protocols that fulfill the various security properties are described. The chapter also introduces common notations used in describing security protocols and describes the security properties of the data that mobile agents gather.

Security framework for mobile agents-based applications

Mobile agents have been proposed for key applications such as forensics analysis, intrusion detection, e-commerce, and resource management. Yet, they are vulnerable to various security threats by malicious hosts or intruders. Conversely, genuine platforms may run malicious agents. It is essential to establish a truly secure framework for mobile agents to gain trust of clients in the system. Failure to accomplish a trustworthy secured framework for Mobile Agent System (MAS) will limit their deployment into the key applications. This chapter presents a comprehensive taxonomy of various security threats to Mobile Agent System and the existing implemented security mechanisms. Different mechanisms are discussed, and the related security deficiencies are highlighted. The various security properties of the agent and the agent platform are described. The chapter also introduces the properties, advantages, and roles of agents in various applications. It describes the infrastructure of the system and discusses several mobile agent frameworks and the accomplished security level.

Mobile Agents Security Protocols

Mobile agents are expected to run in partially unknown and untrustworthy environments. They transport from one host to another host through insecure channels and may execute on non-trusted hosts. Thus, they are vulnerable to direct security attacks of intruders and non-trusted hosts. The security of information the agents collect is a fundamental requirement for a trusted implementation of electronic business applications and trade negotiations. This chapter discusses the security protocols presented in the literature that aim to secure the data mobile agents gather while searching the Internet, and identifies the security flaws revealed in the protocols. The protocols are analyzed with respect to the security properties, and the security flaws are identified. Two recent promising protocols that fulfill the various security properties are described. The chapter also introduces common notations used in describing security protocols and describes the security properties of the data that mobile agents gather.

Conceptual Model and Security Requirements for DRM Techniques Used for e-Learning Objects Protection

This paper deals with the security problems of DRM protected e-learning content. After a short review of the main DRM systems and methods used in e-learning, an examination is made of participators in DRM schemes (e-learning object author, content creator, content publisher, license creator and end user). Then a conceptual model of security related processes of DRM implementation is proposed which is improved afterwards to reflect some particularities in DRM protection of e-learning objects. A methodical way is used to describe the security related motives, responsibilities and goals of the main participators involved in the DRM system. Taken together with the process model, these security properties are used to establish a list of requirements to fulfill and a possibility for formal verification of real DRM systems compliance with these requirements.

Improving tenants' trust in SaaS applications using dynamic security monitors

It is almost impossible to prove that a given software system achieves an absolute security level. This becomes more complicated when addressing multi-tenant cloud-based SaaS applications. Developing practical security properties and metrics to monitor, verify, and assess the behavior of such software systems is a feasible alternative to such problem. However, existing efforts focus either on verifying security properties or security metrics but not both. Moreover, they are either hard to adopt, in terms of usability, or require design-time preparation to support monitoring of such security metrics and properties which is not feasible for SaaS applications. In this paper, we introduce, to the best of our knowledge, the first unified monitoring platform that enables SaaS application tenants to specify, at run-time, security metrics and properties without design-time preparation and hence increases tenants’ trust of their cloud-assets security. The platform automatically converts security metrics and properties specifications into security probes and integrates them with the target SaaS application at run-time. Probes-generated measurements are fed into an analysis component that verifies the specified properties and calculates security metrics’ values using aggregation functions. This is then reported to SaaS tenants and cloud platform security engineers. We evaluated our platform expressiveness and usability, soundness, and performance overhead.

Modeling and Verification of Privacy Enhancing Protocols

Privacy enhancing protocols (PEPs) are a family of protocols that allow secure exchange and management of sensitive user information. They are important in preserving users’ privacy in today’s open environment. Proof of the correctness of PEPs is necessary before they can be deployed. However, the traditional provable security approach, though well established for verifying cryptographic primitives, is not applicable to PEPs. We apply the formal method of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PEP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allow us to reason about various security properties of PIEMCP using state space analysis techniques. This investigation provides us with preliminary insights for modeling and verification of PEPs in general, demonstrating the benefit of applying the CPN-based formal approach to proving the correctness of PEPs.

Quantum coins

One of the earliest cryptographic applications of quantum information was to create quantum digital cash that could not be counterfeited. In this paper, we describe a new type of quantum money: quantum coins, where all coins of the same denomination are represented by identical quantum states. We state desirable security properties such as anonymity and unforgeability and propose two candidate quantum coin schemes: one using black box operations, and another using blind quantum computation.

Applied batch cryptography

The material presented in this thesis may be viewed as comprising two key parts, the first part concerns batch cryptography specifically, whilst the second deals with how this form of cryptography may be applied to security related applications such as electronic cash for improving efficiency of the protocols. The objective of batch cryptography is to devise more efficient primitive cryptographic protocols. In general, these primitives make use of some property such as homomorphism to perform a computationally expensive operation on a collective input set. The idea is to amortise an expensive operation, such as modular exponentiation, over the input. Most of the research work in this field has concentrated on its employment as a batch verifier of digital signatures. It is shown that several new attacks may be launched against these published schemes as some weaknesses are exposed. Another common use of batch cryptography is the simultaneous generation of digital signatures. There is significantly less previous work on this area, and the present schemes have some limited use in practical applications. Several new batch signatures schemes are introduced that improve upon the existing techniques and some practical uses are illustrated. Electronic cash is a technology that demands complex protocols in order to furnish several security properties. These typically include anonymity, traceability of a double spender, and off-line payment features. Presently, the most efficient schemes make use of coin divisibility to withdraw one large financial amount that may be progressively spent with one or more merchants. Several new cash schemes are introduced here that make use of batch cryptography for improving the withdrawal, payment, and deposit of electronic coins. The devised schemes apply both to the batch signature and verification techniques introduced, demonstrating improved performance over the contemporary divisible based structures. The solutions also provide an alternative paradigm for the construction of electronic cash systems. Whilst electronic cash is used as the vehicle for demonstrating the relevance of batch cryptography to security related applications, the applicability of the techniques introduced extends well beyond this.

Strengthening and formally verifying privacy in identity management systems

In a digital world, users’ Personally Identifiable Information (PII) is normally managed with a system called an Identity Management System (IMS). There are many types of IMSs. There are situations when two or more IMSs need to communicate with each other (such as when a service provider needs to obtain some identity information about a user from a trusted identity provider). There could be interoperability issues when communicating parties use different types of IMS. To facilitate interoperability between different IMSs, an Identity Meta System (IMetS) is normally used. An IMetS can, at least theoretically, join various types of IMSs to make them interoperable and give users the illusion that they are interacting with just one IMS. However, due to the complexity of an IMS, attempting to join various types of IMSs is a technically challenging task, let alone assessing how well an IMetS manages to integrate these IMSs. The first contribution of this thesis is the development of a generic IMS model called the Layered Identity Infrastructure Model (LIIM). Using this model, we develop a set of properties that an ideal IMetS should provide. This idealized form is then used as a benchmark to evaluate existing IMetSs. Different types of IMS provide varying levels of privacy protection support. Unfortunately, as observed by Jøsang et al (2007), there is insufficient privacy protection in many of the existing IMSs. In this thesis, we study and extend a type of privacy enhancing technology known as an Anonymous Credential System (ACS). In particular, we extend the ACS which is built on the cryptographic primitives proposed by Camenisch, Lysyanskaya, and Shoup. We call this system the Camenisch, Lysyanskaya, Shoup - Anonymous Credential System (CLS-ACS). The goal of CLS-ACS is to let users be as anonymous as possible. Unfortunately, CLS-ACS has problems, including (1) the concentration of power to a single entity - known as the Anonymity Revocation Manager (ARM) - who, if malicious, can trivially reveal a user’s PII (resulting in an illegal revocation of the user’s anonymity), and (2) poor performance due to the resource-intensive cryptographic operations required. The second and third contributions of this thesis are the proposal of two protocols that reduce the trust dependencies on the ARM during users’ anonymity revocation. Both protocols distribute trust from the ARM to a set of n referees (n > 1), resulting in a significant reduction of the probability of an anonymity revocation being performed illegally. The first protocol, called the User Centric Anonymity Revocation Protocol (UCARP), allows a user’s anonymity to be revoked in a user-centric manner (that is, the user is aware that his/her anonymity is about to be revoked). The second protocol, called the Anonymity Revocation Protocol with Re-encryption (ARPR), allows a user’s anonymity to be revoked by a service provider in an accountable manner (that is, there is a clear mechanism to determine which entity who can eventually learn - and possibly misuse - the identity of the user). The fourth contribution of this thesis is the proposal of a protocol called the Private Information Escrow bound to Multiple Conditions Protocol (PIEMCP). This protocol is designed to address the performance issue of CLS-ACS by applying the CLS-ACS in a federated single sign-on (FSSO) environment. Our analysis shows that PIEMCP can both reduce the amount of expensive modular exponentiation operations required and lower the risk of illegal revocation of users’ anonymity. Finally, the protocols proposed in this thesis are complex and need to be formally evaluated to ensure that their required security properties are satisfied. In this thesis, we use Coloured Petri nets (CPNs) and its corresponding state space analysis techniques. All of the protocols proposed in this thesis have been formally modeled and verified using these formal techniques. Therefore, the fifth contribution of this thesis is a demonstration of the applicability of CPN and its corresponding analysis techniques in modeling and verifying privacy enhancing protocols. To our knowledge, this is the first time that CPN has been comprehensively applied to model and verify privacy enhancing protocols. From our experience, we also propose several CPN modeling approaches, including complex cryptographic primitives (such as zero-knowledge proof protocol) modeling, attack parameterization, and others. The proposed approaches can be applied to other security protocols, not just privacy enhancing protocols.

Privacy compliance verification in cryptographic protocols

To provide privacy protection, cryptographic primitives are frequently applied to communication protocols in an open environment (e.g. the Internet). We call these protocols privacy enhancing protocols (PEPs) which constitute a class of cryptographic protocols. Proof of the security properties, in terms of the privacy compliance, of PEPs is desirable before they can be deployed. However, the traditional provable security approach, though well-established for proving the security of cryptographic primitives, is not applicable to PEPs. We apply the formal language of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PEP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allow us to reason about various privacy properties of PIEMCP using state space analysis techniques. This investigation provides insights into the modelling and analysis of PEPs in general, and demonstrates the benefit of applying a CPN-based formal approach to the privacy compliance verification of PEPs.