Specification of Agent Explicit Knowledge in Cryptographic Protocols

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.

Authors:

• Khair Eddin Sabri
• Ridha Khedri
• Jason Jaskolka

Keywords:

• Information Algebra
• Agent Knowledge
• CryptographicProtocols

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.