ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/49899
Record Status Checked
Record Id 49899
Title A Static Analysis Framework for Security Properties in Mobile and Cryptographic Systems
Contributors
Abstract We introduce a static analysis framework for detecting instances of security breaches in infinite mobile and cryptographic systems specified using the languages of the \pi-calculus and its cryptographic extension, the spi calculus. The framework is composed from three components: First, standard denotational semantics of the \pi-calculus and the spi calculus are constructed based on domain theory. The resulting model is sound and adequate with respect to transitions in the operational semantics. The standard semantics is then extended correctly to non-uniformly capture the property of term substitution, which occurs as a result of communications and successful cryptographic operations. Finally, the non-standard semantics is abstracted to operate over finite domains so as to ensure the termination of the static analysis. The safety of the abstract semantics is proven with respect to the non-standard semantics. The results of the abstract interpretation are then used to capture breaches of the secrecy and authenticity properties in the analysed systems. Two initial prototype implementations of the security analysis for the \pi-calculus and the spi calculus are also included in the thesis. The main contributions of this thesis are summarised by the following. In the area of denotational semantics, the thesis introduces a domain-theoretic model for the spi calculus that is sound and adequate with respect to transitions in the structural operational semantics. In the area of static program analysis, the thesis utilises the denotational approach as the basis for the construction of abstract interpretations for infinite systems modelled by the pi-calculus and the spi calculus. This facilitates the use of computationally significant mathematical concepts like least fixed points and results in an analysis that is fully compositional. Also, the thesis demonstrates that the choice of the term-substitution property in mobile and cryptographic programs is rich enough to capture breaches of security properties, like process secrecy and authenticity. These properties are used to analyse a number of mobile and cryptographic protocols, like the file transfer protocol and the Needham-Schroeder, SPLICE/AS, Otway-Rees, Kerberos, Yahalom and Woo Lam authentication protocols.
Organisation CCLRC , ESC
Keywords Engineering , Security , Process Algebra , Static Analysis , Mobile Systems , Cryptography
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Thesis PhD, Dublin City University, Dublin, Ireland, 2003. thesis.pdf 2003