Browse DORAS
Browse Theses
Search
Latest Additions
Creative Commons License
Except where otherwise noted, content on this site is licensed for use under a:

Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting

Butin, Denis Frédéric (2012) Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. PhD thesis, Dublin City University.

Full text available as:

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
1493Kb

Abstract

Security protocols are predefined sequences of message exchanges. Their uses over computer networks aim to provide certain guarantees to protocol participants. The sensitive nature of many applications resting on protocols encourages the use of formal methods to provide rigorous correctness proofs. This dissertation presents extensions to the Inductive Method for protocol verification in the Isabelle/HOL interactive theorem prover. The current state of the Inductive Method and of other protocol analysis techniques are reviewed. Protocol composition modelling in the Inductive Method is introduced and put in practice by holistically verifying the composition of a certification protocol with an authentication protocol. Unlike some existing approaches, we are not constrained by independence requirements or search space limitations. A special kind of identity-based signatures, auditable ones, are specified in the Inductive Method and integrated in an analysis of a recent ISO/IEC 9798-3 protocol. A side-by-side verification features both a version of the protocol with auditable identity-based signatures and a version with plain ones. The largest part of the thesis presents extensions for the verification of electronic voting protocols. Innovative specification and verification strategies are described. The crucial property of voter privacy, being the impossibility of knowing how a specific voter voted, is modelled as an unlinkability property between pieces of information. Unlinkability is then specified in the Inductive Method using novel message operators. An electronic voting protocol by Fujioka, Okamoto and Ohta is modelled in the Inductive Method. Its classic confidentiality properties are verified, followed by voter privacy. The approach is shown to be generic enough to be re-usable on other protocols while maintaining a coherent line of reasoning. We compare our work with the widespread process equivalence model and examine respective strengths.

Item Type:Thesis (PhD)
Date of Award:November 2012
Refereed:No
Supervisor(s):Gray, David
Uncontrolled Keywords:Security Protocols; Formal Methods; Correctness Proofs
Subjects:Computer Science > Computer networks
Computer Science > Computer security
DCU Faculties and Centres:DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing
Use License:This item is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 3.0 License. View License
Funders:SFI
ID Code:17459
Deposited On:15 Nov 2012 11:05 by David Gray. Last Modified 16 Nov 2012 10:50

Download statistics

Archive Staff Only: edit this record