Abstract
Many cryptographic protocols proposed to securely send and receive information with someone in unsecured network for various purposes. To design secure cryptographic protocols, formal analysis for cryptographic protocols should be included as an essential activity in a process of cryptographic protocol design. In other word, the ideal process consists of design, formalization, formal analysis, interpretation, and improvement, and the five activities are done repeatedly as similar as activities in spiral model of software development. This paper presents a supporting tool for the ideal process of cryptographic protocol design. At first, the paper presents the spiral model of cryptographic protocol design, and introduces formal analysis method with reasoning as a suitable formal analysis method for the spiral model. The paper also presents design of the supporting tool and its implementation for key exchange protocols. By the supporting tool, designers can only focus on design and improvement activities in the spiral model.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE (2001)
Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. Springer, Berlin (2003)
Cheng, J.: A strong relevant logic model of epistemic processes in scientific discovery. Inf. Modell. Knowl. Bases XI 61, 136–159 (2000)
Cheng, J., Miura, J.: Deontic relevant logic as the logical basis for specifying, verifying, and reasoning about information security and information assurance. In: Proceedings of the 1st International Conference on Availability, Reliability and Security, pp. 601–608. Vienna (2006)
Cheng, J., Nara, S., Goto Y.: FreeEnCal: a forward reasoning engine with general-purpose. In: Knowledge-Based Intelligent Information and Engineering Systems. Lecture Notes in Artificial Intelligence, vol. 4693, pp. 444–452. Springer, Berlin (2007)
Clark, J., Jacob, J.: A survey of authentication protocol literature: version 1.0. http://www.cs.york.ac.uk/~jac/ (1997)
Cremers, C.: The Scyther Tool: verification, falsification, and analysis of security protocols. In: Proceedings of the 20th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
Diaconescu, R., Futatsugi, K.: CafeOBJ Report. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)
Otway, D., Rees, O.: Efficient and timely mutual authentication. ACM SIGOPS Operating Syst. Rev. 21(1), 8–10 (1987)
Paulson, L.C.: Isabelle: a generic theorem prover. In: Lecture Notes in Computer Science, vol. 828. Springer, Berlin (1994)
Schneier, B.: Applied Cryptography. In: Schneier, B. (ed.) Protocols, Algorithms, and Source Code in C. Wiley, New York (1996)
Wagatsuma, K., Anze, S., Goto, Y., Cheng, J.: Formalization for formal analysis of cryptographic protocols with reasoning approach. In: Future Information Technology. Lecture Notes in Electrical Engineering, vol. 309, pp. 211–218. Springer, Heidelberg (2014)
Wagatsuma, K., Goto, Y., Cheng, J.: A formal analysis method with reasoning for key exchange protocols. IPSJ J. (in Japanese) 56(3), 903–910 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wagatsuma, K., Harada, T., Anze, S., Goto, Y., Cheng, J. (2016). A Supporting Tool for Spiral Model of Cryptographic Protocol Design with Reasoning-Based Formal Analysis. In: Park, J., Chao, HC., Arabnia, H., Yen, N. (eds) Advanced Multimedia and Ubiquitous Engineering. Lecture Notes in Electrical Engineering, vol 354. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47895-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-47895-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47894-3
Online ISBN: 978-3-662-47895-0
eBook Packages: EngineeringEngineering (R0)