Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol

• Autorzy: Kacprzak M. , Lomuscio A. , Niewiadomski A. , Penczek W. , Raimondi F. , Szreter M.
• Języki publikacji: EN

Abstrakty

EN

We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.

Słowa kluczowe

EN

verification; Dining Cryptographers Protocol; bounded model checking; binary decision diagrams; SAT solver

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 72, nr 1-3
• Strony: 215--234
• Opis fizyczny: tab., wykr., bibliogr. 25 poz.

Twórcy

autor

Kacprzak M.

autor

Lomuscio A.

autor

Niewiadomski A.

autor

Penczek W.

autor

Raimondi F.

autor

Szreter M.

• Institute of Mathematics Technical University of Białystok ul. Wiejska 45A, 15-351 Białystok, Poland

Bibliografia

• [1] Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs, Proc. of the 11th Int. Conf. on Computer Aided Verification (CAV'99), 1633, Springer-Verlag, 1999.
• [2] Bryant, R. E.: Graph-Based Algorithms for Boolean FunctionManipulation, IEEE Transactions on Computers, 35(8), August 1986, 677-691.
• [3] Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., Hwang, L. J.: Symbolic Model Checking: 1020 States and Beyond, Information and Computation, 98(2), June 1992, 142-170.
• [4] Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability, Journal of Cryptology, 1(1), 1988, 65-75.
• [5] Clarke, E. M., Grumberg, O., Peled, D.: Model Checking, MIT Press, 1999.
• [6] Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Wo´zna, B., Zbrzezny, A.: VerICS: A Tool for Verifying Timed Automata and Estelle Specifications, Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), 2619, Springer-Verlag, 2003.
• [7] Doroś, A., Janowska, A., Janowski, P.: FromSpecification Languages to Timed Automata, Proc. of CS&P the Int. Workshop on Concurrency, Specification and Programming (CS&P'02), 161(1), Humboldt University, 2002.
• [8] Emerson, E. A., Clarke, E.M.: Using Branching-Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, 2(3), 1982, 241-266.
• [9] Fagin, R., Halpern, J. Y., Moses, Y., Vardi, M. Y.: Reasoning about Knowledge, MIT Press, Cambridge, 1995, ISBN 0-262-06162-7.
• [10] van der Hoek, W., Wooldridge, M., van Otterloo, S.: Model Checking Knowledge and Time via Local Propositions: Cooperative and Adversarial Systems, 2004, Submitted.
• [11] Huth, M. R. A., Ryan, M. D.: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, Cambridge, England, 2000, ISBN Hardback: ISBN 0-521-65200-6, Paperback: ISBN 0-521-65602-8.
• [12] Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems., Proceedings of TACAS06, Springer Verlag, March 2006, To appear.
• [13] Lomuscio, A., Sergot, M.: Deontic Interpreted Systems, Studia Logica, 75(1), 2003, 63-92.
• [14] Lomuscio, A., Sergot, M.: A formalisation of violation, error recovery, and enforcement in the bit transmission problem, Journal of Applied Logic, 2(1), March 2004, 93-116.
• [15] Lowe, G., Roscoe, A. W.: Using CSP to Detect Errors in the TMN Protocol, Software Engineering, 23(10), 1997, 659-669.
• [16] van der Meyden, R., Su, K.: Symbolic Model Checking the Knowledge of the Dining Cryptographers, 17th IEEE Computer Security FoundationsWorkshop, 2004.
• [17] W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, and M. Szreter. VerICS 2004: A model checker for real time and multi-agent systems. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04), volume 170(1) of Informatik-Berichte, pages 88-99. Humboldt University, 2004.
• [18] Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking, Proc. of the 2nd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'03), ACM, July 2003.
• [19] Penczek, W., Woźna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL, Fundamenta Informaticae, 51(1-2), 2002, 135-156.
• [20] Raimondi, F., Lomuscio, A.: MCMAS - A tool for verification of multi-agent systems, http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/.
• [21] Raimondi, F., Lomuscio, A.: Verification of multiagent systems via ordered binary decision diagrams: an algorithm and its implementation, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'04) (N. R. Jennings, C. Sierra, L. Sonenberg, M. Tambe, Eds.), II, ACM, July 2004.
• [22] Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs, Journal of Applied Logic, 2005, To appear in Special issue on Logic-based agent verification.
• [23] Visser,W., Havelund, K., Brat, G., Park, S.: Model Checking Programs, Proc. of the 15th IEEE Int. Conf. On Automated Software Engineering (ASE'00), IEEE Computer Society, 2000.
• [24] Woźna, B., Lomuscio, A., Penczek,W.: BoundedModel Checking for Deontic Interpreted Systems, Proc. Of the 2nd Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'04), 126, Elsevier, 2004.
• [25] Wożna, B., Penczek,W., Zbrzezny, A.: Reachability for Timed Systems Based on SAT-Solvers, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'02), 161(2), Humboldt University, 2002.