Formal Specification of Information Transmission Architecture Based on Automatic Generation of Primitives in Digital Campus

2013 ◽  
Vol 846-847 ◽  
pp. 1644-1647
Author(s):  
Xiao Le Li ◽  
Ying Wen ◽  
Ming Weng
Keyword(s):  
Information Transmission ◽  
Formal Analysis ◽  
Automatic Generation ◽  
Comprehensive Analysis ◽  
Security Requirements ◽  
Digital Campus ◽  
Application Systems ◽  
Secure Information ◽  
Common Framework ◽  
Automatic Tool

Based on comprehensive analysis on security requirements of information transmission, security primitive is generated by automatic tool in asymmetric key cryptosystem, and improved with addition of compositional factors. And then, formal processes of secure information transmission are constructed with composition method. Formal analysis shows that, secrecy, integrity, availability, controllability, non-repudiation and identifiability during information transmission can be insured by this architecture, as a common framework for development of various application systems in digital campus from the viewpoint of information security.

Design and Verification of Security Protocol for Information Transmission in Digital Campus

2012 ◽  
Vol 532-533 ◽  
pp. 1230-1234 ◽  
Author(s):  
Xiao Le Li ◽  
Yong Jun Luo ◽  
Yu Liang ◽  
Ying Wen
Keyword(s):  
Information Security ◽  
Information Transmission ◽  
Formal Analysis ◽  
Comprehensive Analysis ◽  
Security Protocol ◽  
Security Requirements ◽  
Transmission Model ◽  
Digital Campus ◽  
Application Systems ◽  
Formal Design

This paper mainly studies application of formal design for security protocols in digital campus. With a comprehensive analysis on security requirements of information transmission in digital campus, an information transmission model is built from the viewpoint of information security. Based on this model, a new security protocol, called DCIT for short, is designed. The formal analysis shows that secrecy, integrity, availability, controllability, non-repudiation and identifiability of information during transmission could be insured by DCIT, which could be used as a direction for development of various application systems in digital campus, from the viewpoint of information security.

scholarly journals A Method for Model-Driven Information Flow Security

2012 ◽  
pp. 199-229 ◽  
Author(s):  
Fredrik Seehusen ◽  
Ketil Stølen
Keyword(s):  
Software Development ◽  
Information Flow ◽  
System Architecture ◽  
Security Requirements ◽  
State Machines ◽  
Flow Properties ◽  
Information Flow Security ◽  
Software Developer ◽  
Model Driven ◽  
Secure Information

We present a method for software development in which information flow security is taken into consideration from start to finish. Initially, the user of the method (i.e., a software developer) specifies the system architecture and selects a set of security requirements (in the form of secure information flow properties) that the system must adhere to. The user then specifies each component of the system architecture using UML inspired state machines, and refines/transforms these (abstract) state machines into concrete state machines. It is shown that if the abstract specification adheres to the security requirements, then so does the concrete one provided that certain conditions are satisfied.

scholarly journals Understanding Hohfeld and Formalizing Legal Rights: The Hohfeldian Conceptions and Their Conditional Consequences

Studia Logica ◽  
2019 ◽  
Vol 108 (1) ◽  
pp. 129-158 ◽  
Author(s):  
Réka Markovich
Keyword(s):  
Legal Theory ◽  
Formal Analysis ◽  
Comprehensive Analysis ◽  
Legal Rights ◽  
Fundamental Theory ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Different Types ◽  
Multi Agent ◽  
Judicial Reasoning

Abstract Hohfeld’s analysis (Fundamental Legal Conceptions as Applied in Judicial Reasoning, 1913, 1917) on the different types of rights and duties is highly influential in analytical legal theory, and it is considered as a fundamental theory in AI&Law and normative multi-agent systems. Yet a century later, the formalization of this theory remains, in various ways, unresolved. In this paper I provide a formal analysis of how the working of a system containing Hohfeldian rights and duties can be delineated. This formalization starts from using the same tools as the classical ones by Kanger and Lindahl used, but instead of focusing on the algebraic features of rights and duties, it aims at providing a comprehensive analysis of what these rights and duties actually are and how they behave and at saying something substantial on Power too—maintaining all along the Hohfeldian intentions that these rights and duties are sui generis and inherently relational.

Formal Analysis of an Efficient Handover Authentication Scheme for EAP-Based Wireless Networks with Extending BAN Logic

2013 ◽  
Vol 401-403 ◽  
pp. 1864-1867 ◽  
Author(s):  
Li Ling Cao ◽  
Wan Cheng Ge
Keyword(s):  
Wireless Networks ◽  
Privacy Preservation ◽  
Formal Analysis ◽  
Main Idea ◽  
Authentication Protocol ◽  
Security Requirements ◽  
Ban Logic ◽  
Handover Authentication ◽  
Authentication Schemes ◽  
Extensible Authentication Protocol

The existing Extensible Authentication Protocol (EAP) based handover authentication schemes have show robust security features especially the Qi Jing et al.'s design, which not only meets the essential security requirements in handover authentication but also achieves privacy preservation. However, it still suffers pitfalls in the process of authentication. The main idea of this paper is to extend the work by Qi Jing et al. and particularly focus on the formal analysis using extending BAN logic which is more concise yet practical to use on PKI-based protocols.

scholarly journals A RSA-Biometric Based User Authentication Scheme For Smart-Homes Using Smartphone

2021 ◽  
Author(s):  
Amir Mohammadi Bagha
Keyword(s):  
User Authentication ◽  
Smart Cities ◽  
Formal Analysis ◽  
Smart Homes ◽  
Authentication Scheme ◽  
Security Requirements ◽  
Computational Time ◽  
Automation System ◽  
Push Button ◽  
User Authentication Scheme

Internet of Things (IoT) is considered as one of the emerging leading technologies that allow the mainstreaming of smart homes and smart cities in the recent years, by creating a communication system for physical objects over the Internet. In a smart home (also called push-button home automation system), devices are not necessarily homogeneous in terms of topology, security protocols, computational power and communication. This nature of the devices causes some incompatibility with conventional authentication methods and the security requirements of IoT standards. This thesis proposes an RSA-Biometric based three-factor User Authentication Scheme for Smart-Homes using Smartphone (called RSA-B-ASH-S scheme). An informal security analysis of the proposed RSA-B-ASH-S scheme is provided, along with its performance evaluation in terms of computational time, storage requirements and communication overload. Furthermore, a formal analysis of the proposed RSA-B-ASH-S scheme using the Burrows-Abadi-Needham (BAN) Logic is described, showing that the proposed scheme achieves the forward secrecy property by utilizing a fresh encryption key for each session and it also satisfies the anonymity of the user by using a one-time token. A proof of concept of the proposed RSA-B-ASH-S scheme is also provided.

Sign in / Sign up

Export Citation Format

Share Document