View in EDS

Cryptographic protocol logic: Satisfaction for (timed) Dolev–Yao cryptography

Saved in:
Bibliographic Details
Title: Cryptographic protocol logic: Satisfaction for (timed) Dolev–Yao cryptography
Authors: Kramer, Simon1 simon.kramer@a3.epfl.ch
Source: Journal of Logic & Algebraic Programming. Sep2008, Vol. 77 Issue 1/2, p60-91. 32p.
Subjects: Cryptography, Mathematical models, Algebra, Requirements engineering, Logic programming, Quantitative research
Abstract: Abstract: This article 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 knowledge, norms, provability, space, and time. Secondary concepts 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. [Copyright &y& Elsevier]
Copyright of Journal of Logic & Algebraic Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:Abstract: This article 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 knowledge, norms, provability, space, and time. Secondary concepts 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. [Copyright &y& Elsevier]
ISSN:15678326
DOI:10.1016/j.jlap.2008.05.005