scholarly journals Formal Verification of CHAP PPP authentication Protocol for Smart City/Safe City Applications.

2022 ◽  
Vol 2161 (1) ◽  
pp. 012046
Author(s):  
R Pradeep ◽  
N R Sunitha

Abstract A smart city is a technologically advanced metropolitan region with several connected devices that collects data using various electronic technologies, voice activation methods, and sensors. The information obtained from the data is utilised to efficiently manage assets, resources, and services; in turn, the data is used to enhance operations throughout the city. Achieving security for smart cities is one of the major challenges as the number of connected devices increases the vulnerability also increases. The security of a smart city system depends on the reliability of the security protocols used by the security systems. To design and develop a highly secure system for a smart city the security protocols used must be highly reliable. To prove the reliability of a security protocol the validation technique is not desirable because of its several drawbacks, these drawbacks can be overcome using the formal verification technique which provides the mathematical proof for its correctness. In this work, The Challenge-Handshake Authentication Protocol Point-to-Point (CHAP PPP) which is more commonly used in PPP authentication of smart cities is formally verified using the well-known verification technique known as the model checking technique. The Scyther model checker is the tool used to build the abstract security protocol model.

2003 ◽  
Vol 10 (10) ◽  
Author(s):  
Federico Crazzolara ◽  
Giuseppe Milicia

The chi-Spaces framework provides a set of tools to support every step of the security protocol's life-cycle. The framework includes a simple, yet powerful programming language which is an implementation of the Security Protocol Language (SPL). SPL is a formal calculus designed to model security protocols and prove interesting properties about them. In this paper we take an authentication protocol suited for low-power wireless devices and derive a chi-Spaces implementation from its SPL model. We study the correctness of the resulting implementation using the underlying SPL semantics of chi-Spaces.


2021 ◽  
Author(s):  
Elie Mina ◽  
Saša Petar

Abstract: The concept of the Smart City is increasingly gaining popularity and defines an approach that uses Information and Communication Technology to support the different facets of sustainability processes, while taking into consideration the interests of different stakeholders. Security is one of many issues raised in Smart City initiatives; the security issue is often tackled by the adoption of systems that enhance security systems. Smart Cities raises noteworthy political, specialized, and socioeconomic challenges for creators, trustworthiness, and organizations included in administrating these modern substances. An expanding number of considers center on the security, privacy, and risks inside Smart Cities, highlighting the dangers relating to data security and challenges for Smart City framework within the management and handling of individual information. Smart City has circulated over the created world influencing urban improvement programs and government methodologies. Such future cities are proclaimed for their proficient networked technologies implanted inside the texture of urban situations that give unused implies of social control for the state. These cities are imagined as a technological settle for the numerous issues of advanced city life; Rising advances are not faultless and have vulnerabilities that can be controlled by criminal performing artists. Indeed so, there's a curiously hush around the issues of security among the advocates of Smart Cities. Sažetak: Koncept Pametnog grada sve više dobiva na popularnosti i podrazumijeva pristup koji koristi informacijsku i komunikacijsku tehnologiju za podršku različitim aspektima procesa održivosti, uzimajući u obzir interese različitih dionika. Sigurnost je jedno od mnogih pitanja pokrenutih u inicijativama Pametnog grada. Sigurnosno pitanje često se rješava uvođenjem sustava koji poboljšavaju sigurnost. Pametni gradovi predstavljaju značajne političke, specijalizirane i socioekonomske izazove donositeljima odluka kao i organizacijama uključenim u upravljanje tim modernim sustavima. Sve veći broj istrtaživanja usmjeren je na sigurnost, privatnost i rizike u Pametnim gradovima, ističući opasnosti povezane sa sigurnošću podataka i izazove za Pametni grad u kontekstu upravljanja i korištenja pojedinih informacija. Pametni grad je dio svjetskog konteksta koji utječe na programe urbanih poboljšanja i metode upravljanja. Takvi su gradovi budućnosti zamišljeni kao vješto umrežene tehnologije ugrađene u teksturu urbanih situacija koje otvaraju neiskorištene mogućnosti društvene kontrole države. Ti su gradovi zamišljeni kao tehnološko rješenje za brojna pitanja kvalitete gradskog života. Napredak nije besprijekoran i ranjiv je. Uistinu, među zagovornicima Pametnih gradova postoji neobična šutnja oko pitanja sigurnosti.


Author(s):  
Tom Coffey

This chapter concerns the correct and reliable design of modern security protocols. It discusses the importance of formal verification of security protocols prior to their release by publication or implementation. A discussion on logic-based verification of security protocols and its automation provides the reader with an overview of the current state-of-the-art of formal verification of security protocols. The authors propose a formal verification centred development process for security protocols. This process provides strong confidence in the correctness and reliability of the designed protocols. Thus, the usage of weak security protocols in communication systems is prevented. A case-study on the development of a security protocol demonstrates the advantages of the proposed approach. The case-study concludes with remarks on the performance of automated logic-based verification and presents an overview of formal verification results of a range of modern security protocols.


2022 ◽  
Vol 2161 (1) ◽  
pp. 012042
Author(s):  
H Rekha ◽  
M. Siddappa

Abstract It is very difficult to develop a perfect security protocol for communication over the IoT network and developing a reliable authentication protocol requires a detailed understanding of cryptography. To ensure the reliability of security protocols of IoT, the validation method is not a good choice because of its several disadvantages and limitations. To prove the high reliability of Cryptographic Security Protocols(CSP) for IoT networks, the functional correctness of security protocols must be proved secure mathematically. Using the Formal Verification technique we can prove the functional correctness of IoT security protocols by providing the proofs mathematically. In this work, The CoAP Machine to Machine authentication protocol and centralied IoT network Authentication Protocol RADIUS is formally verified using the well-known verification technique known as model checking technique and we have used the Scyther model checker for the verification of security properties of the respective protocols. The abstract protocol models of the IoT authentication protocols were specified in the security protocol description language and the security requirements of the authentication protocols were specified as claim events.


2018 ◽  
pp. 60-67
Author(s):  
Henrika Pihlajaniemi ◽  
Anna Luusua ◽  
Eveliina Juntunen

This paper presents the evaluation of usersХ experiences in three intelligent lighting pilots in Finland. Two of the case studies are related to the use of intelligent lighting in different kinds of traffic areas, having emphasis on aspects of visibility, traffic and movement safety, and sense of security. The last case study presents a more complex view to the experience of intelligent lighting in smart city contexts. The evaluation methods, tailored to each pilot context, include questionnaires, an urban dashboard, in-situ interviews and observations, evaluation probes, and system data analyses. The applicability of the selected and tested methods is discussed reflecting the process and achieved results.


2020 ◽  
Vol 18 (4) ◽  
pp. 765-779
Author(s):  
E.V. Popov ◽  
K.A. Semyachkov ◽  
K.V. Zhunusova

Subject. This article explores the basic elements of the engineering infrastructure of smart cities. Objectives. The article aims to systematize theoretical descriptions of the engineering infrastructure of a smart city. Methods. For the study, we used a logical analysis and systematization. Results. The article highlights the main areas of infrastructure development of smart cities. Conclusions. Improving process management mechanisms, optimizing urban infrastructure, increasing the use of digital technologies, and developing socio-economic innovation improve the quality of the urban environment in a digitalized environment. And improving the efficiency of urban planning and security, studying its properties and characteristics, and forming an effective urban information system lead to its functional transformations.


2017 ◽  
Vol 14 (1) ◽  
pp. 118-128
Author(s):  
Jason Cohen ◽  
Judy Backhouse ◽  
Omar Ally

Young people are important to cities, bringing skills and energy and contributing to economic activity. New technologies have led to the idea of a smart city as a framework for city management. Smart cities are developed from the top-down through government programmes, but also from the bottom-up by residents as technologies facilitate participation in developing new forms of city services. Young people are uniquely positioned to contribute to bottom-up smart city projects. Few diagnostic tools exist to guide city authorities on how to prioritise city service provision. A starting point is to understand how the youth value city services. This study surveys young people in Braamfontein, Johannesburg, and conducts an importance-performance analysis to identify which city services are well regarded and where the city should focus efforts and resources. The results show that Smart city initiatives that would most increase the satisfaction of youths in Braamfontein  include wireless connectivity, tools to track public transport  and  information  on city events. These  results  identify  city services that are valued by young people, highlighting services that young people could participate in providing. The importance-performance analysis can assist the city to direct effort and scarce resources effectively.


2020 ◽  
Vol 15 (2) ◽  
pp. 52-58
Author(s):  
L. V. Shkvarya ◽  
A. S. Semenov

In the twenty-first century different countries and cities are increasingly seeking to introduce quality improvements in their livelihoods, generate for its residents an environment that is called “smart city” on the basis of high technologies. The article shows that the emergence of a “smart” city is an objective necessity due to the rapid growth of cities in the present and in the future. “Smart” city is designed to solve life problems in cities and create conditions for the socio-economic development of cities and countries, and for a favorable stay of residents on its territory. There are a number of strategies to implement the concept of “smart”, but it is important for each urban settlement to develop its own approaches and projects.


2020 ◽  
pp. 50-62
Author(s):  
K.S. Teteryatnikov ◽  
S.G. Каmolov ◽  
A.A. Pyatova

The article is meant to analyze various strategies and models for the development of smart cities, as well as the concept of project financing of smart cities, proposed by Pietro Doran, one of the founding partners of the world’s first smart city built from scratch in South Korea — Songdo. The authors believe that Songdo’s financing model, based on P. Doran’s Project Model can be considered as an effective way to attract investment in greenfield projects for the development of «smart cities» in Russia on the basis of public-private partnership.


Sign in / Sign up

Export Citation Format

Share Document