An Extension of CryptoPAi to the Formal Analysis of E-voting Protocols

Document Type : Research Article

Authors

1 Computer Group, International University of Imamreza

2 Sharif University of Technology, Computer Engineering Department

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 of
more 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

References

[1] Gavin Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(1-2):53--84, 1998. [ bib | DOI ]
[2] C. Caleiroa, L. Viganò  , and D. Basin. On the semantics of Alice & Bob specifications of security protocols. Theoretical Computer Science, 367(1-2):88--122, 2006. [ bib | DOI ]
[3] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM (JACM), 31(3):560--599, 1984. [ bib | DOI ]
[4] R. Milner. A calculus of communicating systems. In Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 1980. [ bib | DOI ]
[5] M. Abadi and A. D.Gordon. A calculus for cryptographic protocols: The spi calculus. Information and computation, 148(1):1--70, 1999. [ bib | DOI ]
[6] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. [ bib ]
[7] D. Hughes and V. Shmatikov. Information hiding, anonymity and privacy: A modular approach. Journal of Computer Security, 12(1):3--36, 2004. [ bib | DOI ]
[8] F. Dechesne and Y. Wang. To know or not to know: epistemic approaches to security protocol verification. Synthese, 177(1):51--76, 2010. [ bib | DOI ]
[9] A. Hommersom, J.-J. Meyer, and E.P. de Vink. Update semantics of security protocols. Synthese, 142(2):229--267, 2004. [ bib | DOI ]
[10] A. Baltag and M. Sadrzadeh. The algebra of multi-agent dynamic belief revision. Electronic Notes in Theoretical Computer Science, 157(4):37 -- 56, 2006. [ bib | DOI ]
[11] Simon Kramer. Cryptographic protocol logic: Satisfaction for (timed) dolev-yao cryptography. The Journal of Logic and Algebraic Programming, 77(1-2):60--91, 2008. [ bib | DOI ]
[12] S. Richards and M. Sadrzadeh. Aximo: Automated axiomatic reasoning for information update. Electronic Notes in Theoretical Computer Science, 231:211--225, 2009. [ bib | DOI ]
[13] Yanjing Wang. Epistemic Modeling and Protocol Dynamics. PhD thesis, University of Amsterdam, 2010. [ bib ]
[14] R. Chadha, S. Delaune, and S. Kremer. Epistemic logic for the applied pi calculus. In International Conference on Formal Methods for Open Object-Based Distributed Systems, pages 182--197. Springer, Berlin, Heidelberg, 2009. [ bib | DOI ]
[15] S. Kramer, C. Palamidessi, R. Segala, A. Turrini, and C. Braun. A quantitative doxastic logic for probabilistic processes and applications to information-hiding. The Journal of Applied Non-Classical Logic, 19(4):489--516, 2009. [ bib | DOI ]
[16] R. Milner. A spatial-epistemic logic for reasoning about security protocols. In International Workshop on Security Issues in Concurrency (SecCo), 2010. [ bib | DOI ]
[17] H. R. Mahrooghi and M. R.Mousavi. Reconciling operational and epistemic approaches to the formal analysis of crypto-based security protocols. In Proceedings of the 9th International Workshop on Security Issues in Concurrency, 2011. [ bib ]
[18] M. Abadi and J. Jürjens. Formal eavesdropping and its computational interpretation. In International Symposium on Theoretical Aspects of Computer Software, pages 82--94. Springer, Berlin, Heidelberg, 2001. [ bib | DOI ]
[19] L. Peeter and R. Corin. Sound computational interpretation of formal encryption with composed keys. In International Conference on Information Security and Cryptology, pages 55--66. Springer, Berlin, Heidelberg, 2003. [ bib | DOI ]
[20] M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of cryptology, 15(12):103--127, 2002. [ bib | DOI ]
[21] Tomohiro Hoshi. Epistemic Modeling and Protocol Information. PhD thesis, Stanford University, 2009. [ bib ]
[22] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137--161, 1985. [ bib | DOI ]
[23] F. Raimondi and A. Lomuscio. Automatic verification of deontic interpreted systems by model checking via OBDD's. Journal of Applied Logic, 5(2):235--251, 2006. [ bib | DOI ]
[24] J. Y. Halpern and K. R. O'Neill. Anonymity and information hiding in multiagent systems. Journal of Computer Security, 13(3):483--514, 2005. [ bib | DOI ]
[25] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001), pages 104--115. ACM, 2001. [ bib | DOI ]
[26] J. v. Eijck and S. Orzan. Epistemic verification of anonymity. In Proceedings VODCA'06, 2006. [ bib ]
[27] P.J. Broadfoot. Data Independence in the Model Checking of Security Protocols. PhD thesis, Oxford University, 2001. [ bib ]
[28] F. Dechesne, M. R. Mousavi, and S. Orzan. Operational and epistemic approaches to protocol analysis: bridging the gap. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 226--241. Springer, Berlin, Heidelberg, 2007. [ bib | DOI ]
[29] G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Progamming, pages 17--139, 2004. [ bib | DOI ]
[30] A. Fujioka, T. Okamoto, and K. Ohta. A practical secret voting scheme for large scale elections. In International Workshop on the Theory and Application of Cryptographic Techniques, pages 244--251. Springer, Berlin, Heidelberg, 1992. [ bib | DOI ]
[31] S. Delaune, S. Kremer, and M. Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 17(4):435--487, 2009. [ bib | DOI ]
[32] H. R. Mahrooghi, M. H. Haghighat, and R. Jalili. Formal verification of authentication-type properties of an electronic voting protocol using mcrl2. In Proceedings of the Fourth international conference on Verification and Evaluation of Computer and Communication Systems. eWiC, 2010. [ bib | DOI ]
[33] J. v. Eijck and S. Orzan. Epistemic verification of anonymity. Electronic Notes in Theoretical Computer Science, 168:159--174, 2007. [ bib | DOI ]
[34] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Springer, 2007. [ bib ]
[35] A. Baskar, R. Ramanujam, and S. P. Suresh. Knowledge-based modelling of voting protocols. In Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-2007), pages 62--71. ACM, 2007. [ bib | DOI ]
Journal of Computing and Security
Volume 6, Issue 1
January 2019
Pages 25-42

Files

History

  • Receive Date: 16 October 2018
  • Revise Date: 04 August 2019
  • Accept Date: 09 October 2019

Share

How to cite

Statistics