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

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