检索结果-南通市图书馆

A Novel formal analysis Method of Network Survivability Based on Stochastic Process Algebra

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Tsinghua Science and Technology 2007年第S1期12卷 175-179页

作者：赵国生王慧强王健 Center of Computer Network and Information Harbin Normal University Institute of Computer Science and Technology Harbin Engineer UniversityHarbin 150001China Institute of Computer Science and Technology Harbin Engineer University

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.

关键词： formal analysis stochastic process algebra network survivability performance analysis

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

在线全文

学校读者我要写书评

暂无评论

Computer Modeling in Engineering & Sciences 2024年第3期138卷 2641-2663页

作者： Ke Yang Meihua Xiao Zehuan Li School of Electrical Engineering and Automation East China Jiaotong UniversityNanchang330013China School of Software East China Jiaotong UniversityNanchang330013China

Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure *** protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network *** 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 *** proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of *** definition accurately captures the inherent requirements of fair exchange *** upon event logic,the model incorporates the time factor into predicates and introduces knowledge set *** enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired *** maximize the intruder’s capabilities,channel errors are translated into the behaviors of the *** participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential *** employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol *** entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding *** 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.

关键词： Fair exchange protocols fairness formal analysis logic reasoning

A Novel Approach to Automatic Security Protocol analysis Based on Authentication Event Logic

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2015年第1期24卷 187-192页

作者： XIAO Meihua MA Chenglin DENG Chunyan ZHU Ke School of Software East China Jiaotong University

Since security protocols form the cornerstones of modern secure networked systems, it is important to develop informative, accurate, and deployable approach for finding errors and proving that protocols meet their security requirements. We propose a novel approach to check security properties of cryptographic protocols using authentication event logic. Compared with logic of algorithm knowledge, authentication event logic guarantees that any well-typed protocol is robustly safe under attack while reasoning only about the actions of honest principals in the protocol. It puts no bound on the size of the principal and requires no state space enumeration and it is decidable. The types for protocol data provide some intuitive explanation of how the protocol works. Our approach has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.

关键词： Security protocols formal analysis Authentication event logic.

Visual Specification and analysis of Contract-Based SoftwareArchitectures

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2017年第5期32卷 1025-1043页

作者： Mert Ozkaya Department of Computer Engineering Istanbul Kemerburgaz University Istanbul 34217 Turkey

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.

关键词： architectural language design-by-contract visual modelling language interaction protocol formal analysis

Algebra model and security analysis for cryptographic protocols

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science in China(Series F) 2004年第2期47卷 199-220页

作者： HUAIJinpeng LIXianxian SchoolofComputer BeijingUniversityofAeronauticsandAstronauticsBeijing100083China

More and more cryptographic protocols have been used to achieve various security requirements of distributed systems in the open network environment. However cryptographic protocols are very difficult to design and analyze due to the complexity of the cryptographic protocol execution, and a large number of problems are unsolved that range from the theory framework to the concrete analysis technique. In this paper, we build a new algebra called cryptographic protocol algebra (CPA) for describing the message operations with many cryptographic primitives, and proposed a new algebra model for cryptographic protocols based on the CPA. In the model, expanding processes of the participants knowledge on the protocol runs are characterized with some algebraic notions such as subalgebra, free generator and polynomial algebra, and attack processes are modeled with a new notion similar to that of the exact sequence used in homological algebra. Then we develope a mathematical approach to the cryptographic protocol security analysis. By using algebraic techniques, we have shown that for those cryptographic protocols with some symmetric properties, the execution space generated by an arbitrary number of participants may boil down to a smaller space generated by several honest participants and attackers. Furthermore we discuss the composability problem of cryptographic protocols and give a sufficient condition under which the protocol composed of two correct cryptographic protocols is still correct, and we finally offer a counterexample to show that the statement may not be true when the condition is not met.

关键词： cryptographic protocol formal analysis information security algebra system.

Cryptographic protocol security analysis based on bounded constructing algorithm

在线全文

学校读者我要写书评

暂无评论

Science in China(Series F) 2006年第1期49卷 26-47页

作者： LI Xianxian HUAI Jinpeng School of Computer Beihang University Beijing 100083 China

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.

关键词： cryptographic protocol formal analysis security verification.

Security analysis of an Electronic Commerce Protocol Using Casper/FDR2

在线全文

学校读者我要写书评

暂无评论

Wuhan University Journal of Natural Sciences 2012年第6期17卷 499-503页

作者： CHANG Yinlong HU Huaping Department of Mathematics and Computer Science/Key Laboratory of Information Security of Network System Fuzhou UniversityFuzhou 350108FujianChina School of Computer Science National University of Defense TechnologyChangsha 410073HunanChina

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

关键词： Casper FDR2 electronic commerce model checking formal analysis

New Semantic Model for Authentication Protocols in ASMs

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2004年第4期19卷 555-563页

作者： RuiXue Deng-GuoFeng StateKeyLaboratoryofInformationSecurity InstituteofSoftwareTheChineseAcademyofSciencesBeijing100080P.R.China

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.

关键词： cryptographic protocol formal analysis abstract state machine (ASM) authentication protocol

Cursor caging:enhancing focus targeting in interactive fisheye views

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2013年第5期56卷 115-130页

作者： SONG HongZhi FU Yi ZHANG Liang ZHANG XiaoLong(Luke) College of Informatics South China Agricultural University College of Information Sciences and Technology Pennsylvania State University307D IST BuildingUniversity ParkPA 16802USA

Fisheye view is an effective approach to visualizing and navigating large data sets by offering both local details and global context in the same ***,by using different magnification factors for detail and context information,fisheye view also leads to new usability issues,one of which is the focus targeting *** challenge happens when a user tries to select a target to either shift the focus to a new place or chooses the *** of the magnification factors applied to the fisheye view,the target moves when the cursor moves,and consequently,the moving distance the cursor actually needs to travel to reach the target does not match the distance between the cursor and target shown on the *** accuracy and efficiency can be *** paper analyzes the mechanism of this difficulty and proposes a new technique,cursor caging,as a method to alleviate the focus targeting difficulty in interactive fisheye *** technique extends the fisheye magnification approach from one element to a focal region,which can contain several elements,and allows the mouse cursor to move freely inside this region without affecting the magnification of objects inside the focal *** addition to the mathematical representation of this technique,we also develop two designs that incorporate the cursor caging concept in fisheye views,and describe a usability study on the *** results showed that cursor caging can significantly improve the task completion time and reduce the error rate in focusing targeting tasks.

关键词： fisheye view non-linear magnification focus targeting formal analysis cursor caging