Protocol Composition Logic (PCL) is a logic for proving authentication and secrecy properties of network protocols. This chapter presents the central concepts of PCL, including a protocol programming language, the semantics of protocol execution in the presence of a network attacker, the syntax and semantics of PCL assertions, and axioms and proof rules for proving authentication properties. The presentation draws on a logical framework enhanced with subtyping, setting the stage for mechanizing PCL proofs. and gives a new presentation of PCL semantics involving honest and unconstrained principals. Other papers on PCL provide additional axioms, proof rules, and case studies of standardized protocols in common use.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com