Abstraction for epistemic model checking of dining cryptographers-based protocols
作者： Omar Al Bataineh , Ron van der Meyden
关键词:
摘要: The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved the preserves a rich class specifications in logic knowledge. This result applied to optimize model checking implementations knowledge-based program uses protocol as primitive anonymous broadcast system. Performance results given concrete and abstract models this protocol, some new conclusions about derived.
core.ac.uk
acm.org
arxiv.org
unsw.edu.au 
sci-hub.se 参考文章(25)
Xiangyu Luo, Kaile Su, Ming Gu, Lijun Wu, Jinji Yang, Symbolic model checking the knowledge in Herbivore protocol MoChArt'10 Proceedings of the 6th international conference on Model checking and artificial intelligence. pp. 112- 129 ,(2010) , 10.1007/978-3-642-20674-0_8
Kai Baukus, Ron van der Meyden, A Knowledge Based Analysis of Cache Coherence international conference on formal engineering methods. pp. 99- 114 ,(2004) , 10.1007/978-3-540-30482-1_15
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Alessio Lomuscio, Mika Cohen, Mads Dam, Francesco Russo, Abstraction in model checking multi-agent systems adaptive agents and multi agents systems. ,vol. 1, pp. 945- 952 ,(2009) , 10.25560/9294
Michael Waidner, Birgit Pfitzmann, The dining cryptographers in the disco: unconditional sender and recipient untraceability with computationally secure serviceability theory and application of cryptographic techniques. pp. 690- 690 ,(1990) , 10.1007/3-540-46885-4_69
Cynthia Dwork, Yoram Moses, Knowledge and common knowledge in a Byzantine environment I: crash failures theoretical aspects of rationality and knowledge. pp. 149- 169 ,(1986) , 10.1016/B978-0-934613-04-0.50013-2
Alessio Lomuscio, Mika Cohen, Hongyang Qu, Mads Dam, A symmetry reduction technique for model checking temporal-epistemic logic international joint conference on artificial intelligence. pp. 721- 726 ,(2009) , 10.1007/978-3-642-04761-9
Matteo Maffei, Esfandiar Mohammadi, Michael Backes, Computationally Sound Abstraction and Verification of Secure Multi-Party Computations foundations of software technology and theoretical computer science. ,vol. 8, pp. 352- 363 ,(2010) , 10.4230/LIPICS.FSTTCS.2010.352
Alessio Lomuscio, Hongyang Qu, Franco Raimondi, MCMAS: A Model Checker for the Verification of Multi-Agent Systems Computer Aided Verification. pp. 682- 688 ,(2009) , 10.1007/978-3-642-02658-4_55
Emin Sirer, Mark Robson, Sharad Goel, Milo Polte, Herbivore: A Scalable and Efficient Protocol for Anonymous Communication Cornell University. ,(2003)