Cryptographic Protocol Logic (CPL)

The extended abstract for the LICS2003 short presentation

	"A Language and a Notion of Truth for Cryptographic Properties"

is available at:


We provide a logical language and outline a notion of truth for the
specification and verification of cryptographic protocols. The language
integrates modalities for temporal, epistemic, and normative statements.
It allows one to express and compare arbitrary cryptographic properties
intuitively, succinctly, and in an endogenous fashion. The notion of 
is external and defined through satisfaction in terms of models of 
guarded cryptographic processes. It allows for mechanical verification
by means of model-checking.

The formalism will be called CPL (for Cryptographic Protocol Logic).

Latest changes to the formalism (not mentioned in the extended 
(1) the replacement of the predicate for syntactic equality of messages 
a predicate for sub-term-related messages
(2) the addition of two atomic predicates for typing messages and
sub-typing message types