A Theorem for Secrecy in Tagged Protocols Using the Theory of Witness-Functions
Jaouhar Fattahi
TL;DR
This paper introduces a theorem for analyzing secrecy in tagged cryptographic protocols using witness-functions, and applies it to a new version of the Needham-Schroeder protocol to demonstrate its effectiveness.
Contribution
It presents a formal theorem for secrecy in tagged protocols and applies it to a new tagged version of the Needham-Schroeder protocol.
Findings
Theorem provides a formal basis for secrecy analysis in tagged protocols
Application to Needham-Schroeder protocol demonstrates practical utility
Highlights importance of tagging in cryptographic security
Abstract
In this paper, we enunciate the theorem of secrecy in tagged protocols using the theory of witness-functions and we run a formal analysis on a new tagged version of the Needham-Schroeder public-key protocol using this theorem. We discuss the significance of tagging in securing cryptographic protocols as well.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.