Compilation Method for the Verification of Temporal-Epistemic Properties of Cryptographic Protocols
作者： Alessio Lomuscio , Ioana Cristina Boureanu , Mika Cohen
DOI:
关键词: Model checking 、 Programming language 、 Specification language 、 Compiler 、 Authentication 、 Epistemology 、 Cryptographic protocol 、 Computer science 、 Input language 、 Theoretical computer science 、 Secrecy 、 State space
摘要: We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. Our work is based on model checking multi-agent systems against properties given AI logics. PC2IS, compiler from CAPSL to ISPL, input of MCMAS, symbolic checker MAS. The also reduces state space be considered by checker, thereby maximising number and sessions that can verified. evaluate Clark-Jacobs library custom secrecy authentication requirements as well more advanced are expressible this epistemic-based approach.
参考文章(24)
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
Paul F. Syverson, Stuart G. Stubblebine, Group Principals and the Formalization of Anonymity formal methods. pp. 814- 833 ,(1999) , 10.1007/3-540-48119-2_45
Alessio Lomuscio, Wojciech Penczek, LDYIS: a Framework for Model Checking Security Protocols Fundamenta Informaticae. ,vol. 85, pp. 359- 375 ,(2008)
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
Gavin Lowe, A Family of Attacks upon Authentication Protocols ,(1997)
Dominic Hughes, Vitaly Shmatikov, Information hiding, anonymity and privacy: a modular approach Journal of Computer Security. ,vol. 12, pp. 3- 36 ,(2004) , 10.3233/JCS-2004-12102
Xiao De-qin, Zhang Huan-guo, Model checking electronic commerce security protocols based on CTL Wuhan University Journal of Natural Sciences. ,vol. 10, pp. 333- 337 ,(2005) , 10.1007/BF02828681
Michael Burrows, Martin Abadi, Roger Needham, A logic of authentication ACM Transactions on Computer Systems. ,vol. 8, pp. 18- 36 ,(1990) , 10.1145/77648.77649
Alessio Lomuscio, Franco Raimondi, MCMAS: a model checker for multi-agent systems tools and algorithms for construction and analysis of systems. pp. 450- 454 ,(2006) , 10.1007/11691372_31
D. Dolev, A. Yao, On the security of public key protocols IEEE Transactions on Information Theory. ,vol. 29, pp. 198- 208 ,(1983) , 10.1109/TIT.1983.1056650