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.     

Fabrication, microstructure, and mechanical properties of tin nanostructures

Vertically aligned, cylindrical tin nanopillars have been fabricated via an electron beam lithography and electroplating method. Characterization by a non-destructive synchrotron X-ray microdiffraction (μSXRD) technique revealed that the tin nanostructures are body-centered tetragonal and are likely single-crystalline, or consist of a few large grains. The mechanical properties of tin nanopillars with average diameters of 920 nm, 560 nm, and 350 nm were studied by uniaxial compression in a nanoindenter outfitted with a flat punch diamond tip. The results of compression tests reveal strain rate sensitivity for nanoscale tin deformation, which matches closely to the previously reported bulk tin values. However, unlike bulk, tin nanopillars exhibit size-dependent flow stresses where smaller diameter specimens exhibit greater attained strengths. The observed size-dependence matches closely to that previously reported for single-crystalline face centered cubic metals at the nanoscale. μSXRD data was used to compare the dislocation density between as-fabricated and deformed tin nanopillars. Results of this comparison suggest that there is no measurable accumulation of dislocations within deformed tin nanopillars.     

Fabrication,structure and mechanical properties of indium nanopillars

Solid and hollow cylindrical indium pillars with nanoscale diameters were prepared using electron beam lithography followed by the electroplating fabrication method. The microstructure of the solid-core indium pillars was characterized by scanning micro-X-ray diffraction, which shows that the indium pillars were annealed at room temperature with very few dislocations remaining in the samples. The mechanical properties of the solid pillars were characterized using a uniaxial microcompression technique, which demonstrated that the engineering yield stress is ～9 times greater than bulk and is ～1/28 of the indium shear modulus, suggesting that the attained stresses are close to theoretical strength. Microcompression of hollow indium nanopillars showed evidence of brittle fracture. This may suggest that the failure mode for one of the most ductile metals can become brittle when the feature size is sufficiently small.     

Turning event logs into process movies: animating what has really happened

Today’s information systems log vast amounts of data. These collections of data (implicitly) describe events (e.g. placing an order or taking a blood test) and, hence, provide information on the actual execution of business processes. The analysis of such data provides an excellent starting point for business process improvement. This is the realm of process mining, an area which has provided a repertoire of many analysis techniques. Despite the impressive capabilities of existing process mining algorithms, dealing with the abundance of data recorded by contemporary systems and devices remains a challenge. Of particular importance is the capability to guide the meaningful interpretation of “oceans of data” by process analysts. To this end, insights from the field of visual analytics can be leveraged. This article proposes an approach where process states are reconstructed from event logs and visualised in succession, leading to an animated history of a process. This approach is customisable in how a process state, partially defined through a collection of activity instances, is visualised: one can select a map and specify a projection of events on this map based on the properties of the events. This paper describes a comprehensive implementation of the proposal. It was realised using the open-source process mining framework ProM. Moreover, this paper also reports on an evaluation of the approach conducted with Suncorp, one of Australia’s largest insurance companies.     

A user-centric federated single sign-on system

Current identity management systems are not concerned with user privacy. Users must assume that identity providers and service providers will ensure their privacy, which is not always the case. This paper proposes an extension of the existing federated single sign-on (FSSO) systems that adopts the beneficial properties of the user-centric identity management (UCIM) model. This new identity management system allows the users to control and enforce their privacy requirements while still retaining the convenience of single sign-on over a federation of service providers. Colored Petri Nets are used to formally model the new identity management system to provide assurance that the privacy goals are achieved. To our knowledge, Colored Petri Nets have not been used to model privacy in identity management systems before.