网络取证协议：识别网络犯罪来源及数字证据

沙特国王大学学报识别网络犯罪真实来源的网络取证调查协议Rachana Y.放大图片创作者：Patila，Satish R.德瓦恩湾aA.C.Patil College of Engineering，Kharghar，410210 Navi Mumbai，IndiabDatta Meghe College of Engineering，Airoli，400708 Navi Mumbai，India阿提奇莱因福奥文章历史记录：收到2019年2019年11月20日修订2019年11月30日接受在线提供2019年关键词：网络取证网络犯罪数字证据设备指纹AVISPA安全攻击A B S T R A C T数字化程度的提高导致了网络犯罪。现有的网络协议不足以收集网络犯罪所需的数字证据，这最终使法医调查过程变得困难。在当前的网络取证场景中，具有当前能力的调查人员只能到达ISP。这不是主要证据。目前，可用的工具仅在网络层工作在这项工作中，我们提出了一个协议，确保跟踪到真正的来源，事先收集-ING法医健全的证据。所提出的协议可以在代理进程的帮助下以设备指纹的形式从设备收集目标数据。拟议的方法将有助于证明不可否认性，这是法证案件中众所周知的挑战。该方法生成的指纹证据具有在犯罪分子试图销毁证据时不被废弃的能力。所部署的指纹识别技术使用哈希树，并以这种方式生成证据，该指纹可以作为法律证据。所提出的系统的安全性验证是使用BAN逻辑。使用AVISPA工具进行正式验证。该系统已实现为原型，并托管在AWS上。©2019作者由爱思唯尔公司出版代表沙特国王大学这是一个开放的访问CC BY-NC-ND许可证下的文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍数字化的快速发展正在引发网络犯罪。Cyber security Ventures预测，到2022年将有60亿互联网用户，到2030年将有75亿互联网用户（Morgan，2017）。根据国家犯罪记录局（NCRB）的数据，迄今为止登记的网络犯罪案件数量超过了逮捕人数（印度犯罪，2018年）。主要原因是缺乏针对犯罪分子的法律证据。收集的证据不符合法院规定的特征，其中大多数数字取证调查都停留在边缘路由器或攻击者的ISP上。许多技术使用攻击者的公共IP来跟踪攻击者，而在真实的场景中，ISP背后有一个巨大的网络，攻击者隐藏在背后（Patil和Devane，2017）。它成为一项重要的任务*通讯作者。电子邮件地址：rachana.y. gmail.com（R.Y. 帕蒂尔）。沙特国王大学负责同行审查制作和主办：Elsevier让调查员确定攻击的确切来源确定确切的来源还需要ISP的大力合作，但作为ISP之间的竞争对手，ISP不愿意在调查过程中合作（Yao等人，2015年）。此外，互联网服务供应商所保存的日志资料的保安问题亦备受关注。没有这种机制可用来核实ISP数据的完整性。司法证据是司法鉴定的重要组成部分。注重证据的真实收集和保存，是提高证据在法庭上的可接受性的需要。为了从网络中收集法医学上可靠的证据，我们需要收集有关网络设备的更详细的信息，这将有助于开发支持法医调查的准确技术。目前，大多数现有的网络协议携带路由目的和内容安全所需的信息。这些信息（如IP地址或端口号）只能帮助识别攻击者的边缘路由器或ISP，而不是用于尝试网络犯罪的确切设备（Patil和Devane，2017）。这些信息不能在法庭上用作证据。这不足以进行法医分析和调查。拟议的证据收集程序通过具体载列调查所需的详细资料而不干扰现有程序的原有功能来应对这一挑战。https://doi.org/10.1016/j.jksuci.2019.11.0161319-1578/©2019作者。由爱思唯尔公司出版代表沙特国王大学这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。可在ScienceDirect上获得目录列表沙特国王大学学报杂志首页：www.sciencedirect.com2032R.Y.公司Patil，S.R.Devane/ Journal of King Saud University为了超越ISP来识别网络犯罪的原始来源，我们提出的系统使用了设备指纹的概念。设备指纹的想法先前被各种应用使用，如用户识别和跟踪、软件许可和盗版保护（Kohno等人，2005年）。但这些应用程序生成的指纹并不满足证据的所有特征，因此不适合用作法医调查中的证据。所提出的设备指纹识别方法是生成满足所有证据要求的设备指纹，并可以在法庭上作为证据使用。1.1. 研究贡献本文的贡献是多方面的：提出了一种新的设备指纹采集安全协议，该协议将有助于网络取证调查。拟议中的协议将收集设备的指纹前手，可以作为法律证据，在法庭上，如果出现任何争议。该协议还实现了公平的不可否认性，这是证明证据的最高要求。所提出的设备指纹算法可以通过使用哈希树的概念从设备参数生成设备指纹。该算法生成的设备指纹具有较强的鲁棒性，满足印度证据法规定的所有法定证据特征。它还提供了部分核实证据的特点非正式的安全性分析所提出的系统提供了检查其鲁棒性对可能的已知的攻击，如非法内部攻击，会话劫持攻击等。形式化的安全性分析使用广泛使用的BAN逻辑表明，所提出的协议提供了安全性和实现不可否认性。使用AVISPA工具进行的形式化安全验证表明，该协议具有抵抗重放攻击和中间人攻击的能力。最后，通过在Java中实现并使用JNLP，展示了所提出的方法的实际演示该系统是通过使用广泛使用的亚马逊网络服务（AWS）部署和托管。1.2. 纸结构第2节中给出了对相关现有方案的讨论。在第3节中，讨论了拟议方案的特征以及假设。与所提出的系统及其详细描述相关的各个阶段，并提出了设备指纹识别算法进行了讨论。第4节对拟议方法进行了细致的非正式安全分析。第5节讨论了使用BAN的协议分析。在第6节中，使用互联网安全协议和应用程序自动验证（AVISPA）工具对所提出的协议进行了正式验证。实验评估和系统架构在第7中进行了演示。最后，我们将在第8中结束我们的工作。2. 相关工作网络安全是保护连接到互联网的系统或设备免受网络攻击或网络盗窃。而网络取证则是在网络犯罪发生过程中或发生后，从网络设备追踪网络犯罪的原始设备是网络法医调查的首要目标（Kim等人，2015年）。这些技术被广泛称为追溯方法。根据（Akyuz和Sogukpinar，2009），追溯是一种适当的网络取证技术，用于通过调查攻击踪迹来发现数据包的来源。各种基于回溯的方法都有自己的优点和局限性。基于分组标记的方法在（Liu等人，2018年; Yu等人，2016; Cheng等人，2014; Alenezi和Reed，2014;Tian等人，2013年）。大多数方法都是主动的，只有在攻击完成后才能找到攻击的来源。在大多数情况下，这种标记策略使用分组报头的字段来嵌入证据数据。 用于受害者分组标记方法的存储器容量相对较高，需要在受害者一方存储大量的证据包以评估和检索准确的源信息。重要的是，这些方法是灵活的和可部署的。但许多解决方案允许ISP高度参与。在（Yao et al.，2015;Saurabh和Sairam，2014; Cheng等人，2012; Guerid等人，2011; Wang和Schulzrinne，2004）大多是反应性的。在检测到攻击后，可以立即触发查找攻击来源的过程。大多数技术都使用TCP协议。一些技术使用专门设计的消息来发送有关证据的信息。在这种方法中，受害者和网络的数据开销是微不足道的。它可以轻松地在大型网络中实施和扩展这些解决方案。然而，基于消息传递的技术的缺点是消息会产生额外的网络流量.在（ Aghaei-Foroushani 和 Zincir-Heywood ， 2016; Alenezi 和Reed，2013;Tian等人，2012; Tian和Bi，2012）利用自动系统到达确切的入侵者。对于这样的技术，这些自治系统的覆盖网络被建立，并且自治系统之间需要高度合作。回溯性能取决于覆盖网络中涉及较高的数值对应于准确的结果。基于叠加的解决方案本质上是反应性的，与其他方法相比，ISP的参与程度这些技术已经被许多研究人员提出，使用BGP作为底层协议。很少有技术是基于OSFP协议的。覆盖网络方法具有良好的可扩展性在（Fadel等人，2016; Jeong和Lee，2014; Yang，2012; Malliga和Tamilarasi，2008）是两种或多种回溯技术的组合。通过结合所需的方法，可以减少内存需求和存储需求。混合技术响应迅速，允许单个数据包定位攻击源。在传输过程中，许多混合回溯的作者都注意到了数据的安全性。大多数研究者将数据包标记和基于日志的回溯技术相结合。然而，在这些识别攻击的真正来源的追溯技术中，生成证据并将其转发给攻击的受害者是最关键的任务。大多数将证据信息发送给受害者的方法都使用了一些IP报头字段。证据信息被嵌入在IP报头中。在数据包的传输过程中，并非IP报头中的所有字段都始终被使用。大多数现有的跟踪方法都使用这些未使用的字段在IP报头中嵌入标记信息。（Vasseur等人，（2015年）然而，从公共网络收集跟踪攻击者源系统所需的数据会增加网络的主要开销，并且在查找攻击源方面不是很有效（Belenky和Ansari，2003年）●●●●R.Y.公司Patil，S.R.Devane/ Journal of King Saud University2033使用网络流量作为收集证据的来源有很大的局限性，因为缺乏专门的工具，可用于分析大量的交通从法医的角度（凯西，2004年）。多年来，人们提出了许多不同方法的网络取证技术来收集网络犯罪证据。Pilli et al.，2010年）。这些作者还根据调查方法将网络取证技术分为不同类型。所有调查的主要目的是找出法院将接受的针对攻击者的法律证据。在基于网络流量模式检测可疑活动之后收集证据的框架在（Divakaranet al.，2017年）。在这项工作中，流量模式被用作证据来证明恶意活动或攻击。最可靠的证据是找到攻击的确切来源。识别用于网络犯罪的器械是最相关的证据（Patil和Devane，2017）。然而，这些源识别技术的关键方面是，它们可以到达攻击者的ISP。为了识别网络犯罪的确切来源，第一个要求是唯一识别网络中存在的每个设备（Patil和Devane，2018），以便设备身份可以用作证据。计算机等电子设备也具有唯一的数字指纹，可以用来正确识别它们。现有 的 设 备 指 纹 技 术 （ Blakemore例 如 ， 2016; Takeda ， 2012;François等人，（2011）利用如果系统被格式化或安装了新的操作系统，这些操作系统特定参数将很容易使指纹无效。然而，器件指纹印刷的一些技术（Lanze等人，2012; Arackaparambil等人，2010; Huang等人，2012）正在使用设备时钟偏移作为唯一标识符。然而，基于时钟偏斜的方法具有诸如易受时钟偏斜欺骗的缺点。此外，由于时钟偏差是使用传出TCP数据包中的时间戳选项测量的，因此如果设备禁用了该选项，则无法执行测量。这种指纹技术不足以用于法医调查。在上述工作的背景下，网络取证调查中最关键的一步是找到网络犯罪的真实来源并收集攻击的证据。现有的方法只能到达攻击者的第一个边缘路由器。由于取证证据是取证调查的关键组成部分，因此仅到达边缘路由器是没有帮助的。现有的网络协议都是只考虑网络流量而设计的。目前，还没有将袭击者的证据送交受害者进行法医调查的计划。要超越这一点，到达攻击者的确切系统仍然是一个巨大的挑战。3. 拟议议定书框架数字证据在法院证明网络犯罪中起着非常关键的作用。在大多数情况下，证据是在犯罪发生后收集的。在这样的调查中，攻击者有足够的时间销毁证据或掩盖铁轨除此之外，死亡取证是一个耗时和昂贵的程序。收集的证据的可靠性和使用的方法是值得怀疑的，往往是在法庭上不可接受的。建议的证据收集程序旨在收集有关客户的足够资料，以便日后出现任何争议时，可作为呈堂证据。该协议的主要目的是帮助法医调查过程，并减少所需的时间和资源所提出的协议的特点如下秘密收集法庭上可以接受的关于网络犯罪的可靠证据。在不使用可信第三方的情况下实现了不可否认性。器械指纹识别算法生成的证据在法医学上是可靠的。拟议的议定书还尽量减少调查期间所需的ISP或任何其他第三方如图1所示的所提出的系统工作如下1. 代理进程在服务器端准备2. 认证完成后，通过嵌入HTML页面的方式将代理部署到客户端.3. 代理进程从目标客户端获得执行的同意图1. 拟议的议定书框架。●●●2034R.Y.公司Patil，S.R.Devane/ Journal of King Saud University4. 如果客户端同意，代理将在客户端机器上执行并收集所需的指纹参数。5. 然后将参数安全地传输到服务器。6. 服务器执行设备指纹算法并生成客户端机器的唯一指纹。7. 指纹安全地存储在服务器端，以便在需要进行法医调查时进行进一步验证。假设。该协议假设存在一个已建立的公钥基础设施（PKI），其中所有参与的实体都已经发布了它们的密钥，并且其余实体。在所提出的方法中，客户端和服务器之间的消息交换如图2所示。一旦客户端提交凭证并且认证成功，服务器就激活代理以从客户端设备收集数据，以便生成指纹。在进行法医调查时，为指纹生成收集的数据是必要的。协议解释分为以下两个阶段3.1. 拟议系统阶段1：基于代理的指纹参数采集为了从客户端设备收集指纹数据，需要在客户端机器上执行代理进程。的Java图二. 拟议方法的详细说明。R.Y.公司Patil，S.R.Devane/ Journal of King Saud University2035使用在客户机上执行的网络启动协议（JNLP）。指纹参数被安全地收集并发送到服务器。JNLP的详细描述将在后面的章节中给出。阶段2A：用于传输指纹参数的协议需要通过实现不可否认性将收集的指纹参数安全地传输到服务器。以下步骤指纹参数传输协议如下。客户端生成对称密钥K（在另一节中解释）使用秘密密钥K加密参数数据。Ek（数据）生成时间戳Tc，并将客户端身份C和时间戳Tc附加到加密数据，使用客户端私钥对消息进行数字签名符号c[C，Tc，Ek（数据）]在服务器端，服务器将使用客户端的公钥验证签名由于数据是用密钥K加密的，服务器将无法访问数据。服务器将保留上述消息作为来源不可否认的证明。作为上述消息的接收，服务器将把自己的身份和时间戳附加到加密数据中，并使用自己的身份和时间戳对其进行签名。私钥。符号s[S，Ts，Ek（数据）]收到上述消息后，客户端将使用服务器的公钥验证签名客户端使用服务器的公钥加密密钥，并将身份和时间戳附加到加密的密钥中，并在数字签名后将其发送给服务器。符号c[C，Tc，Es_pub（K）]服务器将使用自己的私钥验证签名并解密密钥。Ds_pvt[E s_pub（K）] = K服务器现在可以使用对称密钥解密数据。Dk [Ek（数据）] =数据服务器现在将执行指纹识别算法以生成客户端机器的设备指纹FP，并将其与参数一起存储在数据库中。阶段2B：重新获取指纹参数在事务完成之后，客户端将再次生成时间戳Tc，并将客户端身份C和时间戳Tc附加到加密数据，并通过使用客户端私钥对消息进行数字签名符号c[C，Tc，Ek（数据）]服务器现在可以使用对称密钥解密数据Dk [Ek（数据）] =数据再次执行指纹识别算法以使用Data'生成客户端机器的设备指纹FP● 如果FP = FP阶段2B的目的是保护系统免受认证会话劫持攻击。在这个阶段，指纹数据可以在交易结束后收集。另一种解决方案可以是定期收集数据3.2. 对称密钥（K）的生成所提出的对称密钥生成过程在图3中解释。从客户端机器提取的参数的加密需要对称密钥。密钥的大小取决于基础对称密钥算法，例如，DES为64位，AES为128、192和256位，IDEA为128位。对称密钥由设备参数本身生成。首先，所有密钥生成参数被划分为K/4比特的相等大小的块。如果最后一个块小于K/4，则附加填充位以使其成为K/4位。使用随机函数从所有参数中随机考虑一个K/4比特块。追加所有4个K/4位的块并生成对称密钥的K位。3.3. 指纹生成算法通过考虑数字证据的必要性，开发了设备指纹识别方法。数字证据的基本要求是其在法庭上的可接受性。它应该是准确的收集，和完整性和真实性图三. 对称密钥生成过程。●●●●●●●●●●●2036R.Y.公司Patil，S.R.Devane/ Journal of King Saud University见图4。 指纹识别方法。才能令人信服地判决案件为了满足证据的所有这些特征，所提出的指纹识别方法使用了哈希树的思想。哈希树的概念最初是由Merkle（1987）的作者提出的。散列树的每个叶节点保存一个指纹参数（例如，H（MP）保存主板指纹的哈希值图4所示的指纹生成算法如下工作。考虑从被指纹识别客户端设备接收的各个指纹识别参数。通过计算每个指纹参数（级别0）通过连接指纹参数散列对（级别0）创建级别1节点，并再次对结果信息进行散列（水平）1)在哈希树中向上移动使用从较低级别新生成的散列重复该过程，直到整个数据有一个散列摘要。在第3级树的根部，我们得到一个哈希值，我们称之为设备指纹。4. 拟议方法对协议的非正式安全性分析保证了该方案能够抵抗以下已知的安全攻击。4.1. 该协议具有抵抗重放攻击的安全性该协议能够抵抗重放攻击。入侵者可能试图窃听消息，并在随后的会话中将其发送到服务器。该协议在客户端和服务器端发送的每一条消息中使用时间篡改，通过检测传输时间的延迟来抵抗应答攻击。假设入侵者i已经截获了从一个入侵者到服务器{（C，Tc，（Data）k）Kps}Kpc-1的消息。对于入侵者来说，要改变时间戳，他必须实时解决离散对数问题，这是困难的。因此，它将导致传输延迟，这将在服务器端被检测到，并且消息将被拒绝。4.2. 该协议对中间人攻击是安全的假设入侵者i截取消息{（C，Tc，（Data）k）Kps}Kpc- 1，并试图通过改变设备参数（Data）k来修改该消息。在这种情况下，即使入侵者试图用（Data ′）k ′替换整个项（Data）k，他也不会成功，因为要替换一个由于客户端的公钥已知，每个入侵者都可以做到这一点，并访问消息（C，Tc，（Data）k）Kps。为了修改数据，入侵者必须再次解密使用服务器公钥加密的消息，这是不可能的。即使入侵者试图替换整个项（C，Tc，（Data）k并试图使用服务器的公钥加密如果消息没有被客户端签名，它将在服务器端被拒绝。这表明，该协议是弹性的人在中间攻击4.3.该协议是安全的，可以抵抗内部攻击即使服务器是可信实体，服务器的内部用户也假设i想要滥用在客户端C的某个合法事务如果不知道客户端的私钥，入侵者将无法生成这样的每次从客户端的机器捕获数据因此，找到客户端的私钥在计算上是不可行的因此，所提出的协议对于这种攻击4.4.该协议能抵抗会话劫持攻击在会话劫持攻击中，入侵者将访问客户端和服务器之间的会话。会话劫持最常见的方式是在身份验证过程结束后。在所提出的协议中，当代理进程部署在客户机上时，它捕获数据，客户机发送消息{(C，Tc，（Data）k）Kps}Kpc-1发送到服务器。来自客户端的数据是客户端设备的唯一标识。在会话劫持中，设备将发生变化，当服务器试图从客户端机器捕获数据时，它将获得与前一个不匹配的不同数据。这种数据在一个单一的会话中的不匹配将引起警报，这证明了我们提出的协议是弹性的会话劫持攻击。4.5. 所提出的协议提供密钥新鲜度该方案保证了客户端和服务器端之间密钥的新鲜性。每次数据从客户端发送到服务器时，它都由客户端在运行时使用其参数生成的密钥加密。在前面的第三节中解释了密钥的生成。即使相同的客户端向服务器发送相同的数据，由于过程的随机性，生成的密钥也会不同。因此，在每个会话中，生成唯一且新鲜的密钥。4.6. 提出的协议是安全的，可以抵抗拒绝服务攻击该协议要求每个客户端在访问服务器上的资源之前进行基于密码的身份验证因此，拒绝服务攻击很难尝试。●●●●●●R.Y.公司Patil，S.R.Devane/ Journal of King Saud University2037Jj）ð ÞQP$4.7. 该协议实现了不可否认性在阶段2期间，在将指纹参数安全地发送到服务器的同时，应实现不可否认性，因为交易争议是商业世界中的常见问题为了公平地解决争议，交易双方都应该有足够的证据证明交易的在基本交易中出现的典型争议如下。4.7.1. 服务器声称它从客户端接收到数据，而客户端否认发送了数据起源的不可否认性（NRO）的特征是一种安全服务，以保护系统免受发件人为了提供来源的不可否认性，作为发送者向接收者发送消息的证据，发送者在向接收者发送消息时，应该使用发送者的私钥对内容进行数字签名为了证明来源的不可否认性，消息的接收者必须能够提供足够的证据证明签名是由发送者生成在接收到签名的消息后，接收方可以验证消息是否由签名的。发送者。如果使用公钥对签名进行验证，则证明了源的不可否认性。例如：。客户端将指纹参数发送到服务器。指纹参数在图1B上被示出为叶节点。3.第三章。在该消息中，客户端首先使用由客户端生成的秘密密钥K对数据进行加密，然后将时间戳Tc和客户端的身份C附加C：生成KC：E k（数据）||T c||CS->C：符号s[S，T s，E k（数据）]= E Ks_pvt[E k（数据）||T s||S]客户端收到此消息后，可以使用服务器的公钥验证签名。C：符号s[S，Ts，Ek（数据）]C：验证签名D Ks_pub [E Ks_pvt [E k（数据）||T s||S]]如果使用服务器公钥成功验证了签名，则客户端信任该消息是由服务器发送的这可以提供收据5. 使用BAN逻辑进行在部署这一创新的安全协议之前，必须确保这些协议正确运行。安全协议中的缺陷所造成的损害可能是灾难性的。 分析密码安全协议的常规方法（Rubin和Honeyman，（1993）“Formal”）基本上始于Bur rows、Abadi和Needham（BAN）逻辑（Burrows等人，1990年）。协议的形式化分析是发现协议缺陷的基本要求。协议分析的形式化方法也被称为信念逻辑用于形式化协议分析的BAN逻辑的基本原理是解释协议消息、解释和验证协议是否满足预期目标。如果我们能够推导出定义目标的证明，分析就会得出结论。5.1. BAN逻辑BAN逻辑包括如下预定义的符号。P XP相信陈述X是正确的。PXP接收到包含X的消息，并且P可以看到语句X。P X P曾经说过X。P在某个时间发送了报表X。当P说X时P XP对X有管辖权。或P控制X，并对X具有作者身份，应被信任PKC->S：签名 [C，T，E（数据）] = E[E（数据）||不|| C]K是P和Q之间的共享密钥CcKkc_pvtK C声明X用K加密。钥匙不太好-服务器收到该消息后，可以使用客户端的公钥验证签名S：接收符号c[C，Tc，Ek（数据）]S：验证签名D Kc_pub [E Kc_pvt[E k（数据）||T c||C]]如果使用客户端公钥成功验证了签名，则确认该消息是由客户端发送的这可以为原产地5.1.1. 客户端声称已将数据发送到服务器，而服务器否认已收到数据接收不可否认性（NRR）的特点是作为一种安全服务，以确保接收者不会错误地拒绝接收消息。它保护系统不受接收者错误地拒绝接收消息的企图的影响。为了提供收据的不可否认性作为证据，接收者应该使用接收者的私钥对通过附加用密钥、时间戳和接收者的身份加密的数据而生成的收据进行数字签名例如：。在接收到加密格式Ek（Data）的指纹参数（Data）之后，服务器必须将其连同它的缺点和优点。-X X是新创建的，在当前时间之前没有在消息中发送。K你好！QK q iapubluckeyofQ;私钥是K q-1PX Q X是P和Q5.2. BAN逻辑下面描述协议分析所需的BAN逻辑中的推理规则5.2.1. 消息意义规则MM1：（消息表示对称密钥的规则）如果P相信P之间的j <$Qj~ XQ是K，如果P可以看到用K加密的消息X，那么P相信X是由Q发送的MM2：（消息表示公钥规则）PK服务器服务器必须使用服务器的私钥对此收据进行数字签名在此步骤中，服务器无法访问由密钥加密的原始数据。这是一个证明从服务器（S）到客户端（C）的S：E k（数据）||T s||Sjj！如果P相信K是用户Q的公钥并且PPj <$ Qj~ X如果P可以看到由私钥K-1签名的消息，则P相信X是由 Q发送的。MM3：（消息表示共享密钥的规则Pj <$ QYP;P <$XY如果P相信Y是P和QPj <$ Qj~ X如果P可以看到与Y连接的消息，则P相信X是由Q2038R.Y.公司Patil，S.R.Devane/ Journal of King Saud Universityj$.ΣCS$KC-15.2.2. NV：Nonce验证规则如果P相信X的新鲜度并且P相信Q一次，Pj Qj XX说，那么P相信Q相信X。5.2.3. JR：管辖权规则如果P相信Q相信X，并且P相信Q有欺诈行为，Pj X控制X（Q生成X），则P也相信X。5.2.4. 分解规则3. 服务器将在交换消息3之后接收密钥为公平交流数据，我们必须证明SData和S只有在交换消息3之后，数据才为真。所提出的协议由4个消息组成，因此有5个状态，因为S0是初始假设状态。状态显示了每个实体在时刻i的所见和所信信息。BAN逻辑中的状态概念首先由作者使用（Teepe，2008）。 消息的形式是Ci？ Si：Xi，意味着在时刻i，参与者C正在向参与者S发送消息，D1见分解规则P1 X;YPX参见X如果P能看见（X，Y），则P能消息的内容是X。在状态i交换消息之后，我们可以说Si<$ Xi。如果P相信新鲜度，Pj则P也相信（X，Y）的新鲜度D3信念分解规则Pj X;Y如果P相信（X，Y），则P在所提出的协议中，通信双方的状态关系上述证明表明，在服务器SS1的状态1中，在接收到也相信X。PjX从客户端发送消息1，服务器将通过SS0。在应用扩展公钥规则后，我们可以证明，5.2.5. EPK：扩展公钥规则S. 这意味着服务器可以看到fDatagK，但如果P相信X的新鲜度，如果P所Pj<$Q<$X;Y<$;Pj<$Qj<$ X;Z<$服务器不知道状态SS0中的密钥K;它不能解密消息。（X，Y），如果P可以看到用P的公钥加密的消息（X，Z），则P相信Q可以看到（X，Y），并且P也相信（X，Z）是由Q发送5.3. 拟议方案5.3.1. 使用BAN语法的信息1：C？ 史：n. CjNc;fDat agKKo圣人因此，服务器只能看到加密的内容，而不是原始数据。因此，我们可以说，“服务器认为客户端曾经说过f Dat a g K 0，因为消息是由客户端使用自己的私钥签名的，该私钥被认为是好的并且没有被泄露。NRO证明的推导如图所示。五、因此，服务器在Eq中的信念。(1)为真，服务器可将其用作不可否认性或来源的证明。上面的证明表明，在服务器CS2的状态2中，在接收到从服务器发送消息2，客户端将验证服务器信息2：S？ C：n。SjNc;NsfDatagKKCoKS-1应用消息意义规则和CS0.在应用扩展公钥规则后，我们可以证明，信息3：C？史：nCjNc;Ns;CK So信息4：S？C：nnSjNc;CK So oC-1CSjNc;NsfDatagK，这意味着客户端将取回fDatagK，在状态1中发送 客户将验证fDat agK和Nc 的正 确性。因此，我们可以说，5.3.2. 初始假设-KKS-1服务器曾经说fDatagK0，因为消息是由服务器使用其自己的私钥签名的NRR证明的推导如图6所示。因此，等式2中的客户端的信念为真，其可以被使用作为客户不可否认或已收到的证明。A1：CKs SA4：SKsSA7：Cj提到的是BAN逻辑的目标部分被导出为如下：j！A2：SKCj！KjN）A11：CK美元低点。 其推导如图1A和1B所示。 7和8Sj！CA5：Cc-1A8：Sj！（j）C$上述讨论证明，在所提出的协议中，A3：CKC CA6：SKs-1S A9：SjCj）CKS客户端和服务器都接收不可否认性证明，j！5.3.3. 目标j！$在解决争端时可以使用在原型的最后表1客户国G1：Cj CK S G2：Sj CK S G3：Cj Sj CK S G4：Sj Cj CK S- ----Client C Messages seen查看客户端C消息CS0KSKC5.4. 协议分析在所提出的协议中，我们必须证明服务器在交换消息3之前无法看到数据。对于公平的不可否认性，客户端应该首先接收服务器在发送密钥K以解密数据之前在gK处接收到数据的证明声明：服务器可以看到fDat agK，但在交换消息3之前无法看到{Data}。！ S，！ CCS1-CS2Nc;NsfDatagKNc;Ns;SjfDatagKCS3数据库CS4K Sj K表2服务器的状态Server S Messages seen服务器S消息这一说法是正确的，因为SS0KcC，KsS！啊！SSNc，fDatagKgK1. 服务器只能看到fDatagK1SS2Cj f数据E′，2. 密钥K由客户端SS3; 4C KS，数据C j KKSKR.Y.公司Patil，S.R.Devane/ Journal of King Saud University2039图五. 起源不可否认的推导见图6。 收据不可否认性的推导见图7。 目标4和目标2的推导。col run服务器成功地接收到由代理生成的秘密密钥，并相信它（见图1）。 9）。6. 基于AVISPA的协议形式化安全性验证互联网安全协议和应用的自动验证（AVISPA）是一种用于加密协议验证的自动化工具（AVISPA，2019; Armando等人，2005年）。AVISPA使用高级协议规范语言（HLPSL）（Oheimb，2005）来演示安全协议及其安全属性。HLPSL中指定的协议使用转换器HLPSL2IF转换为中间格式（IF）的低级语言。通过AVISPA的四个后弯分析安全协议的中间格式规范，以检查协议中指定的安全目标是否满足或违反。AVISPA提供了四个后端，它们是，基于约束逻辑的攻击搜索器（CLAtSe）、基于可满足性的模型搜索器（ SATMC ） 和 用 于 安 全 协 议 分 析 的 基 于 自 动 近 似 的 树 自 动 机（TA4SP）。Security Protocol Animator（Glouche等人，2006）forAVISPA（SPAN）是AVISPA的图形用户界面。它用于模拟加密协议。SPAN还将密码协议的CAS+规范（Saillard和Genet，2011）转换为HLPSL。入侵者模拟可以模拟协议与被动或主动攻击者的关系。如果存在对指定协议的攻击，则SAPN还在攻击模拟下模拟OFMC和CLAtSe的输出。6.1. HLPSL规范HLPSL规范包含三个部分。首先是角色的定义，其次是声明协议应该满足的安全目标。第三个是通过传递参数来实例化main角色。2040R.Y.公司Patil，S.R.Devane/ Journal of King Saud University见图8。 目标3的推导。表3HLPSL代码中使用的符号注释说明C客户端S服务器Kpc客户端公钥Kps服务器公钥Inv（Kpc）客户端私钥Inv（Kps）服务器私钥Hash（）单向哈希函数见图9。 客户角色。在所提出的协议的情况下，有两个基本角色，我们称之为客户端，是需要指纹识别的设备，服务器是指纹识别设备。每个基本角色都描述了参与者在开始时可以使用的信息（参数）、初始状态以及状态可以更改的方式（转换）。HLPSL 正 在 实 现 Doley-Yao 入 侵 者 模 型 （ Dolev 和 Yao ，1983），以验证对指定密码协议的中间人攻击和应答在这个模型中，假设入侵者可以窃听、捕获和创建任何消息客户端角色的HLPSL代码如图所示。8.第八条。HLPSL代码中使用的注释见表3。当客户端接收到状态0的启动信号时，客户端最初处于状态0，然后将其状态从0变为1，并将登录id Uid和自己的身份C安全地发送然后客户端接收来自服务器的密码请求。在下一步客户端安全地回复其密码，并通过公共通道接收来自服务器的登录验证回复Dolev-Yao入侵者模型用于实现.Snd（）和Rcv（）通道。类似地，HLPSL中指定的服务器角色被实现，其细节如图所示。 10个。声明见证（C，S，ser_client_nc，Nc '）表示由客户端生成的随机现时值Nc对于服务器是新鲜的，并且请求（S，C，client_server_ns，Ns'）表示客户端以类似的方式，见证（S，C，client_ser_ver_ns，{S，C}）确保所生成的随机数Nc和Ns在客户端和服务器之间保持图11和12由会话和环境角色组成。在目标部分中，指定了三个认证目标和四个保密目标。例如，保密性目标Nc描述了Nc对客户端和服务器保密，认证目标client_server-ver_ns描述了服务器必须对客户端为服务器生成的随机数ns进行认证。6.2. 仿真结果所提出的协议针对中间人攻击和应答攻击通过使用运行中模型验证（OFMC）进行测试（Basin等人，基于约束逻辑的攻击搜索器R.Y.公司Patil，S.R.Devane/ Journal of King Saud University2041见图12。 角色环境。见图10。 角色服务器。图十三. OFMC输出。（CL-AtSe）（Turuani，2006）AVISPA的后端。当合法用户执行协议时，AVISPA后端会引入被动入侵者（一）。对于Dolev-Yao模型检查，后端验证入侵者是否可能进行任何中间人攻击。所提出的协议的模拟结果示于图1A和1B中。 13和14号。在OFMC的情况下，总访问节点数为387，深度为13桩，搜索时间为一点零五秒。CL-AtSe协议分析的结果表明，分析的状态数为19个，其中10个状态是可达的，翻译时间为0.04 s。结果表明，该协议对所有主动和被动攻击都是安全的.7. 实验评价见图11。角色会话。系统架构的概述如图15所示。建议的系统利用亚马逊网络服务托管的解决方案。Apache Tomcat服务器用作Web服务器和数据服务器。2042R.Y.公司Patil，S.R.Devane/ Journal of King Saud University系统和Internet Explorer、Mozilla Firefox或Google Chrome浏览器。用户至少需要Java JRE 1.5版本。在运行时从服务器获取要在指纹客户机上部署和执行的用于收集设备指纹参数的代理进程。这个代理进程可以使用Java网络启动协议（JNLP）启动（Zukowski，2002）。7.2.从fingerprintee客户端机器见图14。 CL-AtSe输出。运行MySQL 5.5的基本服务器。建议系统的实施分为4个部分7.1. 代理进程对于代理进程在服务器上的本地部署，设备指纹参数提取文件和其他支持文件存储在服务器本地文件系统中。这些文件存储为NTFS文件。JAR使用数字签名进行签名（使用SSL签名工具），以便可以建立完整性和真实性。这样做可以保护系统免受二进制修改攻击。指纹客户端目前可以使用Windows和Linux操作系统-一旦用户来到网页，输入登录凭据，并按下“登录！”按钮时，基于JNLP的代理进程在后台的客户机上执行，并且提取的关于设备参数的信息被发送到在服务器上执行的指纹脚本。指纹识别脚本将生成设备指纹，并将其与原始参数一起存储在MySQL数据库中。Windows Management Instrumentation Commands