skip to main content
column

Logical concepts in cryptography

Published: 01 December 2007 Publication History

Abstract

The thesis is about a breadth-first exploration of logical concepts in cryptography and their linguistic abstraction and model-theoretic combination in a comprehensive logical system, called CPL (for Cryptographic Protocol Logic). We focus on two fundamental aspects of cryptography. Namely, the security of communication (as opposed to security of storage) and cryptographic protocols (as opposed to cryptographic operators). The logical concepts explored are the following. Primary concepts: the modal concepts of belief, knowledge, norms, provability, space, and time. Secondary concepts: belief with error control, individual and propositional knowledge, confidentiality norms, truth-functional and relevant (in particular, intuitionistic) implication, multiple and complex truth values, and program types. The distinguishing feature of CPL is that it unifies and refines a variety of existing approaches. This feature is the result of our wholistic conception of property-based (modal logics) and model-based (process algebra) formalisms. We illustrate the expressiveness of CPL on representative requirements engineering case studies. Further, we extend (core) CPL (qualitative time) with rational-valued time, i.e., time stamps, timed keys, and potentially drifting local clocks, to tCPL (quantitative time). Our extension is conservative and provides further evidence for Lamport's claim that adding real time to an untimed formalism is really simple. Furthermore, we sketch an extension of (core) CPL with a notion of probabilistic polynomial-time (PP) computation. We illustrate the expressiveness of this extended logic (ppCPL) on tentative formalisation case studies of fundamental and applied concepts. Fundamental concepts: (1) one-way function, (2) hard-core predicate, (3) computational indistinguishability, (4) (n-party) interactive proof, and (5) (n-prover) zero-knowledge. Applied concepts: (1) security of encryption schemes, (2) unforgeability of signature schemes, (3) attacks on encryption schemes, (4) attacks on signature schemes, and (5) breaks of signature schemes. In the light of logic, adding PP to a formalism for cryptographic protocols is perhaps also simple and can be achieved with an Ockham's razor extension of an existing core logic, namely CPL.

Cited By

View all
  • (2010)To know or not to know: epistemic approaches to security protocol verificationSynthese10.1007/s11229-010-9765-8177:S1(51-76)Online publication date: 24-Aug-2010
  • (2010)A spatial equational logic for the applied π-calculusDistributed Computing10.1007/s00446-010-0112-623:1(61-83)Online publication date: 13-Jul-2010
  • (2008)Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol2008 IEEE Symposium on Security and Privacy (sp 2008)10.1109/SP.2008.23(202-215)Online publication date: May-2008

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGACT News
ACM SIGACT News  Volume 38, Issue 4
December 2007
54 pages
ISSN:0163-5700
DOI:10.1145/1345189
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 2007
Published in SIGACT Volume 38, Issue 4

Check for updates

Author Tags

  1. applied formal logic
  2. information security

Qualifiers

  • Column

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2010)To know or not to know: epistemic approaches to security protocol verificationSynthese10.1007/s11229-010-9765-8177:S1(51-76)Online publication date: 24-Aug-2010
  • (2010)A spatial equational logic for the applied π-calculusDistributed Computing10.1007/s00446-010-0112-623:1(61-83)Online publication date: 13-Jul-2010
  • (2008)Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol2008 IEEE Symposium on Security and Privacy (sp 2008)10.1109/SP.2008.23(202-215)Online publication date: May-2008

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media