Verification of secure gateway selection protocol using PI-calculus

Author

Rai, A.K. ; Tewari, Rajiv Ranjan

Author_Institution

Dept. of Electron. & Commun., Univ. of Allahabad, Allahabad, India

fYear

2013

Firstpage

1

Lastpage

6

Abstract

For modeling and verifying software systems Formal Methods is an effective methodology. Pi-calculus is a kind of process algebra which can be used to model concurrent and dynamic systems. For analyzing and verifying mobile concurrent systems described by pi-calculus we use Mobility Workbench (MWB) tool. This paper presents a protocol that provides secure gateway (GW) selection mechanism depending on sensitivity of data, as well as provides security to the sensitive data to be forwarded through secure GW from MANET domain to Internet. The proposed protocol allows a source node to forward sensitive data only through secure GW. We model and verify the proposed protocol using Formal Methods in MWB tool.

Keywords

Internet; computer network security; formal verification; internetworking; mobile ad hoc networks; pi calculus; GW selection mechanism; Internet; MANET; MWB tool; data sensitivity; formal methods; mobile concurrent systems; mobility workbench tool; pi-calculus; process algebra; secure gateway selection protocol verification; Internet; Logic gates; Manganese; Mobile ad hoc networks; Routing protocols; Security; Gateway; Internet connectivity; MANET; MWB; Pi-calculus; Security;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering (NUiCONE), 2013 Nirma University International Conference on

Conference_Location

Ahmedabad

Print_ISBN

978-1-4799-0726-7

Type

conf

DOI

10.1109/NUiCONE.2013.6780080

Filename

6780080