Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAbstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols
141
0
0.0
(
0
)
Added by
Omar Bataineh
Publication date
2010
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The paper describes an abstraction for protocols that are based on multiple rounds of Chaums Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.
rate research
Read More
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.
The notion of knowledge-based program introduced by Halpern and Fagin provides a useful formalism for designing, analysing, and optimising distributed systems. This paper formulates the two phase commit protocol as a knowledge-based program and then an iterative process of model checking and counter-example guided refinement is followed to find concrete implementations of the program for the case of perfect recall semantic in the Byzantine failures context with synchronous reliable communication. We model several different kinds of Byzantine failures and verify different strategies to fight and mitigate them. We address a number of questions that have not been considered in the prior literature, viz., under what circumstances a sender can know that its transmission has been successful, and under what circumstances an agent can know that the coordinator is cheating, and find concrete answers to these questions. The paper describes also a methodology based on temporal-epistemic model checking technology that can be followed to verify the shortest and longest execution time of a distributed protocol and the scenarios that lead to them.
This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, uppaalsmc relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. uppaalsmc comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.
This paper shows that conditional independence reasoning can be applied to optimize epistemic model checking, in which one verifies that a model for a number of agents operating with imperfect information satisfies a formula expressed in a modal multi-agent logic of knowledge. The optimization has been implemented in the epistemic model checker MCK. The paper reports experimental results demonstrating that it can yield multiple orders of magnitude performance improvements.
This volume contains the proceedings of the First Workshop on Logics and Model-checking for self-* systems (MOD* 2014). The worshop took place in Bertinoro, Italy, on 12th of September 2014, and was a satellite event of iFM 2014 (the 11th International Conference on Integrated Formal Methods). The workshop focuses on demonstrating the applicability of Formal Methods on modern complex systems with a high degree of self-adaptivity and reconfigurability, by bringing together researchers and practitioners with the goal of pushing forward the state of the art on logics and model checking.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
