Formal Analysis of SA-TEK 3-Way Handshake Protocols

IEEE 802.16 is the standard for broadband wireless access.The security sublayer is provided within IEEE 802.16 MAC layer for privacy and access control,in which the privacy and key management(PKM)protocols are specified.In IEEE 802.16e,SA-TEK 3-way handshake is added into PKM protocols,aiming to facilitate re-authentication and key distribution.This paper analyzes the SA-TEK 3-way handshake protocol,and proposes an optimized version.We also use CasperFDR,a popular formal analysis tool,to verify our analysis.Moreover,we model various simplified versions to find the functions of those elements in the protocol,and correct some misunderstandings in related works using other formal analysis tools.

A Formal Model for Analyzing Fair Exchange Protocols Based on Event Logic

Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network transactions.In order to address the limitations of current research methods and enhance the analytical capabilities for fair exchange protocols,this paper proposes a formal model for analyzing such protocols.The proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of fairness.This definition accurately captures the inherent requirements of fair exchange protocols.Building upon event logic,the model incorporates the time factor into predicates and introduces knowledge set axioms.This enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired knowledge.To maximize the intruder’s capabilities,channel errors are translated into the behaviors of the intruder.The participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential impact.By employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol analysis.The entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding countermeasures.The developedmodel enhances the ability to reason about and evaluate the security properties of fair exchange protocols,thereby contributing to the advancement of secure network transactions.

A Novel Formal Analysis Method of Network Survivability Based on Stochastic Process Algebra

Stochastic process algebras have been proposed as compositional specification formalisms for performance models. A formal analysis method of survivable network was proposed based on stochastic process algebra, which incorporates formal modeling into performance analysis perfectly, and then various performance parameters of survivable network can be simultaneously obtained after formal modeling. The formal description with process expression to the survivable network system was carried out based on the simply introduced syntax and operational semantics of stochastic process algebra. Then PEPA workbench tool was used to obtain the probability of system’s steady state availability and transient state availability. Simulation experiments show the effectiveness and feasibility of the developed method.

Skyline refinement exploiting fuzzy formal concept analysis

Purpose-The study of the skyline queries has received considerable attention from several database researchers since the end of 2000’s.Skyline queries are an appropriate tool that can help users to make intelligent decisions in the presence of multidimensional data when different,and often contradictory criteria are to be taken into account.Based on the concept of Pareto dominance,the skyline process extracts the most interesting(not dominated in the sense of Pareto)objects from a set of data.Skyline computation methods often lead to a set with a large size which is less informative for the end users and not easy to be exploited.The purpose of this paper is to tackle this problem,known as the large size skyline problem,and propose a solution to deal with it by applying an appropriate refining process.Design/methodology/approach-The problem of the skyline refinement is formalized in the fuzzy formal concept analysis setting.Then,an ideal fuzzy formal concept is computed in the sense of some particular defined criteria.By leveraging the elements of this ideal concept,one can reduce the size of the computed Skyline.Findings-An appropriate and rational solution is discussed for the problem of interest.Then,a tool,named SkyRef,is developed.Rich experiments are done using this tool on both synthetic and real datasets.Research limitations/implications-The authors have conducted experiments on synthetic and some real datasets to show the effectiveness of the proposed approaches.However,thorough experiments on large-scale real datasets are highly desirable to show the behavior of the tool with respect to the performance and time execution criteria.Practical implications-The tool developed SkyRef can have many domains applications that require decision-making,personalized recommendation and where the size of skyline has to be reduced.In particular,SkyRef can be used in several real-world applications such as economic,security,medicine and services.Social implications-This work can be expected in all domains that require decision-making like hotel finder,restaurant recommender,recruitment of candidates,etc.Originality/value-This study mixes two research fields artificial intelligence(i.e.formal concept analysis)and databases(i.e.skyline queries).The key elements of the solution proposed for the skyline refinement problem are borrowed from the fuzzy formal concept analysis which makes it clearer and rational,semantically speaking.On the other hand,this study opens the door for using the formal concept analysis and its extensions in solving other issues related to skyline queries,such as relaxation.

Trustworthy Explainable Recommendation Framework for Relevancy

Explainable recommendation systems deal with the problem of‘Why’.Besides providing the user with the recommendation,it is also explained why such an object is being recommended.It helps to improve trustworthiness,effectiveness,efficiency,persuasiveness,and user satisfaction towards the system.To recommend the relevant information with an explanation to the user is required.Existing systems provide the top-k recommendation options to the user based on ratings and reviews about the required object but unable to explain the matched-attribute-based recommendation to the user.A framework is proposed to fetch the most specific information that matches the user requirements based on Formal Concept Analysis(FCA).The ranking quality of the recommendation list for the proposed system is evaluated quantitatively with Normalized Discounted Cumulative Gain(NDCG)@k,which is better than the existing systems.Explanation is provided qualitatively by considering trustworthiness criterion i.e.,among the seven explainability evaluation criteria,and its metric satisfies the results of proposed method.This framework can be enhanced to accommodate for more effectiveness and trustworthiness.

Security Analysis of an Electronic Commerce Protocol Using Casper/FDR2

Researchers have proposed several security protocols to protect the electronic commerce security in these years;however,not all of them are secure enough.This article extends model checking method with Casper/FDR2 to model and analyze a new electronic protocol.Attacks are found in the protocol and their mechanisms are discussed.A variety of solutions are given to different security flaws.The improved protocol is proven to be robust and secure.

Visual Specification and Analysis of Contract-Based SoftwareArchitectures

XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e., interaction protocols). XCD is supported by a translator that produces formal models in SPIN’s ProMeLa formal verification language, which can then be formally analysed using SPIN’s model checker. XCD is extended with a visual notation set called VXCD. VXCD extends UML’s component diagram and adapts it to XCD’s structure, contractual behaviour, and interaction protocol specifications. Visual VXCD specifications can be translated into textual XCD specifications for formal analysis. To illustrate VXCD, the well-known gas station system is used. The gas system is specified contractually using VXCD’s visual notation set and then formally analysed using SPIN’s model checker for a number of properties including deadlock and race-condition.

Cryptographic protocol security analysis based on bounded constructing algorithm

An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message concurrent. We propose an efficient structures are complex and their executions are automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra （CPA） model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.

New Semantic Model for Authentication Protocols in ASMs

A new semantic model in Abstract State Model (ASM) for authentication protocols is presented. It highlights the Woo-Lam's ideas for authentication, which is the strongest one in Lowe's definition hierarchy for entity authentication. Apart from the flexible and natural features in forming and analyzing protocols inherited from ASM, the model defines both authentication and secrecy properties explicitly in first order sentences as invariants. The process of proving security properties with respect to an authentication protocol blends the correctness and secrecy properties together to avoid the potential flaws which may happen when treated separately. The security of revised Helsinki protocol is shown as a case study. The new model is different from the previous ones in ASMs.

Ontology-Based Model of Network and Computer Attacks for Security Assessment

With increased cyber attacks over years,information system security assessment becomes more and more important.This paper provides an ontology-based attack model,and then utilizes it to assess the information system security from attack angle.We categorize attacks into a taxonomy suitable for security assessment.The proposed taxonomy consists of five dimensions,which include attack impact,attack vector,attack target,vulnerability and defense.Afterwards we build an ontology according to the taxonomy.In the ontology,attack related concepts included in the five dimensions and relationships between them are formalized and analyzed in detail.We also populate our attack ontology with information from national vulnerability database(NVD)about the vulnerabilities,such as common vulnerabilities and exposures(CVE),common weakness enumeration(CWE),common vulnerability scoring system(CVSS),and common platform enumeration(CPE).Finally we propose an ontology-based framework for security assessment of network and computer systems,and describe the utilization of ontology in the security assessment and the method for evaluating attack efect on the system when it is under attack.

Topic-Feature Lattices Construction and Visualization for Dynamic Topic Number

The topic recognition for dynamic topic number can realize the dynamic update of super parameters,and obtain the probability distribution of dynamic topics in time dimension,which helps to clear the understanding and tracking of convection text data.However,the current topic recognition model tends to be based on a fixed number of topics K and lacks multi-granularity analysis of subject knowledge.Therefore,it is impossible to deeply perceive the dynamic change of the topic in the time series.By introducing a novel approach on the basis of Infinite Latent Dirichlet allocation model,a topic feature lattice under the dynamic topic number is constructed.In the model,documents,topics and vocabularies are jointly modeled to generate two probability distribution matrices:Documentstopics and topic-feature words.Afterwards,the association intensity is computed between the topic and its feature vocabulary to establish the topic formal context matrix.Finally,the topic feature is induced according to the formal concept analysis(FCA)theory.The topic feature lattice under dynamic topic number(TFL DTN)model is validated on the real dataset by comparing with the mainstream methods.Experiments show that this model is more in line with actual needs,and achieves better results in semi-automatic modeling of topic visualization analysis.

Cooperative Answering of Fuzzy Queries

The majority of existing information systems deals with crisp data through crisp database systems. Traditional Database Management Systems （DBMS） have not taken into account imprecision so one can say there is some sort of lack of flexibility. The reason is that queries retrieve only elements which precisely match to the given Boolean query. That is, an element belongs to the result if the query is true for this element; otherwise, no answers are returned to the user. The aim of this paper is to present a cooperative approach to handling empty answers of fuzzy conjunctive queries by referring to the Formal Concept Analysis （FCA） theory and fuzzy logic. We present an architecture which combines FCA and databases. The processing of fuzzy queries allows detecting the minimal reasons of empty answers. We also use concept lattice in order to provide the user with the nearest answers in the case of a query failure.

Subposition Assembly-Based Construction of Non-Frequent Concept Semi-Lattice

An efficient way to improve the efficiency of the applications based on formal concept analysis （FCA） is to construct the needed part of concept lattice used by applications. Inspired by this idea, an approach that constructs lower concept semi-lattice called non-frequent concept semi-lattice in this paper is introduced, and the method is based on subposition assembly. Primarily, we illustrate the theoretical framework of subposition assembly for non-frequent concept semi-lattice. Second, an algorithm called Nocose based on this framework is proposed. Experiments show both theoretical correctness and practicability of the algorithm Nocose.