View in EDS HTML Full Text PDF Full Text

Proving security protocols with model checkers by data independence techniques.

Saved in:
Bibliographic Details
Title: Proving security protocols with model checkers by data independence techniques.
Authors: Roscoe, A.W., Broadfoot, P.J.
Source: Journal of Computer Security. 1999, Vol. 7 Issue 2/3, p147. 44p. 1 Diagram.
Subjects: Computer network protocols, CSP (Computer program language)
Abstract: Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols -- see, for example, [16,20] and many of the papers in [7]. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources such as keys and nonces, is free of attacks. While for specific protocols there are frequently good reasons for supposing that this will find any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related fields can be used to achieve the illusion that nodes can call upon an infinite supply of different nonces, keys, etc., even though the actual types used for these things remain finite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs, and to claim that a finite-state run on a model checker has proved that a given protocol is free from attacks which could be constructed in the model used. We develop our methods via a series of case studies, discovering a number of methods for restricting the number of states generated in attempted proofs, and using two distinct approaches to protocol specification. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Computer Security is the property of Sage Publications Inc. 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
Full text is not displayed to guests.
FullText Links:
  – Type: pdflink
Text:
  Availability: 1
Header DbId: egs
DbLabel: Engineering Source
An: 2559049
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Proving security protocols with model checkers by data independence techniques.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Roscoe%2C+A%2EW%2E%22">Roscoe, A.W.</searchLink><br /><searchLink fieldCode="AR" term="%22Broadfoot%2C+P%2EJ%2E%22">Broadfoot, P.J.</searchLink>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Computer+Security%22">Journal of Computer Security</searchLink>. 1999, Vol. 7 Issue 2/3, p147. 44p. 1 Diagram.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Computer+network+protocols%22">Computer network protocols</searchLink><br /><searchLink fieldCode="DE" term="%22CSP+%28Computer+program+language%29%22">CSP (Computer program language)</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols -- see, for example, [16,20] and many of the papers in [7]. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources such as keys and nonces, is free of attacks. While for specific protocols there are frequently good reasons for supposing that this will find any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related fields can be used to achieve the illusion that nodes can call upon an infinite supply of different nonces, keys, etc., even though the actual types used for these things remain finite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs, and to claim that a finite-state run on a model checker has proved that a given protocol is free from attacks which could be constructed in the model used. We develop our methods via a series of case studies, discovering a number of methods for restricting the number of states generated in attempted proofs, and using two distinct approaches to protocol specification. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Computer Security is the property of Sage Publications Inc. 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=2559049
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.3233/JCS-1999-72-303
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 44
        StartPage: 147
    Subjects:
      – SubjectFull: Computer network protocols
        Type: general
      – SubjectFull: CSP (Computer program language)
        Type: general
    Titles:
      – TitleFull: Proving security protocols with model checkers by data independence techniques.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Roscoe, A.W.
      – PersonEntity:
          Name:
            NameFull: Broadfoot, P.J.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: 1999
              Type: published
              Y: 1999
          Identifiers:
            – Type: issn-print
              Value: 0926227X
          Numbering:
            – Type: volume
              Value: 7
            – Type: issue
              Value: 2/3
          Titles:
            – TitleFull: Journal of Computer Security
              Type: main
ResultId 1