零信任网络安全：用户行为形式建模与安全策略生成

0Array 14 (2022) 1001460mmons.org/licenses/by/4.0/）的开放获取文章。0ScienceDirect提供的内容列表0数组0期刊主页：www.elsevier.com/locate/array0通过对用户行为进行形式建模生成用户特定安全策略来增强网络安全0Arwa AlQadheeb a，Siddhartha Bhattacharyya a，�，Samuel Perl b0a佛罗里达理工学院计算机工程与科学，墨尔本，FL，32901，美国b卡内基梅隆大学软件工程研究所，匹兹堡，PA，15213，美国0文章信息0关键词：零信任自动验证正确性网络安全策略安全策略形式方法用户行为自动安全策略生成有限状态自动机定时计算树逻辑0摘要0当今组织面临着一个艰巨的挑战，即在拥抱新兴技术的同时保护支持关键业务功能的系统和数据。尽管安全执行技术取得了重大进展，攻击者仍然能够 compromise组织和访问。计算机入侵的影响已经变得难以忍受，以至于许多组织正在彻底重新思考其对内部网络安全的方法。这种方法被称为零信任，它试图消除对受信任的内部网络边界的任何概念。零信任的好处包括显著增加攻击者实现目标所需的工作量。但零信任也将增加内部安全团队的管理复杂性。这些团队将需要一种方式来收集数据并根据分析做出策略决策。这个过程将需要对所有组织系统和数据进行，并且需要在所有访问上下文中进行。我们的方法使用形式方法来对最终用户的安全相关行为进行建模和检查。研究人员发现，用户的安全决策与诸如人口统计学、人格特征、决策风格和风险偏好等因素相关。我们使用有限状态自动机（FSA）来描述这些行为。这允许基于定时计算树逻辑（TCTL）自动制定线性时间安全属性。然后，该逻辑用于检查收集和观察到的安全行为对策略的满意程度。这种形式行为分析可以与上下文分析过程中的其他安全和网络数据相结合，这需要对每个零信任访问请求进行。其他网络或主机安全数据可能包括地址标识符、令牌、事件数据、数据包检查、运行进程数据、网络威胁情报等等。我们的方法允许拥抱零信任理念的组织生成特定上下文的安全策略，并对其正确性和完整性进行自动验证。01.介绍0当今组织面临着一个艰巨的挑战，即在拥抱新兴技术的同时保护支持关键业务功能的系统和数据。尽管安全执行技术取得了重大进展，攻击者仍然能够compromise组织和访问。也许比以往任何时候都更多，组织需要拥抱包括物联网、机器学习和统计分析以及云计算在内的新技术创新。随着这些新设备和服务的推出，组织有业务需求将它们连接到其业务网络。如果他们不这样做，他们就有可能被竞争对手在市场上超越。这进一步测试了他们的安全团队防止0� 通讯作者。邮箱地址：sbhattacharyya@fit.edu（S.Bhattacharyya）。0新的入侵是一种挑战，因为攻击面迅速变化，软件供应链变得越来越复杂。安全专业人员正在开发新的安全模型，以更好地准备预防、检测、应对和恢复网络攻击。0https://doi.org/10.1016/j.array.2022.1001462021年6月10日收到；2022年2月15日修订后收到；2022年4月1日接受2moet al. [13] and Mandal, Sudakshina, et al. [14] both focus on dy-namically generating access control decisions but neither explicitlyincludes recent user security behaviors, choices, or device settings asdecision-making as input or as model features. Eidle, Dayna, et al. [15]adjusts access policy for 8 different trust levels dynamically via firewallAccess Control Lists (ACLs) and Authentication Gateways. The modeltakes alert data from firewalls, authentication gateways, and othernetwork devices as input but does not include recent user securitybehaviors that do not trigger alarms. Lastly, Dean, Erik, et al. [16] useautomated device health attestation results as input for some of theuser devices in their network during session authentication in a ZeroTrust environment. This maps to the properties in Device Securement,and Updating and may even map to Passwords or ProActive Awareness.However, the work does not list the specific device parameter checksthat are performed in the ‘‘Health Check’’. Another key difference isthat the work does not use reachability analysis to apply differentlevels of security permissions for slightly higher risk but still acceptabledevice configurations.0Array 14 (2022) 1001460A. AlQadheeb等人。0心理学，人类信息处理能力的局限性，以及他们依赖以往经验来采取未来行动可能会妨碍他们的安全选择。0大多数计算机系统都是基于一般认知设计的。0大多数计算机系统都是基于一般认知设计的。0著名黑客凯文∙D∙米特尼克表示，最有效的入侵技术是利用人类作为系统中最薄弱的环节。从他的观点来看，克服这个问题0著名黑客凯文∙D∙米特尼克表示，最有效的入侵技术是利用人类作为系统中最薄弱的环节。从他的观点来看，克服这个问题的唯一可靠方法是将安全技术与严格的安全政策结合起来，并为用户提供适当的教育计划和培训课程。0我们的方法展示了基于形式方法的框架使用0为生成用户特定安全策略提供了对现有文献的新贡献。0本研究的其余部分组织如下：第2节0更深入地描述了相关工作。第3节介绍了研究方法，概述了自动化方法的顺序开发过程。第4节讨论了用户安全行为的选择。第5节讨论了模型考虑因素和所选的建模范式。第6节讨论了在第6.1节中选择和建模安全行为的整体实验，第6.2节解释了检查用户安全行为满意度的过程。第6.3节定义了生成用户特定策略的规则。第7节讨论了使用我们框架获得的最终结果。最后，第8节阐明了我们的结论和未来工作。02. 相关工作0基于形式方法的方法已被应用于建模0对用户行为进行分析，并使用认知架构中描述的用户模型，如Curzon[8]所述。通过这种方法，研究人员能够捕捉设备和人类之间潜在的错误交互。Curzon的研究重点在于0人类认知的建模遵循认知原则。形式模型是使用定理证明器进行验证的，而不是模型检查器。因此，它比模型检查器使用的自动化方法更为手动。最后，Curzon的工作讨论了一种验证方法，但没有实施这种方法。Degani[9]讨论了在航空电子领域中对人机界面进行形式建模和分析的方法，以捕捉界面设计中的错误。一旦用户模型被开发，就会开发一张对应表来了解用户对事件的反应。最后，通过生成用户模型与自动驾驶仪模型的掩蔽同步乘积来开发组合模型。这项工作也是一项理论研究，没有使用任何工具实施。Bolton[10]调查了基于形式验证的方法，用于验证人机交互以识别界面设计中的错误。但是，所有这些方法都集中在应用形式方法来在设计时识别错误，没有一种方法讨论了如何将形式用户模型作为分析实时数据的一部分，以及用于网络安全的安全策略生成。我们的方法展示了如何对用户的形式化建模的网络安全行为进行实时分析，然后生成安全策略。Houser[11]讨论了开发心理用户模型来捕捉用户对系统当前状态的认知，系统的实际状态，然后识别是否存在任何漏洞。Houser的模型没有捕捉到用户实际表现的行为，而我们通过Egelman[12]进行的研究来对用户表现的安全和不安全行为进行建模，这可以用来生成安全策略。一个类似的工作是Enoch, Simon Yusuf.‘‘动态网络安全建模与分析。’’（2018）[1]。Enoch使用网络状态输入来生成基于约束的可适应安全模型。动态网络状态的变化被用作输入来生成修改后的图形安全模型，但并没有明确采用用户行为输入。该工作也针对的是一个可以动态调整网络配置的网络（也称为主动防御），而不是假设零信任环境。用于生成和评估攻击场景的模型侧重于可能的攻击者行为（攻击树），而不是评估最终用户行为、选择和设备设置的风险。03. 研究方法0研究方法描述了解决问题所使用的方法。0生成遵循零信任理念的用户特定安全策略的问题。30数组14（2022）1001460A. AlQadheeb等人0图1. 研究方法。0我们的方法利用了对人类意图、态度、规范以及由此产生的网络安全决策行为的研究结果。有许多研究表明可用安全性是一个难题。用户经常忽视明确的警告，并误解许多风险及其造成的影响的可能性[17]。用户也会理性地拒绝警告，因为他们在过去的经验中经历了太多的虚假警报[18,19]。人与计算机的交互界面很难设计，固有的认知弱点可能会对安全决策产生负面影响[3,20]。一些研究发现，基于背景、文化和态度提出安全决策时，个体用户的行为会有所不同[2,5,21]。由于人类行为多种多样，难以预测且开放式，我们将研究中的安全行为限制在已经在先前研究中得到验证的现有量表中。Egelman和Peer创建了一个安全行为意图量表（SeBIS）[12]，用于评估用户根据自我声明的信息遵守计算机安全建议的能力。该量表侧重于四个构建，即设备保护、密码生成、积极意识和更新。Gratian等人[2]证实了SeBIS的准确性，并扩展了SeBIS以研究个性特征和人口统计学与安全意图的相关性。我们在图1中的形式化方法指导的用户特定策略生成框架（FMUSPGF）中设定了整个研究的结构，该图显示了开发过程作为四个阶段的序列。FMUSPGF中的第一步涉及选择安全行为，通过对现有文献进行调查来确定预期的安全行为。一旦选择了安全行为，第二步涉及对这些行为进行建模，我们采用了基于形式化方法的方法。在对安全行为进行建模后，下一步涉及对安全行为进行标记，这是通过执行使用形式化规范设计的查询来完成的。最后，根据前一步中的标记生成用户特定的安全策略。我们的主要贡献在于设计了一个基于形式化方法的框架，以支持网络安全的用户特定策略生成过程。在这个过程中，我们演示了如何识别和选择定义用户安全行为的基本特征。然后，我们将已识别的安全行为建模为形式化模型，以实现自动推理。最后，我们能够检测用户安全行为中的弱点，然后提出相关的策略。04. 选择安全行为0在本节中，我们重点关注通过考虑用户所做的安全决策来选择用户的安全相关行为。它描述了数据收集、比较和选择的范围，以构建一个可靠的知识库，代表了开发正式模型的要求，我们在审查了各种可能性后完成了这一目标。先前的研究已经全面调查了人口统计学、个性特征、决策风格和冒险偏好的个体差异与其影响之间的相关性0表1 [5]和[2]心理测量的比较0度量研究[5] 研究[2]0考虑未来后果（CFC）� � 安全行为意图量表（SeBIS）� � 领域特定风险态度（DoSpeRT）� �国际人格项目池（IPIP）� � 普通决策风格（GDMS）� � 巴拉特冲动量表（BIS）� �认知需求（NFC）� �0在网络空间中用户安全相关行为的研究。我们选择关注决策，因为实验证明它比人口统计学、个性特征和冒险行为更能预测安全实践[2,12]。本研究的预测因子的选择源自两个早期研究的观察，分别由Egelman和Peer[5]以及Gratian等人[2]进行。这两项研究旨在开发定制的安全防御措施，考虑个体之间的差异，以限制用户的错误及其后果。[2]的样本人群包括来自美国一所大型公立大学的高等教育参与者，而Egelman和Peer调查了一群年龄超过18岁的亚马逊机械土耳其（MTurk）的个体。他们都使用SeBIS进行研究；然而，Egelman和Peer关于安全的兴趣是调查SeBIS与决策心理测量之间的相关性。Gratian等人对[5]进行了扩展版本，以证实SeBIS的准确性，扩大了SeBIS的使用范围，以检查个性特征和人口统计学与安全意图的相关性。从表1比较Egelman等人[5]和Gratian等人[2]，我们确定SeBIS、DoSpeRT和GDMS用于确定安全意图、冒险行为和决策制定之间的关系。确定如何对特定情况做出反应的过程需要风险评估，考虑未来的后果，并探索可能的替代方案。人类心理的自然结构、人类信息处理能力的限制以及他们几乎完全依赖以前的经验，阻碍了做出正确的选择[3]。未能确定什么是正确的事情，反之亦然，在网络安全中是一个重要问题。如果有些人决定在公共场所不看管他们的设备，设置容易猜测或破解的密码，匆忙下载匿名电子邮件附件，或低估软件更新的重要性，他们更容易成为狡猾个体的受害者。我们认为，将安全行为建模为每个用户的行为作为一系列不同连接的决策。每个决策与特定的SeBIS构造相关：设备安全、密码生成、积极意识或更新。根据我们从[2,5]收集的发现，我们选择在这项工作中使用Egelman和Peer的结果，根据特定的安全决策来开发正式的用户安全相关行为，因为这些行为被确定为现实和用户安全行为。40Array 14（2022）1001460A. AlQadheeb等0图2.网络安全用户行为知识表示架构。05.建模用户安全行为0在审查了与安全行为相关的决策过程的研究后，构建了适当的知识库，并选择了最相关的用户行为来开发形式模型。本节的内容侧重于与架构的抽象级别和所选建模范式相关的设计选择。05.1.设计选择：抽象级别0模拟人机交互是具有挑战性的，因为人类行为的复杂性和广泛的知识要求。尽管我们选择了特定的知识库，但模拟和检查与设备保护、密码生成、主动意识和更新相关的用户安全行为的每个方面仍然具有挑战性。为了模拟SeBIS不同方面的用户行为，我们应用了从软件/系统工程中继承的分解原则来设计模型的结构。模拟关于安全行为的知识的架构包括不同抽象级别，以便于调试，增加可读性/可维护性并减少复杂性。我们将结构分解为多层的不同类型的安全服务，从（1）作为最抽象的级别开始，到（3）作为最低抽象级别结束。通过这样做，我们消除了关于我们为特定SeBIS维度使用了哪些安全方面的混乱。在这里，我们详细说明每个抽象级别。0•第（1）层是四个安全服务检查层中最抽象的一层。它吸收了SeBIS概念：设备保护、密码生成、主动意识和更新，这些是由Egelman和Peer指定的。这些对应于需要执行的安全任务的最高级别表示。•第（2）层根据第1级中确定的每个类别的关键参数来分解SeBIS概念，例如设备保护、更新机制、密码方法以及对威胁和违规行为的关注。然后，根据用户对他们想要采取的行动的决定，进一步分解为可能的附加子服务。•第（3）层有一个子树，从第2层的具体内容下降，例如用于设备保护的屏幕锁定功能，并由用户选择启用。05.2.设计选择：建模范式选择0尽管有几种方法可以用来建模用户行为，比如马尔可夫链、架构表示，我们选择了基于形式方法的方法。我们决定，表示用户行为最合适的方法是通过有限状态自动机（FSA）[22]，因为它允许我们在设计阶段早期进行自动化分析，这将使我们能够推理用户行为的逻辑表示，以评估替代设计选项是否存在深远的影响。它还允许以图形方式可视化用户行为。它还可以使用定义良好的工具。为了选择正确的平台来设计和检查用户行为的形式验证的可满足性，仔细考虑了NuXMV[23]、Uppaal [24]、PVS [25]和Z3 [26]等几种形式化方法。我们选择了Uppaal[27,28][24]，因为它能够模拟对网络安全至关重要的时间方面，以及生成和可视化反例。Uppaal将模型表示为定时自动机，Uppaal形式主义支持使用时间逻辑对网络定时自动机进行模型检查。这种建模范式允许将需求作为时间逻辑查询的执行，以彻底检查相关安全属性的满足情况。接下来我们将描述Uppaal使用的定时自动机形式主义。05.2.1.时钟自动机内的数学表示。Uppaal使用时钟自动机[29]，作为建模形式的混合自动机的一个子集。在设计人机交互的基本要求之一是能够模拟与操作或规则执行相关联的时间。时钟自动机是有限自动机，扩展了有限集的实值时钟。在自动机内部的转换的守卫中使用时钟或其他相关变量的值。根据守卫评估的结果，转换可能启用或禁用。变量可以被重置并作为状态的不变量实现。使用时钟自动机方法对时态系统进行建模是符号化的而不是显式的。它允许根据需要考虑无限状态空间的有限子集（即，使用依赖于安全属性和时钟自动机的等价关系的区域自动机），这被称为区域自动机。还存在各种工具来输入和分析时钟自动机和扩展，包括模型检查器Uppaal和Kronos[30]。0• 时钟自动机（TA）时钟自动机是一个元组(�, �0, �, �, �,�)，其中：�是位置的集合；�0 ∈�是初始位置；�是时钟的集合；�是动作、共动作和不可观察的内部动作的集合；���×�×�(�)×2�×�是位置之间的边的集合，带有5comentation) will vary based upon organizations and their Zero Trustsolutions, devices, policies, and procedures. There are also differentproposed solutions for implementing Zero Trust policy decisions, andany data collection or measurement of user security behavior will needto interact with the specific Zero Trust solution. Zero Trust solutionsnotionally include a policy enforcement point and a policy engine.Typically data needed for a security decision is collected by the policyenforcement point and sent to the policy engine for review. Organi-zations could add data collection agents to include end-user securitybehaviors according to their specific implementations and policies. Ourmethod allows organizations that embrace a Zero Trust philosophy togenerate context specific security policies that can be automaticallyverified for correctness and completion. Future work will be requiredto add user specific security behavioral data to existing data that is fedto the policy engine. Zero Trust environments are typically envisionedto have a policy engine analyzing network, application, device, anddata access policies and determining a decision in an access context.Some examples include using network or host security data includingMAC addresses identifiers, Internet Protocol (IP) addresses identifiers,security access tokens, session tokens, process event data, packet in-spection data, running process data, threat intelligence data, devicespecific data such as installed application inventories, configurationsettings, security relevant settings, and much more.0数组14（2022）1001460A. AlQadheeb等人0动作、守卫和一组要重置的时钟；�∶�→�(�)将不变量分配给位置。我们将时钟估值定义为从时钟集到非负实数的函数�∶�→R≥0。让R�表示所有时钟估值的集合。对于所有�∈�，�0(�)=0。如果我们将守卫和不变量视为时钟估值的集合（稍微放松形式），我们可以说�∈�(�)表示�满足�(�)。0• 时钟自动机语义0让(�, �0, �, �, �,�)是一个时钟自动机��。时钟自动机��的语义被定义为一个带标签的转换系统�→�，其中��� × R�是状态的集合，�0 = (�0, �0)是初始状态，而→�� × {R≥�是转换关系，使得：01. (�, �) → � (�, � + �) 如果 ��′：0 ≤ �′ ≤ � � � + �′ ∈ �(�) 2. (�, �) �′) ∈ �，使得� ∈ �，0� = [� � 0]�且�′∈�(�)0对于 � ∈ R ≥ 0，� + � 将�中的每个时钟�映射到值�(�) + �，并且[� �0]�表示时钟估值，将�中的每个时钟映射到0，并在���上与�一致。请注意，�对时钟的简单条件，使得从一个位置到另一个位置的转换（或边�）成为可能的，除非发生相应的动作�，否则不会执行启用的转换。类似地，边�的重置时钟�指定了在边上执行转换时将值设置为零的时钟。因此，时钟自动机是一个有限的有向图，其上标有对非负实值时钟的重置和条件。然后，时钟自动机可以组合成一个时钟和动作的公共集合上的时钟自动机网络，由�个时钟自动机��� = (��, �0, �, �, ��, ��)，1 ≤ � ≤�。这使我们能够检查在时钟自动机网络上表达的可达性、安全性和活性属性，这些属性是用时态逻辑表达的。时钟自动机的执行，由����(��)表示，是连续转换的序列，而��的执行轨迹集合由������(��)表示。05.3. 用于验证的查询语言0Uppaal中的验证过程使用一种特定类型的查询语言，用于指定需要检查的一组属性。查询语言是计0•  �  是属性或命题 •  a  是原子动作。 •  g  是时钟约束。 •  E表示‘‘对于一些路径’’。 •  A  表示‘‘对于所有路径’’。 •  J是边界为自然数的区间。 •  state  � �  �  E( � 1  ∪ � � 2 ) ‘‘对于一些路径’’  � � ,  � �+1 ...0验证过程中，Uppaal使用特定类型的查询语言，用于指定需要检查的一组属性。查询语言是计算树计算树逻辑的0•  state  � �  �  A ( � 1  ∪ � � 2 ) ‘‘对于每条路径’’  � � ,  � � +1...0( �  k  ≥  � , k-i  ∈  J) (( � �  �  q) ( �  j, i  ≤  j < k)( � �  �  p))0T0( �  k  ≥  i, k-i  ∈  J) (( � �  �  q) ( �  j, i  ≤  j  < k)( � �  �  p))0•  G  表示‘‘路径中的所有状态’’。 •  F  表示‘‘路径中的某些状态’’。0表示为符号对。其中，对中的第一个元素表示路径量词之一，即 A 或E，而对中的第二个元素是以下之一：0Uppaal接受的查询语言包括：AG 不变式A[]，EG 可能始终E[]，AF 最终A <>，EF可能E <>。0路径公式和状态公式的不同组合0进行实验的第一步是实验06. 实验06.1. 实验设置：对所选安全行为进行建模0设置，其中包括在时态自动机中对所选安全行为进行建模6.1。一旦模型开发完成，下一步就是进行实验（6.2），以标记良好和不良的安全行为。0我们模型的设计是由能力指导的，以便0概念，但是仪器设备的细节（或数据收集实施）将根据组织及其零信任解决方案、设备、政策和程序的不同而变化。实施零信任策略决策的不同提议解决方案，以及任何用户安全行为的数据收集或测量都需要与特定的零信任解决方案进行交互。零信任解决方案概念上包括策略执行点和策略引擎。通常，安全决策所需的数据是由策略执行点收集并发送到策略引擎进行审查。组织可以添加数据收集代理，以根据其特定的实施和政策包括端用户安全行为。我们的方法允许拥抱零信任理念的组织生成特定上下文的安全策略，并可自动验证其正确性和完整性。未来的工作将需要将用户特定的安全行为数据添加到馈送给策略引擎的现有数据中。零信任环境通常被设想为具有策略引擎分析网络、应用程序、设备和数据访问策略，并在访问上下文中做出决策。一些示例包括使用网络或主机安全数据，包括MAC地址标识符、InternetProtocol（IP）地址标识符、安全访问令牌、会话令牌、进程事件数据、数据包检查数据、运行进程数据、威胁情报数据、设备特定数据，如已安装的应用程序清单、配置设置、安全相关设置等。0在这项工作中，我们手动进行数据收集，以展示06.1.1. 设备安全0• 设备保护0我们选择设备保护作为设备安全性的第一个标准。这意味着用户是否通过密码、PIN码、指纹或图案来保护他们的设备。尽管锁定各种设备是一项简单的安全任务，但有时却被最终用户低估了。在2017年进行的皮尤研究中心调查中，28%的美国手机用户报告称，他们不使用PIN码或任何其他安全功能来访问他们的智能手机[ 32]。这个安全问题在工作环境中更加重要。例如，如果一些员工在工作场所之外使用便携设备（如笔记本电脑、平板电脑或智能手机）作为他们的主要工作电脑，他们可能会在一些地方（如酒店房间或汽车中）不保护设备。这样一来，如果他们的设备被盗，它已经是解锁状态，公司的数据将落入未经授权的个人手中。大多数组织要求对持有其数据的设备进行此类控制，但在所有生态系统和设备中进行监视和执行可能很困难。60数组14（2022）1001460A. AlQadheeb等0图3. 设备安全状态转换图。0表2 设备安全性属性。0编号 知识库属性01 E <>（device_protection.enabled） 2 E<>（device_protection.disabled） 3 E<>（screen_locking.turned_on） 4 E<>（screen_locking.turned_off） 5 E<>（timeout.short） 6 E <>（timeout.long）0• 屏幕锁定密码保护的屏幕保护程序功能是指在设备在一段时间内不活动后自动锁定。一些最终用户发现每次超过超时时间都必须重新登录有点麻烦。其他人对威胁的认识较低；他们认为由于他们几乎一直在他们的便携设备周围，特别是智能手机[ 33]，所以不会出现问题。还有一些人设置了密码保护的屏幕保护程序，但将默认的超时时间（通常为15分钟）调整为更长的时间[ 34]。我们研究设备安全的这一方面，是因为不设置密码保护的屏幕保护程序将允许恶意个人（例如内部威胁）访问数据或执行一些他们无权查看或执行的任务[ 35]。内部威胁是最困难的安全问题之一；恶意内部人员对组织的风险可能比外部人员更大，因为他们更熟悉安全基础设施、实践和漏洞。他们可以更容易地避免被发现，并长时间保持隐匿。在表2中，我们可以看到我们如何将上述标准转化为TCTL公式，而图3分别描述了设备保护、屏幕锁定和屏幕锁定超时状态转换图。06.1.2. 密码生成 • 密码年龄密码在网络安全中一直是一个长期存在的问题。人们提出了很多建议，也制定了政策，但弱密码问题仍在不断增加。设置最大密码年龄是维护良好密码卫生的传统技术之一。它要求用户定期更改密码，通常在30到90天之间[ 36]。有人可能会认为定期更改密码会使密码更难记住0用户记住，因此更有可能被不安全地存储。用户正在调整和发展应对机制，以克服这一负担，通过对他们当前密码进行一些修改。我们将这个规则包含在我们的规范集中，以展示可以包括在知识库中的标准的一个示例。• 密码长度人们想要保护自己的个人信息，但他们不愿意为此付出更多的努力。最大的例子是，尽管持续不断地有关于使用弱密码的安全警告，以及由此行为产生的严重后果，他们仍然使用短小且容易记住的密码。根据《密码心理学报告》，参与研究的人中有47%表示他们更愿意选择简单的密码，因为他们害怕忘记它们[ 37]。Martin等人（2012）说明，通过暴力破解攻击猜测密码最有可能不会成功，而对包含大写和小写字母、数字和符号的长且复杂的密码。他们提到，破解长度为4、8或16个字符的复杂密码分别需要大约81秒、210年和1.4万亿年[38]。根据Maddox和Moschetto（2019）的说法，当用户为某个账户分配密码时，他们应保持足够的长度，避免常见的字符替换，并使用各种字母、数字和特殊字符[ 39]。我们认为密码长度是必须要考虑的，以确定哪些账户容易受到密码攻击。•密码可重复使用由于要处理和跟踪的账户太多，用户可能会诱惑使用一个密码来覆盖它们所有，并给自己带来一些安心；用户可能会后悔。对多个站点重复使用相同的密码比在一张纸上分别写下不同的密码带来更大的风险。如果个人决定为他们的不同账户分配一个密码，他们将允许攻击者入侵使用相同密码的其他账户[ 40]。密码保护的困难在于，大多数最终用户承认密码可重复使用的风险和后果；然而，35%的人忽视这一知识，而更愿意记住他们简单和熟悉的密码[ 37]。我们选择涵盖密码生成的这一方面，因为在最坏的情况下，产生的风险不仅限于最终用户，而且还会延伸到工作场所和同事，如果他们将工作密码重复用于其他个人账户。7A. AlQadheeb et al.0Array 14 (2022) 1001460表3 密码生成属性。0No. 知识库属性01 E <>  (密码年龄.未过期) 2 E <>(密码年龄.已过期) 3 E <>  (密码长度.长) 4 E <>(密码长度.短) 5 E <>  (密码可重用性.未使用) 6 E<>  (密码可重用性.已使用)0表3 列出了Uppaal规范语言中密码年龄、长度和可重用性的等效表达。06.1.3. 积极意识0•  发现威胁迹象0毫无疑问，人们对网络安全的兴趣正在增长和扩展，使他们更加了解和谨慎地对待在线信息共享、虚假电子商务网站、诈骗和安全威胁。在这个不完美的世界中总是有一个‘‘但’’，因为有相当数量的人缺乏数字安全意识和教育，这反过来影响了他们识别威胁的能力，即使有明显的迹象。如果最终用户无法发现设备上的间谍软件迹象、识别社交工程企图、识别钓鱼或欺骗邮件，或者其他隐蔽的活动，他们就无法保护自己免受身份盗窃的威胁。根据Verizon的数据泄露调查报告(DBIR)(2019)，钓鱼攻击是数据泄露的主要原因之一。它是32%的确认数据泄露事件的一个因素，以及78%的网络间谍活动事件[41]。基于此，我们强调了在太迟之前识别和避免钓鱼诈骗的重要性。0•  报告威胁0在‘‘如果发现异常情况，请报告’’的全国宣传活动中，我们被鼓励在发现不寻常情况时向当局报告，以确保自己和社区的安全[42]。在组织环境中也是如此；报告可能的安全事件可以在侵入检测的早期阶段节省宝贵的时间[43]。如果员工了解网络攻击的类型以及它们的外观和发生方式，他们更有可能注意到系统上发生的未经授权的变化。他们可能会更有信心，愿意向IT部门寻求帮助。缺乏网络安全意识、培训和警惕性，以及员工与IT团队之间的沟通不畅，会使前者犹豫不决，质疑自己是否真的发现了什么。我们将这一领域纳入我们的研究范围，是为了模拟用户是否真的没有接受足够的教育，还是他们只是太鲁莽，不愿报告这样紧急的事情。0•  遵守政策0识别、确定和处理对组织资产机密性、完整性和可用性的风险是首要任务。安全政策和程序是任何组织管理控制层次结构的一部分，用于维护敏感数据的安全，这是最关键的资产，免受复杂和不断发展的威胁环境的影响。对任何组织来说，最大的担忧之一是如何保护数据免受员工的侵害[44]。制定安全政策和指南是为了告诉员工在与信息系统互动时什么行为是可以接受的，什么是不可接受的。问题在于员工的不合规行为[45]。根据Mutlaq等人(2016)的说法，不合规行为可能是0表4 积极意识属性。01 E <>  (发现威胁.是) 2 E <>  (发现威胁.否) 3E <>  (报告威胁.是) 4 E <>  (报告威胁.否) 5 E<>  (安全策略.遵守) 6 E <>  (安全策略.违反)0分类为：首先，是有意或计划的行为，旨在损害组织实体的异常行为。其次，是违反安全策略但没有恶意损害的疏忽行为。第三，是由于缺乏网络安全知识和培训而产生的无知行为。在确定安全策略违规的不同解释后，我们对终端用户对安全策略的遵守进行了建模，因为这有助于确定对特定用户施加的正确策略行动。表4显示了生成的线性时间属性，用于研究积极意识的知识库方面。06.1.4. 更新0•  更新机制0与安全相关的软件更新是终端用户应更加关注的最重要的安全保护工具之一，并确保它们按照定期的时间表安装。对于操作系统和应用程序更新，终端用户可以配置几种选项，例如如何下载和安装更新（即自动或手动）在他们的设备上。大多数现代软件系统都设置为自动下载和安装安全和其他必要的更新，无需人类做出决定。相反，手动更新允许用户更好地控制他们的设备，选择安装哪个更新以及何时安装。没有确定的位置可以说一个机制比另一个更好更安全，因为这完全取决于用户对此事的行为。也许会想到自动机制似乎是更负责任的选择。但是，只要终端用户确保他们的系统在新更新可用时立即更新，手动更新也是负责任的。我们选择包括用户对更新机制的偏好，以观察不同的行为。0•  更新时间0尽管一些软件更新和补丁是为了解决先前安装的软件中发现的安全漏洞，但一些终端用户避免或延迟安装，因为他们认为这些增量更新只是无用的技术添加[46]。在此存在着对那些在一段时间后才手动下载和安装更新的用户的风险。我们从中看出，延迟安装最新更新和补丁为恶意个体利用用户设备上的开放安全漏洞创造了机会窗口[47]。因此，我们进一步调查了用户对及时更新的疏忽行为的特征和建模。0•  重启时间0软件开发人员不断努力改进安全性，通过排除用户角色免于软件更新周期。他们发现用户干