Spatiotemporal model checking of location and mobility related security policy specifications

Devrim ÜNAL; Mehmet Ufuk ÇAĞLAYAN

Article Details

Spatiotemporal model checking of location and mobility related security policy specifications

Authors:

Devrim ÜNAL | Mehmet Ufuk ÇAĞLAYAN

Publisher:

TUBITAK

Journal:

Turkish Journal of Electrical Engineering and Computer Science 2013 Vol.21 Issue 1, pp.144-173

Document Type:

Article

Publication Date:

12/2012

Document Language:

Turkish

Document ID (Org No.):

2000743389

Frequency:

Bimonthly

eISSN:

1303-6203

pISSN:

1300-0632

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.

 

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.

Article Details

Spatiotemporal model checking of location and mobility related security policy specifications

Authors: Devrim ÜNAL | Mehmet Ufuk ÇAĞLAYAN

Publisher: TUBITAK

Journal: Turkish Journal of Electrical Engineering and Computer Science 2013 Vol.21 Issue 1, pp.144-173

Document Type: Article

Publication Date: 12/2012

Document Language: Turkish

Document ID (Org No.): 2000743389

Frequency: Bimonthly

eISSN: 1303-6203

pISSN: 1300-0632

Issues

Authors:

Devrim ÜNAL | Mehmet Ufuk ÇAĞLAYAN

Publisher:

TUBITAK

Journal:

Turkish Journal of Electrical Engineering and Computer Science 2013 Vol.21 Issue 1, pp.144-173

Document Type:

Article

Publication Date:

12/2012

Document Language:

Turkish

Document ID (Org No.):

2000743389

Frequency:

Bimonthly

eISSN:

1303-6203

pISSN:

1300-0632