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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 33992208
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Cryptographic protocol logic: Satisfaction for (timed) Dolev–Yao cryptography
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Kramer%2C+Simon%22">Kramer, Simon</searchLink><relatesTo>1</relatesTo><i> simon.kramer@a3.epfl.ch</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Algebraic+Programming%22">Journal of Logic & Algebraic Programming</searchLink>. Sep2008, Vol. 77 Issue 1/2, p60-91. 32p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Cryptography%22">Cryptography</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+models%22">Mathematical models</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra%22">Algebra</searchLink><br /><searchLink fieldCode="DE" term="%22Requirements+engineering%22">Requirements engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+programming%22">Logic programming</searchLink><br /><searchLink fieldCode="DE" term="%22Quantitative+research%22">Quantitative research</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=33992208
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.jlap.2008.05.005
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 32
        StartPage: 60
    Subjects:
      – SubjectFull: Cryptography
        Type: general
      – SubjectFull: Mathematical models
        Type: general
      – SubjectFull: Algebra
        Type: general
      – SubjectFull: Requirements engineering
        Type: general
      – SubjectFull: Logic programming
        Type: general
      – SubjectFull: Quantitative research
        Type: general
    Titles:
      – TitleFull: Cryptographic protocol logic: Satisfaction for (timed) Dolev–Yao cryptography
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Kramer, Simon
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 09
              Text: Sep2008
              Type: published
              Y: 2008
          Identifiers:
            – Type: issn-print
              Value: 15678326
          Numbering:
            – Type: volume
              Value: 77
            – Type: issue
              Value: 1/2
          Titles:
            – TitleFull: Journal of Logic & Algebraic Programming
              Type: main
ResultId 1