View in EDS PDF Full Text

Spatiotemporal model checking of location and mobility related security policy specifications.

Saved in:
Bibliographic Details
Title: Spatiotemporal model checking of location and mobility related security policy specifications.
Authors: ÜNAL, Devrim1 devrim.unal@tubitak.gov.tr, ÇAĞLAYAN, Mehmet Ufuk2
Source: Turkish Journal of Electrical Engineering & Computer Sciences. 2013, Vol. 21 Issue 1, p144-173. 30p.
Subjects: Spatiotemporal processes, Computer security laws, Verification of computer systems, Mobile communication systems, Computer networks, Constraint satisfaction, Algorithms
Abstract: For the formal verification of security in mobile networks, a requirement is that security policies associated with mobility and location constraints are formally specified and verified. For the formal specification and verification of security policies, formal methods ensure that a given network configuration that includes certain network elements satisfies a given security policy. A process calculus based approach is presented, where ambient calculus is used for formal specification of security policies and ambient logic is used for formal representation of mobility and location constraints. A spatiotemporal model checking algorithm is presented for the model checking of formal specifications in ambient calculus with respect to formulas in ambient logic. The presented algorithm allows spatiotemporal model checking of security policy rules and consists of spatial and temporal model checking algorithms. The spatial model checking algorithm is implemented in the Java language and the temporal model checking algorithm is implemented using the NuSMV model checker. [ABSTRACT FROM AUTHOR]
Copyright of Turkish Journal of Electrical Engineering & Computer Sciences is the property of Scientific and Technical Research Council of Turkey 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 Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 91611057
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Spatiotemporal model checking of location and mobility related security policy specifications.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22ÜNAL%2C+Devrim%22">ÜNAL, Devrim</searchLink><relatesTo>1</relatesTo><i> devrim.unal@tubitak.gov.tr</i><br /><searchLink fieldCode="AR" term="%22ÇAĞLAYAN%2C+Mehmet+Ufuk%22">ÇAĞLAYAN, Mehmet Ufuk</searchLink><relatesTo>2</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Turkish+Journal+of+Electrical+Engineering+%26+Computer+Sciences%22">Turkish Journal of Electrical Engineering & Computer Sciences</searchLink>. 2013, Vol. 21 Issue 1, p144-173. 30p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Spatiotemporal+processes%22">Spatiotemporal processes</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+security+laws%22">Computer security laws</searchLink><br /><searchLink fieldCode="DE" term="%22Verification+of+computer+systems%22">Verification of computer systems</searchLink><br /><searchLink fieldCode="DE" term="%22Mobile+communication+systems%22">Mobile communication systems</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+networks%22">Computer networks</searchLink><br /><searchLink fieldCode="DE" term="%22Constraint+satisfaction%22">Constraint satisfaction</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: For the formal verification of security in mobile networks, a requirement is that security policies associated with mobility and location constraints are formally specified and verified. For the formal specification and verification of security policies, formal methods ensure that a given network configuration that includes certain network elements satisfies a given security policy. A process calculus based approach is presented, where ambient calculus is used for formal specification of security policies and ambient logic is used for formal representation of mobility and location constraints. A spatiotemporal model checking algorithm is presented for the model checking of formal specifications in ambient calculus with respect to formulas in ambient logic. The presented algorithm allows spatiotemporal model checking of security policy rules and consists of spatial and temporal model checking algorithms. The spatial model checking algorithm is implemented in the Java language and the temporal model checking algorithm is implemented using the NuSMV model checker. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Turkish Journal of Electrical Engineering & Computer Sciences is the property of Scientific and Technical Research Council of Turkey 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=91611057
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.3906/elk-1105-54
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 30
        StartPage: 144
    Subjects:
      – SubjectFull: Spatiotemporal processes
        Type: general
      – SubjectFull: Computer security laws
        Type: general
      – SubjectFull: Verification of computer systems
        Type: general
      – SubjectFull: Mobile communication systems
        Type: general
      – SubjectFull: Computer networks
        Type: general
      – SubjectFull: Constraint satisfaction
        Type: general
      – SubjectFull: Algorithms
        Type: general
    Titles:
      – TitleFull: Spatiotemporal model checking of location and mobility related security policy specifications.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: ÜNAL, Devrim
      – PersonEntity:
          Name:
            NameFull: ÇAĞLAYAN, Mehmet Ufuk
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Text: 2013
              Type: published
              Y: 2013
          Identifiers:
            – Type: issn-print
              Value: 13000632
          Numbering:
            – Type: volume
              Value: 21
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Turkish Journal of Electrical Engineering & Computer Sciences
              Type: main
ResultId 1