Specification of Agent Explicit Knowledge in Cryptographic Protocols

Authors: Khair Eddin Sabri, Ridha Khedri, Jason Jaskolka

Abstract:

Cryptographic protocols are widely used in various applications to provide secure communications. They are usually represented as communicating agents that send and receive messages. These agents use their knowledge to exchange information and communicate with other agents involved in the protocol. An agent knowledge can be partitioned into explicit knowledge and procedural knowledge. The explicit knowledge refers to the set of information which is either proper to the agent or directly obtained from other agents through communication. The procedural knowledge relates to the set of mechanisms used to get new information from what is already available to the agent. In this paper, we propose a mathematical framework which specifies the explicit knowledge of an agent involved in a cryptographic protocol. Modelling this knowledge is crucial for the specification, analysis, and implementation of cryptographic protocols. We also, report on a prototype tool that allows the representation and the manipulation of the explicit knowledge.

Keywords: Information Algebra, Agent Knowledge, CryptographicProtocols

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1329128

References:

[1] Mart'─▒n Abadi and V'eronique Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 367(1):2-32, 2006.
[2] Martin Abadi and Andrew D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. In Proceedings of the 4th ACM Conference on Computer and Communications Security, pages 36-47. ACM Press, 1997.
[3] Kamel Adi, Mourad Debbabi, and Mohamed Mejri. A New Logic for Electronic Commerce Protocols. Theoretical Computer Science, 291(3):223-283, January 2003.
[4] Issam Al-Azzoni, Douglas G. Down, and Ridha Khedri. Modeling and Verification of Cryptographic Protocols Using Coloured Petri Nets and Design/CPN. Nordic Journal of Computing, 12(3):200-228, September 2005.
[5] Giampaolo Bella. Inductive verification of smart card protocols. Journal of Computer Security, 11(1):87-132, 2003.
[6] Michael Burrows, Mart'─▒n Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18-36, February 1990.
[7] Iliano Cervesato. Typed multiset rewriting specifications of security protocols. In A. Seda, editor, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology ÔÇö MFCSIT-00, pages 1-43, Cork, Ireland, 19-21 July 2000. Elsevier ENTCS 40.
[8] Edmund M. Clarke, Somesh Jha, and Wilfredo Marrero. Verifying Security Protocols with Brutus. ACM Transactions on Software Engineering and Methodology, 9(4):443-487, October 2000.
[9] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge university press, second edition, 2002.
[10] St'ephanie Delaune. Easy Intruder Deduction Problems with Homomorphisms. Information Processing Letters, 97(6):213-218, March 2006.
[11] F. Javier Thayer F'abrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security, 7(2-3):191-230, January 1999.
[12] Riccardo Focardi and Roberto Gorrieri. The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering, 23(9):550-571, September 1997.
[13] J¨urg Kohlas and Robert F. St¨ark. Information Algebras and Consequence Operators. Logica Universalis, 1(1):139-165, January 2007.
[14] Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Intruder deduction for the equational theory of Abelian groups with distributive encryption. Information and Computation, 205(4):581-623, April 2007.
[15] Guy Leduc and Franc┬©ois Germeau. Verification of security protocols using LOTOS-method and application. Computer Communications, 23(12):1089-1103, July 2000.
[16] Gavin Lowe and Bill Roscoe. Using CSP to Detect Errors in the TMN Protocol. IEEE Transactions on Software Engineering, 23(10):659-669, October 1997.
[17] Xiao-Qi Ma and Xiao-Chun Cheng. Formal Verification of Merchant Registration Phase of SET Protocol. International Journal of Automation and Computing, 2(2):155-162, December 2005.
[18] Fabio Martinelli. Analysis of Security Protocols as Open Systems. Theoretical Computer Science, 290(1):1057-1106, January 2003.
[19] Catherine Meadows. Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer. In IEEE Symposium on Security and Privacy, pages 216-231. IEEE Computer Society, May 1999.
[20] John C. Mitchell, Mark Mitchell, and Ulrich Stern. Automated analysis of cryptographic protocols using MurÁ. In IEEE Symposium on Security and Privacy, May 1997.
[21] Jun Pang. Analysis of a security protocol in ╬╝CRL. Technical Report SEN-R0201, CWI, Amsterdam, 2002.
[22] Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1-2):85-128, September 1998.
[23] Khair Eddin Sabri and Ridha Khedri. A multi-view approach for the analysis of cryptographic protocols. In Workshop on Practice and Theory of IT Security (PTITS 2006), pages 21-27, Montreal, QC, Canada, 2006.
[24] Khair Eddin Sabri and Ridha Khedri. A mathematical framework to capture agent explicit knowledge in cryptographic protocols. Technical Report CAS-07-04-RK, department of Computing and Software, Faculty of Engineering, McMaster University, 2007. http://www.cas.mcmaster.ca/cas/research/cas reports06-07.php (accessed on September 15, 2008).
[25] Khair Eddin Sabri and Ridha Khedri. Multi-view framework for the analysis of cryptographic protocols. Technical Report CAS-07-06- RK, department of Computing and Software, Faculty of Engineering, McMaster University, 2007.
[26] Khair Eddin Sabri and Ridha Khedri. Agent explicit knowledge: Survey of the literature and elements of a suitable representation. In 2nd Workshop on Practice and Theory of IT Security (PTITS 2008), pages 4-9, Montreal, QC, Canada, 2008.