Technical reports
Verification of security protocols based on multicast communication
March 2012, 150 pages
This technical report is based on a dissertation submitted February 2011 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare College.
DOI: 10.48456/tr-816
Abstract
Over an insecure network, agents need means to communicate securely. These means are often called security protocols. Security protocols, although constructed through the arrangement of simple security blocks, normally yield complex goals. They seem simple at a first glance, but hide subtleties that allow them to be exploited.
One way of trying to systematically capture such subtleties is through the use of formal methods. The maturity of some methods for protocol verification is a fact today. But these methods are still not able to capture the whole set of security protocols being designed. With the convergence to an online world, new security goals are proposed and new protocols need to be designed. The evolution of formal verification methods becomes a necessity to keep pace with this ongoing development.
This thesis covers the Inductive Method and its extensions. The Inductive Method is a formalism to specify and verify security protocols based on structural induction and higher-order logic proofs. This account of our extensions enables the Inductive Method to reason about non-Unicast communication and threshold cryptography.
We developed a new set of theories capable of representing the entire set of known message casting frameworks. Our theories enable the Inductive Method to reason about a whole new set of protocols. We also specified a basic abstraction of threshold cryptography as a way of proving the extensibility of the method to new cryptographic primitives. We showed the feasibility of our specifications by revisiting a classic protocol, now verified under our framework. Secrecy verification under a mixed environment of Multicast and Unicast was also done for a Byzantine security protocol.
Full text
PDF (1.1 MB)
BibTeX record
@TechReport{UCAM-CL-TR-816,
author = {Martina, Jean E.},
title = {{Verification of security protocols based on multicast
communication}},
year = 2012,
month = mar,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-816.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-816},
number = {UCAM-CL-TR-816}
}