การวิเคราะห์ความมั่นคงปลอดภัยที่ได้รับการปรับปรุงให้ดีขึ้น ของโพรโตคอลสำหรับการเซ็นสัญญาที่มีความยุติธรรมของมิคาลี่ โดยใช้คัลเลอร์เพทริเน็ต (An Improved Security Analysis of Micali’s Fair Contract Signing Protocol by Using Coloured Petri Nets)

Authors

  • ยงยุทธ เพิ่มพูนธนลาภ ห้องปฎิบัติการวิจัยตรรกะศาสตร์และการักษาความมั่นคงปลอดภัย ภาควิศวกรรมคอมพิวเตอร์ คณะวิศวกรรมศาสตร์ มหาวิทยาลัยเทคโนโลยีพระจอมเกล้าธนบุรี

Keywords:

formal methods for cryptographic protocols, model checking, coloured petri nets, cryptographic protocols, , network security, formal methods

Abstract

มิคาลี่ได้นำเสนอโพรโตคอลสำหรับการแลกเปลี่ยนข้อมูลอีเล็กโทรนิกส์แบบที่มีความยุติธรรมโดยใช้เทคนิคการเข้ารหัสข้อมูล ซึ่งมีชื่อว่า อีซีเอสวัน ซึ่งสามารถนำมาใช้ในการเซ็นต์สัญญาที่แลกเปลี่ยนกันระหว่างสองบุคคลใดๆ  ต่อมาเบาว์และคณะ ค้นพบการโจมตีแบบการนำข้อความมาส่งใหม่ ในทั้งอีซีเอสวันและอีซีเอสวันที่ถูกปรับปรุงเพื่อให้มีความชัดเจนมากขึ้น หลังจากนั้นซางและคณะค้นพบการโจมตีอีกสองแบบในอีซีเอสวันที่ถูกปรับปรุงโดยเบาว์ แต่ทั้งการวิเคราะห์โดยเบาว์และซางเป็นการวิเคราะห์โดยใช้มือ ในงานที่แล้วของเราได้พัฒนาวิธีการที่เป็นแบบอัตโนมัติในการวิเคราะห์ความมั่นคงปลอดภัยในโพรโตคอลที่ใช้การเข้ารหัสข้อมูล โดยใช้คัลเลอร์เพทริเน็ต และเราได้ประยุกต์ใช้วิธีการของเราในการวิเคราะห์เบื้องต้นสำหรับทั้งสองโพรโตคอล ซึ่งเราพบการโจมตีสองแบบในอีซีเอสวันและการโจมตีสามแบบในอีซีเอสวันที่ถูกปรับปรุงโดยเบาว์ ในบทความนี้เราได้ทำการขยายการวิเคราะห์ความมั่นคงปลอดภัยให้ละเอียดเพิ่มมากขึ้น ซึ่งทำให้เราค้นพบการโจมตีใหม่สองแบบในลักษณะมัลติเซสชั่นในอีซีเอสวันและการโจมตีใหม่สองแบบในลักษณะมัลติเซสชั่นในอีซีเอสวันที่ถูกปรับปรุงโดยเบาว์Micali proposed a simple and practical cryptographic fair exchange protocol, called ECS1, for contract signing. Bao et al. found some message replay attacks in both the original ECS1 and a modified ECS1 where the latter aims to solve an ambiguity in the former. Later, Zhang et. al. found two multi-session attacks in the modified ECS1. Both Bao’s and Zhang’s analyses are manual. In our previous work, we have developed an automated methodology to analyze cryptographic protocols by using Coloured Petri Nets (CPN) and performed a preliminary analysis on both versions of ECS1. There, we found two multi-session attacks in original ECS1 and three multi-session attacks in the modified ECS1. In this paper, we extend our previous analysis on ECS1 more comprehensively. As a result, we found two new multi-session attacks in original ECS1 and two new multi-session attacks in the modified ECS1.    

Downloads

Download data is not yet available.

Downloads