Analysis of Object-Specific Authorization Protocol (OSAP) using coloured Petri nets

The use of Trusted Platform Module (TPM) is be- coming increasingly popular in many security sys- tems. To access objects protected by TPM (such as cryptographic keys), several cryptographic proto- cols, such as the Object Specific Authorization Pro- tocol (OSAP), can be used. Given the sensitivity and the importance of those objects protected by TPM, the security of this protocol is vital. Formal meth- ods allow a precise and complete analysis of crypto- graphic protocols such that their security properties can be asserted with high assurance. Unfortunately, formal verification of these protocols are limited, de- spite the abundance of formal tools that one can use. In this paper, we demonstrate the use of Coloured Petri Nets (CPN) - a type of formal technique, to formally model the OSAP. Using this model, we then verify the authentication property of this protocol us- ing the state space analysis technique. The results of analysis demonstrates that as reported by Chen and Ryan the authentication property of OSAP can be violated.

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

Thermal stability and decomposition kinetics of styrene-butadiene rubber nanocomposites filled with different particle sized kaolinites

A series of styrene-butadiene rubber (SBR) nanocomposites filledwith different particle sized kaolinites are prepared via a latex blending method. The thermal stabilities of these clay polymer nanocomposites (CPN) are characterized by a range of techniques including thermogravimetry (TG), digital photos, scanning electron microscopy (SEM) and Raman spectroscopy. These CPN show some remarkable improvement in thermal stability compared to that of the pure SBR. With the increase of kaolinite particle size, the residual char content and the average activation energy of kaolinite SBR nanocomposites all decrease; the pyrolysis residues become porous; the crystal carbon in the pyrolysis residues decrease significantly from 58.23% to 44.41%. The above results prove that the increase of kaolinite particle size is not beneficial in improving the thermal stability of kaolinite SBR nanocomposites.

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.

Synthesis of organoclays: A critical review and some unresolved issues

The synthesis of organoclays (OC) by intercalation of quaternary ammonium cation (QAC) into expanding clay minerals, notably montmorillonite (Mt), has attracted a great deal of attention during the past two decades. The OC have also found applications in the manufacture of clay polymer nanocomposites (CPN) and environmental remediation. Despite the wealth of information that exists on the formation and properties of OC, some problems remain to be resolved. The present contribution is an attempt at clarifying two outstanding issues, based on the literature and experimental data obtained by the authors over the past years. The first issue concerns the relationship between the cation exchange capacity (CEC) of the Mt and the basal spacing of the OC which, in turn, is dependent on the concentration and the nature of the added QAC. At a concentration less than 1 CEC, organo-Mt (OMt) formed using the QAC with a short alkyl chain length with nc < 16 (e.g., dodecyl trimethylammonium) gives basal spacings of 1.4–1.6 nm that are essentially independent of the CEC. However, for long-chain QAC with nc ≥ 16 (e.g., hexadecyl trimethylammonium), the basal spacing varies with the QAC concentration. For Mt with a CEC of 80–90 meq/100 g, the basal spacing of the OC increases gradually with the CEC and shows a sudden (stepwise) increase to 3.2–3.8 nm at a QAC concentration of 1.5 CEC and to 3.5–4.0 nm at a concentration of 2.0 CEC. The second issue pertains to the “locking” effect in QAC- and silane-modified pillared interlayered clays (PILC) and Mt. For silylated Mt, the “locking” effect results from the covalent bonding of silane to two adjacent layers within a single clay mineral particle. The same mechanism can operate in silane-grafted PILC but in this case, the “locking” effect may primarily be ascribed to the pillaring of adjacent basal surfaces by metal hydr(oxides).

Formal modelling and analysis of DNP3 secure authentication

Supervisory Control and Data Acquisition (SCADA) systems are one of the key foundations of smart grids. The Distributed Network Protocol version 3 (DNP3) is a standard SCADA protocol designed to facilitate communications in substations and smart grid nodes. The protocol is embedded with a security mechanism called Secure Authentication (DNP3-SA). This mechanism ensures that end-to-end communication security is provided in substations. This paper presents a formal model for the behavioural analysis of DNP3-SA using Coloured Petri Nets (CPN). Our DNP3-SA CPN model is capable of testing and verifying various attack scenarios: modification, replay and spoofing, combined complex attack and mitigation strategies. Using the model has revealed a previously unidentified flaw in the DNP3-SA protocol that can be exploited by an attacker that has access to the network interconnecting DNP3 devices. An attacker can launch a successful attack on an outstation without possessing the pre-shared keys by replaying a previously authenticated command with arbitrary parameters. We propose an update to the DNP3-SA protocol that removes the flaw and prevents such attacks. The update is validated and verified using our CPN model proving the effectiveness of the model and importance of the formal protocol analysis.

Formal security analysis of the DNP3-secure authentication protocol

This thesis evaluates the security of Supervisory Control and Data Acquisition (SCADA) systems, which are one of the key foundations of many critical infrastructures. Specifically, it examines one of the standardised SCADA protocols called the Distributed Network Protocol Version 3, which attempts to provide a security mechanism to ensure that messages transmitted between devices, are adequately secured from rogue applications. To achieve this, the thesis applies formal methods from theoretical computer science to formally analyse the correctness of the protocol.

Manifolds with nonnegative isotropic curvature

We prove that if (M-n, g), n >= 4, is a compact, orientable, locally irreducible Riemannian manifold with nonnegative isotropic curvature,then one of the following possibilities hold: (i) M admits a metric with positive isotropic curvature. (ii) (M, g) is isometric to a locally symmetric space. (iii) (M, g) is Kahler and biholomorphic to CPn/2. (iv) (M, g) is quaternionic-Kahler. This is implied by the following result: Let (M-2n, g) be a compact, locally irreducible Kahler manifold with nonnegative isotropic curvature. Then either M is biholomorphic to CPn or isometric to a compact Hermitian symmetric space. This answers a question of Micallef and Wang in the affirmative. The proof is based on the recent work of Brendle and Schoen on the Ricci flow.

Coloured Petri net models for automated manufacturing systems

In this paper, we propose an approach, using Coloured Petri Nets (CPN) for modelling flexible manufacturing systems. We illustrate our methodology for a Flexible Manufacturing Cell (FMC) with three machines and three robots. We also consider the analysis of the FMC for deadlocks using the invariant analysis of CPNs.

Precisiones nomenclaturales sobre asociaciones iberolevantinas de Limonietalia y Salsolo-Peganetalia

Se proponen los siguientes nombres corregidos de acuerdo con el Art. 43 del CPN: Limonietum latebracteati y Frankenio thym¡foliae-Limonietum latebracteati y se discute la nomenclatura de las asociaciones Salsolo-Peganetum harmalae y Salsolo-Antemisietum herbae-albae,

Index of the Phytosociological Nomenclature Section of Lazaroa (1989-1997)

Se presenta un índice nomenclatural  de los artículos publicados en la Sección de Nomenclatura Fitosociológica desde 1989 hasta 1997. Se adjunta una relación completa de los sintaxones citados en la misma, con la referencia de la página de la revista en que se han tratado; la relación incluye autoría de los nombres, situación nomenclatural, artículos del CPN aplicados e indicación de las referencias bibliográficas de la diagnosis original o de las informaciones sobre tipoficación aportadas.

6. Consideraciones nomenclaturales y sistemáticas en el orden "Ammophiletalia" Br.-BI. 1933

La primera propuesta de sistematización fitosociológica, a nivel de alianza, de las comunidades vegetales de las dunas litorales de las costas europeas, fue la de Braun-Blanquet (Jahrb. St. Gallischen Naturwiss. Ges. 57(2): 346. 1921); allí se describe la alianza Ammophilion para incluir dos asociaciones: “Ammophila-Medicago mnarina-Assoziation” y “Crucianelletum”. La primera es el holotipo de la alianza (CEN, Art. 18), puesto que la segunda no fue válidamente publicada (CPN, Art. 7). Posteriormente el mismo autor (Braun-Blanquet, Prodr. Groupements Vég. 1: 5. 1933) describe el orden Ammophiletalia para incluir las alianzas Ammophilion (holotipo del orden) y Ononidion angustissimae all. prov.

Structures quantiques de certaines sous-variétés lagrangiennes non-monotones

Soit (M,ω) un variété symplectique fermée et connexe.On considère des sous-variétés lagrangiennes α : L → (M,ω). Si α est monotone, c.- à-d. s’il existe η > 0 tel que ημ = ω, Paul Biran et Octav Conea ont défini une version relative de l’homologie quantique. Dans ce contexte ils ont déformé l’opérateur de bord du complexe de Morse ainsi que le produit d’intersection à l’aide de disques pseudo-holomorphes. On note (QH(L), ∗), l’homologie quantique de L munie du produit quantique. Le principal objectif de cette dissertation est de généraliser leur construction à un classe plus large d’espaces. Plus précisément on considère soit des sous-variétés presque monotone, c.-à-d. α est C1-proche d’un plongement lagrangian monotone ; soit les fibres toriques de variétés toriques Fano. Dans ces cas non nécessairement monotones, QH(L) va dépendre de certains choix, mais cela sera irrelevant pour les applications présentées ici. Dans le cas presque monotone, on s’intéresse principalement à des questions de déplaçabilité, d’uniréglage et d’estimation d’énergie de difféomorphismes hamiltoniens. Enfin nous terminons par une application combinant les deux approches, concernant la dynamique d’un hamiltonien déplaçant toutes les fibres toriques non-monotones dans CPn.

Évaluation de la performance des structures des soins de santé primaires du district sanitaire de Labé (Guinée)

Contexte : En République de Guinée, depuis 1984, l’ensemble des structures de soins ont intégré le programme de Soins de santé primaires et Médicaments Essentiels (PEV/SSP/ME). Pour la réalisation de ce programme, d’importants efforts et des sommes des millions de dollars ont été investis, mais les indicateurs de santé du pays sont toujours des plus alarmants du monde (EDS- 2005). Objectif : Evaluer la performance des structures de soins de santé primaires (SSP) d’un district sanitaire guinéen à partir des documents administratifs suivi d’une enquête sur la satisfaction des prestataires et des bénéficiaires et des parties prenantes du district. Méthodologie : Il s’agit d’une étude descriptive de cas touchant 10 des 18 structures de soins de santé primaires du district sanitaire de Labé. Elle porte sur une analyse quantitative de résultats de 10 contrôles semestriels (2004-2009) et sur une analyse qualitative composée d’entretiens menés auprès de 308 bénéficiaires et de quelques membres des Comités de gestion des structures pour apprécier le niveau de performance des structures ciblées. Résultats : Toutes les structures publiques du district sanitaire sous étude étaient intégrées1. Malgré cela, la tendance moyenne des consultations affiche une allure sinusoïdale (fluctuante). Bien que la disponibilité, l’accessibilité, l’utilisation et la couverture adéquate et effective des services de Consultation Primaire Curative (CPC) et de Planification Familiale (PF) n’ont pas connu d’amélioration durant la période de 2004 à 2009. La tendance moyenne de la Consultation prénatale (CPN) et celle de la Vaccination (VA) se sont améliorées au cours de la période d’étude. Les prestataires de services SSP déclarent être assez satisfaits de leur formation mais ne le sont pas pour leur condition de travail surtout ceux du milieu rural (faible rémunération, environnement difficile), qualité moindre de la supervision et ruptures fréquentes de stock en médicaments essentiels. Pour les bénéficiaires, leur satisfaction se limite au respect de leurs valeurs culturelles et de leur interaction avec les prestataires de soins. Cependant, ils déplorent le long temps d’attente, la mauvaise qualité de l’accueil, les coûts élevés des prestations et le manque d’équité qui sont des facteurs qualifiés comme des éléments de contreperformance des structures. Pour les autorités et des parties prenantes, la rupture des stocks en médicaments essentiels, le manque d’équipements et la faible motivation des prestataires sont les facteurs majeurs qui entravent la performance des structures sanitaires, surtout en milieu rural. Conclusion : Malgré l’intégration du programme des SSP dans les structures de SSP du district sanitaire de Labé, on note encore une insuffisance de leur utilisation, la faiblesse de la couverture, le manque de suivi et supervision des structures Une étude actualisée et plus étendue pourrait mieux cerner le sujet.