An Extension of Formal Analysis Method with Reasoning: A Case Study of Flaw Detection for Non-repudiation and Fairness

  • Jingchen Yan
  • Yating Wang
  • Yuichi GotoEmail author
  • Jingde Cheng
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11445)


Formal analysis is used to find out flaws of cryptographic protocols. A formal analysis method with reasoning for cryptographic protocols has been proposed. In the method, behaviors of participants and behaviors of an intruder are used as premises of forward reasoning to deduce formulas, then analysts check whether the deduced formulas are related to flaws. However, the method only can detect the flaws related to confidentiality and authentication but is unable to detect the flaws related to non-repudiation and fairness. This paper proposes an extension of the formal analysis method with reasoning, which can deal with the flaws related to non-repudiation and fairness. This paper also shows a case study of flaw detection for non-repudiation and fairness in ISI protocol with the proposed method. The result shows that the proposed method is effective to find out flaws that related to the two security properties above.


Cryptographic protocol Formal analysis method with reasoning Non-repudiation Fairness 


  1. 1.
    Asokan, N.: Fairness in electronic commerce. Ph.D. thesis, Department of Mathematics, University of Waterloo, Canada (1998)Google Scholar
  2. 2.
    Avalle, M., Alfredo, P., Bogdan, W.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26(1), 99–123 (2014)CrossRefGoogle Scholar
  3. 3.
    Bau, J., Mitchell, J.C.: Security modeling and analysis. IEEE Secur. Priv. 9(3), 18–25 (2011)CrossRefGoogle Scholar
  4. 4.
    Butterfield, A., Ngondi, G.: Oxford Dictionary of Computer Science. Oxford University Press, Oxford (2016)CrossRefGoogle Scholar
  5. 5.
    Cheng, J.: A strong relevant logic model of epistemic processes in scientific discovery. In: Information Modelling and Knowledge Bases XI, Frontiers in Artificial Intelligence and Applications, vol. 61, pp. 136–159 (2000)Google Scholar
  6. 6.
    Cheng, J., Miura, J.: Deontic relevant logic as the logical basis for specifying, verifying, and reasoning about information security and information assurance. In: 1st International Conference on Availability, Reliability and Security, pp. 601–608. IEEE Computer Society, Vienna, Austria (2006)Google Scholar
  7. 7.
    Cheng, J., Nara, S., Goto, Y.: FreeEnCal: a forward reasoning engine with general-purpose. In: Apolloni, B., Howlett, R.J., Jain, L. (eds.) KES 2007. LNCS (LNAI), vol. 4693, pp. 444–452. Springer, Heidelberg (2007). Scholar
  8. 8.
    Clarke Jr., E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  9. 9.
    Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning 46(3–4), 225–259 (2011)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Dolev, D., Andrew, C.Y.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Hauser, R., Steiner, M., Waidner, M.: Micro-payments based on IKP. IBM Zurich Research Laboratory, IBM Research Division Report RZ279, Zurich, Switzerland (1996)Google Scholar
  12. 12.
    International Organization for Standardization: ISO/IEC 13888–3: Information security techniques - non-repudiation - Part: Mechanisms using asymmetric techniques (1997)Google Scholar
  13. 13.
    International Organization for Standardization: ISO/IEC 13888–2: Information security techniques - non-repudiation - Part: Mechanisms using symmetric techniques (1998)Google Scholar
  14. 14.
    International Organization for Standardization: ISO/IEC 29128: Information technology - Security techniques - Verification of cryptographic protocols (2011)Google Scholar
  15. 15.
    Kremera, S., Markowitcha, O., Zhoub, J.: An intensive survey of fair non-repudiation protocols. Comput. Commun. 25(17), 1606–1621 (2002)CrossRefGoogle Scholar
  16. 16.
    Liu, Y., Zhang, H.: Stand spaces analysis of electronic commerce protocols. Comput. Sci. 35(2), 109–114 (2008)MathSciNetGoogle Scholar
  17. 17.
    Medvinsky, G., Neuman, C.: NetCash: a design of practical electronic currency on the internet. In: 1st ACM Conference on Computer and Communications Security, Fairfax, Virginia, USA, pp. 102–106 (1993)Google Scholar
  18. 18.
    Meadows, C.A., Meadows, C.A.: Formal verification of cryptographic protocols: a survey. In: Pieprzyk, J., Safavi-Naini, R. (eds.) ASIACRYPT 1994. LNCS, vol. 917, pp. 133–150. Springer, Heidelberg (1995). Scholar
  19. 19.
    Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)CrossRefGoogle Scholar
  20. 20.
    Markowitch, O., Gollmann, D., Kremer, S.: On fairness in exchange protocols. In: Lee, P.J., Lim, C.H. (eds.) ICISC 2002. LNCS, vol. 2587, pp. 451–465. Springer, Heidelberg (2003). Scholar
  21. 21.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1), 85–128 (1998)CrossRefGoogle Scholar
  22. 22.
    Roe, M.: Cryptography and evidence. Ph.D. thesis, Computer Laboratory, University of Cambridge (1997)Google Scholar
  23. 23.
    Zhou, J., Gollmann, D.: Evidence and non-repudiation. J. Network Comput. Appl. 20(30), 267–281 (1997)CrossRefGoogle Scholar
  24. 24.
    Wagatsuma, K., Goto, Y., Cheng, J.: A formal analysis method with reasoning for key exchange protocols. IPSJ J. 56(3), 903–910 (2015). (in Japanese)Google Scholar
  25. 25.
    Yan, J., Wagatsuma, K., Gao, H., Cheng, J.: A formal analysis method with reasoning for cryptographic protocols. In: 12th International Conference on Computational Intelligence and Security, pp. 566–570. IEEE Computer Society, Wuxi (2016)Google Scholar
  26. 26.
    Yan, J., Ishibashi, S., Goto, Y., Cheng, J.: A study on fine-grained security properties of cryptographic protocols for formal analysis method with reasoning. In: 2018 IEEE SmartWorld, Ubiquitous Intelligence, Computing, Advanced, Trusted Computing, Scalable Computing, Communications, Cloud, Big Data Computing, Internet of People and Smart City Innovations, pp. 210–215. IEEE-CS, Guangzhou (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Jingchen Yan
    • 1
  • Yating Wang
    • 1
  • Yuichi Goto
    • 1
    Email author
  • Jingde Cheng
    • 1
  1. 1.Department of Information and Computer SciencesSaitama UniversitySaitamaJapan

Personalised recommendations