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.

Human Kallikrein 4 signal peptide induces cytotoxic T cell responses in healthy donors and prostate cancer patients.

Immunotherapy is a promising new treatment for patients with advanced prostate and ovarian cancer, but its application is limited by the lack of suitable target antigens that are recognized by CD8+ cytotoxic T lymphocytes (CTL). Human kallikrein 4 (KLK4) is a member of the kallikrein family of serine proteases that is significantly overexpressed in malignant versus healthy prostate and ovarian tissue, making it an attractive target for immunotherapy. We identified a naturally processed, HLA-A*0201-restricted peptide epitope within the signal sequence region of KLK4 that induced CTL responses in vitro in most healthy donors and prostate cancer patients tested. These CTL lysed HLA-A*0201+ KLK4 + cell lines and KLK4 mRNA-transfected monocyte-derived dendritic cells. CTL specific for the HLA-A*0201-restricted KLK4 peptide were more readily expanded to a higher frequency in vitro compared to the known HLA-A*0201-restricted epitopes from prostate cancer antigens; prostate-specific antigen (PSA), prostate-specific membrane antigen (PSMA) and prostatic acid phosphatase (PAP). These data demonstrate that KLK4 is an immunogenic molecule capable of inducing CTL responses and identify it as an attractive target for prostate and ovarian cancer immunotherapy.

The porcine circovirus type 1 capsid gene promoter improves antigen expression and immunogenicity in a HIV-1 plasmid vaccine

Background. One of the promising avenues for development of vaccines against Human immunodeficiency virus type 1 (HIV-1) and other human pathogens is the use of plasmid-based DNA vaccines. However, relatively large doses of plasmid must be injected for a relatively weak response. We investigated whether genome elements from Porcine circovirus type 1 (PCV-1), an apathogenic small ssDNA-containing virus, had useful expression-enhancing properties that could allow dose-sparing in a plasmid vaccine. Results. The linearised PCV-1 genome inserted 5' of the CMV promoter in the well-characterised HIV-1 plasmid vaccine pTHgrttnC increased expression of the polyantigen up to 2-fold, and elicited 3-fold higher CTL responses in mice at 10-fold lower doses than unmodified pTHgrttnC. The PCV-1 capsid gene promoter (Pcap) alone was equally effective. Enhancing activity was traced to a putative composite host transcription factor binding site and a "Conserved Late Element" transcription-enhancing sequence previously unidentified in circoviruses. Conclusions. We identified a novel PCV-1 genome-derived enhancer sequence that significantly increased antigen expression from plasmids in in vitro assays, and improved immunogenicity in mice of the HIV-1 subtype C vaccine plasmid, pTHgrttnC. This should allow significant dose sparing of, or increased responses to, this and other plasmid-based vaccines. We also report investigations of the potential of other circovirus-derived sequences to be similarly used. © 2011 Tanzer et al; licensee BioMed Central Ltd.

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

Analysis of two authorization protocols using Colored Petri Nets

To prevent unauthorized access to protected trusted platform module (TPM) objects, authorization protocols, such as the object-specific authorization protocol (OSAP), have been introduced by the trusted computing group (TCG). By using OSAP, processes trying to gain access to the protected TPM objects need to prove their knowledge of relevant authorization data before access to the objects can be granted. Chen and Ryan’s 2009 analysis has demonstrated OSAP’s authentication vulnerability in sessions with shared authorization data. They also proposed the Session Key Authorization Protocol (SKAP) with fewer stages as an alternative to OSAP. Chen and Ryan’s analysis of SKAP using ProVerif proves the authentication property. The purpose of this paper was to examine the usefulness of Colored Petri Nets (CPN) and CPN Tools for security analysis. Using OSAP and SKAP as case studies, we construct intruder and authentication property models in CPN. CPN Tools is used to verify the authentication property using a Dolev–Yao-based model. Verification of the authentication property in both models using the state space tool produces results consistent with those of Chen and Ryan.

Visualization of complex biological systems: An immune response model using OpenGL

In this paper we present an update on our novel visualization technologies based on cellular immune interaction from both large-scale spatial and temporal perspectives. We do so with a primary motive: to present a visually and behaviourally realistic environment to the community of experimental biologists and physicians such that their knowledge and expertise may be more readily integrated into the model creation and calibration process. Visualization aids understanding as we rely on visual perception to make crucial decisions. For example, with our initial model, we can visualize the dynamics of an idealized lymphatic compartment, with antigen presenting cells (APC) and cytotoxic T lymphocyte (CTL) cells. The visualization technology presented here offers the researcher the ability to start, pause, zoom-in, zoom-out and navigate in 3-dimensions through an idealised lymphatic compartment.

'Take away from the dry sixties style marking': Lecturer and student perceptions and experiences of audio feedback

Providing audio feedback to assessment is relatively uncommon in higher education. However, published research suggests that it is preferred over written feedback by students but lecturers were less convinced. The aim of this paper is to examine further these findings in the context of a third year business ethics unit. Data was collected from two sources. The first is a series of in-depth, semi-structured interviews conducted with three lecturers providing audio feeback for the first time in Semester One 2011. The second source of data was drawn from the university student evaluation system. A total of 363 responses were used providing 'before' and 'after' perspectives about the effectiveness of audio feedback versus written feedback. Between 2005 and 2009 the survey data provided information about student attitudes to written assessment feedback (n=261). From 2010 onwards the data relates to audio (mp3) feedback (n=102). The analysis of he interview data indicated that introducing audio feedback should be done with care. The perception of the participating lecturers was mixed, ranging from sceptism to outright enthusiasm, but over time the overall approach became positive. It was found that particular attention needs to be paid to small (but important) technical details, and lecturers need to be convinced of its effectieness, especially that it is not necessarily more time consuming than providing written feedback. For students, the analysis revealed a clear preference for audio feedback. It is concluded that there is cause for concern and reason for optimism. It is a cause for concern because there is a possibility that scepticism on the part of academic staff seems to be based on assumptions about what students prefer and a concern about using the technology. There is reason for optimism because the evidence points towards students preferring audio feedback and as academic staff become more familiar with the technology the scepticism tends to evaporate. While this study is limited in scope, questions are raised about tackling negative staff perceptions of audio feedback that are worthy of further research.