We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoret...We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoretical analysis of our rules using the strand spaceformalism, and show the soundness of our idealization rules under strand spaces Some examples onusing the new rules to analyze security protocols are also concerned. Our idealization method ismore effective than Mao's method towards many protocol instances, and is supported by a formalmodel.展开更多
Due to their resource constraints,Internet of Things(IoT)devices require authentication mechanisms that are both secure and efficient.Elliptic curve cryptography(ECC)meets these needs by providing strong security with...Due to their resource constraints,Internet of Things(IoT)devices require authentication mechanisms that are both secure and efficient.Elliptic curve cryptography(ECC)meets these needs by providing strong security with shorter key lengths,which significantly reduces the computational overhead required for authentication algorithms.This paper introduces a novel ECC-based IoT authentication system utilizing our previously proposed efficient mapping and reverse mapping operations on elliptic curves over prime fields.By reducing reliance on costly point multiplication,the proposed algorithm significantly improves execution time,storage requirements,and communication cost across varying security levels.The proposed authentication protocol demonstrates superior performance when benchmarked against relevant ECC-based schemes,achieving reductions of up to 35.83%in communication overhead,62.51%in device-side storage consumption,and 71.96%in computational cost.The security robustness of the scheme is substantiated through formal analysis using the Automated Validation of Internet Security Protocols and Applications(AVISPA)tool and Burrows-Abadir-Needham(BAN)logic,complemented by a comprehensive informal analysis that confirms its resilience against various attack models,including impersonation,replay,and man-in-the-middle attacks.Empirical evaluation under simulated conditions demonstrates notable gains in efficiency and security.While these results indicate the protocol’s strong potential for scalable IoT deployments,further validation on real-world embedded platforms is required to confirm its applicability and robustness at scale.展开更多
Ad hoc移动网络路由协议为加强其安全性,采用了密码技术,使其成为安全协议的一种。这使得采用形式化的方法分析其安全性成为可能。考虑ad hoc移动网络路由协议的特点,采用BAN逻辑对协议的安全性进行描述,提出了协议应满足的条件。并对...Ad hoc移动网络路由协议为加强其安全性,采用了密码技术,使其成为安全协议的一种。这使得采用形式化的方法分析其安全性成为可能。考虑ad hoc移动网络路由协议的特点,采用BAN逻辑对协议的安全性进行描述,提出了协议应满足的条件。并对协议的运行过程进行了形式化,给出具体的分析方法。采用该方法对安全路由协议SADSR进行了安全验证,说明方法的有效性。展开更多
文摘We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoretical analysis of our rules using the strand spaceformalism, and show the soundness of our idealization rules under strand spaces Some examples onusing the new rules to analyze security protocols are also concerned. Our idealization method ismore effective than Mao's method towards many protocol instances, and is supported by a formalmodel.
文摘Due to their resource constraints,Internet of Things(IoT)devices require authentication mechanisms that are both secure and efficient.Elliptic curve cryptography(ECC)meets these needs by providing strong security with shorter key lengths,which significantly reduces the computational overhead required for authentication algorithms.This paper introduces a novel ECC-based IoT authentication system utilizing our previously proposed efficient mapping and reverse mapping operations on elliptic curves over prime fields.By reducing reliance on costly point multiplication,the proposed algorithm significantly improves execution time,storage requirements,and communication cost across varying security levels.The proposed authentication protocol demonstrates superior performance when benchmarked against relevant ECC-based schemes,achieving reductions of up to 35.83%in communication overhead,62.51%in device-side storage consumption,and 71.96%in computational cost.The security robustness of the scheme is substantiated through formal analysis using the Automated Validation of Internet Security Protocols and Applications(AVISPA)tool and Burrows-Abadir-Needham(BAN)logic,complemented by a comprehensive informal analysis that confirms its resilience against various attack models,including impersonation,replay,and man-in-the-middle attacks.Empirical evaluation under simulated conditions demonstrates notable gains in efficiency and security.While these results indicate the protocol’s strong potential for scalable IoT deployments,further validation on real-world embedded platforms is required to confirm its applicability and robustness at scale.
