Cryptographic Protocol Logic (CPL)

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Announcement of technical report:

	Title:
	"CPL: An Evidence-Based 5-Dimensional Logic for the Compositional
		Specification and Verification of Cryptographic Protocols.
			Part I: Language, Process Model, Satisfaction."

	Abstract:
	"We
		(1) define a logic, called CPL (for Cryptographic Protocol Logic),
			where truth is established on the grounds of evidence-based
			knowledge (as opposed to awareness-based belief), spanning
			the dimensions of first-order, temporal, epistemic, deontic,
			and linear logic;
		(2) state a few of its key properties; and
		(3) illustrate how it can be used to compositionally specify and 
verify
			cryptographic protocols designed to establish trust in the security
			of communication (as opposed to security of storage) between
			protocol-compliant participants in a hostile environment.
	 Our claim hereby is to give
		(1) the first formalisation of cryptographic discourse within the
			framework of multi-dimensional logic,
		(2) the most comprehensive and logically-connected formal model
			of cryptographic protocols proposed so far, and
		(3) a rigourous clarification of the concepts constituting the common
			knowledge of the community of protocol designers."

	Document:
	http://ic2.epfl.ch/publications/documents/IC_TECH_REPORT_200414.pdf

	Author:
	http://lampwww.epfl.ch/~kramer/