A Z based approach to verifying security protocols

Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism.

Formal verification of type flaw attacks in security protocols

Security protocols are often modelled at a high level of abstraction, potentially overlooking implementation-dependent vulnerabilities. Here we use the Z specification language's rich set of data structures to formally model potentially ambiguous messages that may be exploited in a 'type flaw' attack. We then show how to formally verify whether or not such an attack is actually possible in a particular protocol using Z's schema calculus.

A power system control scheme based on security visualisation in parameter space

Power system real time security assessment is one of the fundamental modules of the electricity markets. Typically, when a contingency occurs, it is required that security assessment and enhancement module shall be ready for action within about 20 minutes’ time to meet the real time requirement. The recent California black out again highlighted the importance of system security. This paper proposed an approach for power system security assessment and enhancement based on the information provided from the pre-defined system parameter space. The proposed scheme opens up an efficient way for real time security assessment and enhancement in a competitive electricity market for single contingency case

The Future of the Australian-U.S. Security Relationship

Australia is an increasingly important ally for the United States. It is willing to be part of challenging global missions, and its strong economy and growing self-confi dence suggest a more prominent role in both global and regional affairs. Moreover, its government has worked hard to strengthen the link between Canberra and Washington. Political and strategic affi nities between the two countries have been refl ected in--and complemented by--practiced military interoperability, as the two allies have sustained a pattern of security cooperation in relation to East Timor, Afghanistan and Iraq in the last 4 years. This growing collaboration between the two countries suggests that a reinvention of the traditional bilateral security relationship is taking place. At the core of this process lies an agreement about the need for engaging in more proactive strategic behavior in the changing global security environment, and a mutual acceptance of looming military and technological interdependence. But this new alliance relationship is already testing the boundaries of bipartisan support for security policy within Australia. Issues of strategic doctrine, defense planning, and procurement are becoming topics of fi erce policy debate. Such discussion is likely to be sharpened in the years ahead as Australia’s security relationship with the United States settles into a new framework.

Synchronization of estrus and fertility in zebu beef heifers treated with three estrus synchronization protocols

The effects on estrus and fertility of 3 estrus synchronization protocols were studied in Brahman beef heifers. In Treatment 1 (PGF protocol; n=234), heifers received 7.5 mg, im prostianol on Day 0 and were inseminated after observed estrus until Day 5. Treatment 2 (10-d NOR protocol; n=220) consisted of norgestomet (NOR; 3 mg, sc implant and 3 mg, im) and estradiol valerate (5 mg, im) treatment on Day -10, NOR implant removal and 400 IU, im PMSG on Day 0, and AI after observed estrus through to Day 5. Treatment 3 (14-d NOR+PGF protocol; n=168) constituted a NOR implant (3 mg, sc) on Day -14, NOR implant removal on Day 0, PGF on Day 16, and AI after observed estrus through to Day 21. All heifers were examined for return to estrus at the next cycle and inseminated after observed estrus. The heifers were then exposed to bulls for at least 21 d. During the period of estrus observation (5 d) after treatment, those heifers treated with the PGF protocol had a lower (P

Analysis of proximal femur DXA scans in growing children: Comparisons of different protocols for cross-sectional 8-month and 7-year longitudinal data

Dual-energy X-ray absorptiometry (DXA) is a widely used method for measuring bone mineral in the growing skeleton. Because scan analysis in children offers a number of challenges, we compared DXA results using six analysis methods at the total proximal femur (PF) and five methods at the femoral neck (FN), In total we assessed 50 scans (25 boys, 25 girls) from two separate studies for cross-sectional differences in bone area, bone mineral content (BMC), and areal bone mineral density (aBMD) and for percentage change over the short term (8 months) and long term (7 years). At the proximal femur for the short-term longitudinal analysis, there was an approximate 3.5% greater change in bone area and BMC when the global region of interest (ROI) was allowed to increase in size between years as compared with when the global ROI was held constant. Trend analysis showed a significant (p < 0.05) difference between scan analysis methods for bone area and BMC across 7 years. At the femoral neck, cross-sectional analysis using a narrower (from default) ROI, without change in location, resulted in a 12.9 and 12.6% smaller bone area and BMC, respectively (both p < 0.001), Changes in FN area and BMC over 8 months were significantly greater (2.3 %, p < 0.05) using a narrower FN rather than the default ROI, Similarly, the 7-year longitudinal data revealed that differences between scan analysis methods were greatest when the narrower FN ROI was maintained across all years (p < 0.001), For aBMD there were no significant differences in group means between analysis methods at either the PF or FN, Our findings show the need to standardize the analysis of proximal femur DXA scans in growing children.

Assessment of image quality of a standard and two dose-reducing protocols in paediatric pelvic CT

Background: Concerns exist regarding the effect of radiation dose from paediatric pelvic CT scans and the potential later risk of radiation-induced neoplasm and teratogenic outcomes in these patients. Objective: To assess the diagnostic quality of CT images of the paediatric pelvis using either reduced mAs or increased pitch compared with standard settings. Materials and methods: A prospective study of pelvic CT scans of 105 paediatric patients was performed using one of three protocols: (1) 31 at a standard protocol of 200 mA with rotation time of 0.75 s at 120 kVp and a pitch factor approximating 1.4; (2) 31 at increased pitch factor approaching 2 and 200 mA; and (3) 43 at a reduced setting of 100 mA and a pitch factor of 1.4. All other settings remained the same in all three groups. Image quality was assessed by radiologists blinded to the protocol used in each scan. Results: No significant difference was found between the quality of images acquired at standard settings and those acquired at half the standard mAs. The use of increased pitch factor resulted in a higher proportion of poor images. Conclusions: Images acquired at 120 kVp using 75 mAs are equivalent in diagnostic quality to those acquired at 150 mAs. Reduced settings can provide useful imaging of the paediatric pelvis and should be considered as a standard protocol in these situations.

Privacy and security enhanced offline oblivious transfer for massive data distribution

Unauthorized accesses to digital contents are serious threats to international security and informatics. We propose an offline oblivious data distribution framework that preserves the sender's security and the receiver's privacy using tamper-proof smart cards. This framework provides persistent content protections from digital piracy and promises private content consumption.