An Extension of CryptoPAi to the Formal Analysis of E-voting Protocols
Publish place: Journal of Computing and Security، Vol: 6، Issue: 1
Publish Year: 1398
نوع سند: مقاله ژورنالی
زبان: English
View: 207
This Paper With 18 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_JCSE-6-1_004
تاریخ نمایه سازی: 19 بهمن 1399
Abstract:
CryptoPAi is a hybrid operational-epistemic framework for specification and analysis of security protocols with genuine support for cryptographic constructs. This framework includes a process algebraic formalism for the operational specification and an epistemic extension of modal mu-calculus with past for the property specification. In this paper, we extend CryptoPAi framework with more cryptographic constructs. The main practical motivation for this work came from the domain of e-voting protocols and then we investigate the applicability of the extended framework in this domain. The framework provides explicit support for cryptographic constructs, which is among the most essential ingredients of security and e-voting protocols. Some more advanced cryptographic constructs are provided to allow specifying the behavior ofmore protocols in our process language and then verifying properties expressed in our logic with both temporal and epistemic operators.We apply our extended framework to the FOO e-voting protocol. We also promote the prototype model-checker of the framework in the Maude rewriting logic tool and apply it to model-check some specified properties on their corresponding models.
Keywords:
Authors
Hamid Reza Mahrooghi
Computer Group, International University of Imamreza
Rasool Jalili
Sharif University of Technology, Computer Engineering Department
مراجع و منابع این Paper:
لیست زیر مراجع و منابع استفاده شده در این Paper را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود Paper لینک شده اند :