Spatiotemporal model checking of location and mobility related security policy specifications

Devrim ÜNAL; Mehmet Ufuk ÇAĞLAYAN

Makale detayları

Spatiotemporal model checking of location and mobility related security policy specifications

Yazarlar:

Devrim ÜNAL | Mehmet Ufuk ÇAĞLAYAN

Yayıncı:

TUBITAK

Dergi:

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

Belge Tipi:

Makale

Yayın Tarihi:

12/2012

Belge Dili:

Türkçe

Document ID (Org No.):

2000743389

Sıklık:

İki Aylık

eISSN:

1303-6203

pISSN:

1300-0632

Özet:

 

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.

Makale detayları

Spatiotemporal model checking of location and mobility related security policy specifications

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

Yayıncı: TUBITAK

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

Belge Tipi: Makale

Yayın Tarihi: 12/2012

Belge Dili: Türkçe

Document ID (Org No.): 2000743389

Sıklık: İki Aylık

eISSN: 1303-6203

pISSN: 1300-0632

Sayı

Yazarlar:

Devrim ÜNAL | Mehmet Ufuk ÇAĞLAYAN

Yayıncı:

TUBITAK

Dergi:

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

Belge Tipi:

Makale

Yayın Tarihi:

12/2012

Belge Dili:

Türkçe

Document ID (Org No.):

2000743389

Sıklık:

İki Aylık

eISSN:

1303-6203

pISSN:

1300-0632