Security Protocol Verification and Optimization by Epistemic Model Checking
Final rept. 25 Aug 2009-25 Aug 2010
NEW SOUTH WALES UNIV (AUSTRALIA)
Pagination or Media Count:
When a distributed systems protocol is used in a particular context as part of a solution to a larger problem, additional information may be generated from the context. Such information may be used for optimization of the system, and, in the case of security protocols, may be of use to the adversary for attacks. The project conducted a case study of the application of the epistemic model checker MCK to automatically detect such optimization opportunities, and to verify that the protocol remains secure in the mode of use. The particular protocol studied was Chaums Dining Cryptographers protocol, a security protocol that allows a single agent to anonymously transmit a signal. The context of use considered was a more general 2-phase protocol for anonymous broadcast by an arbitrary number of agents, also proposed by Chaum. The aims of the 2-phase anonymous broadcast protocol were formulated as a knowledge-based program, and an iterative process of model checking and manual counter-example guided refinement was followed to converge on implementations of this knowledge-based program in which local predicates were identified that correspond precisely to the knowledge conditions in the knowledge-based program. This analysis demonstrated that the 2-phase protocol contains some quite subtle flows of information that can be used to optimize its performance, but no violation of the anonymity property was found. As an additional contribution of the research, a formal abstraction technique was developed, and proved correct, for epistemic model checking of protocols that call the Dining Cryptographers protocol as a subroutine. Experimental results show that the optimization improves epistemic model checking performance by orders of magnitude and enables problems of larger scale to be attacked.
- Computer Systems Management and Standards
- Radio Communications