认知过程中的机密泄露的检测及认知架构研究

理论计算机科学电子札记183（2007）21-38www.elsevier.com/locate/entcs检测机密泄露的认知原因*R. Ru ksestecna s a，1，P. Curzona，2 和A. B土地为db，3a部。 英国伦敦大学玛丽皇后学院计算机科学系b英国伦敦大学学院互动中心摘要大多数安全研究都集中在系统的技术方面。我们从以用户为中心的角度考虑安全性。我们专注于认知过程，在安全的信息流从用户连接到电脑系统为此，我们扩展了为验证可用性属性而开发的框架。最后，我们考虑一些小例子来说明这些想法和方法，并展示如何在我们的框架中检测到由不适当的设计和人类认知的某些方面相结合而导致的一些机密泄漏。保留字：人为错误，安全，认知架构，形式验证，SAL。1引言关于信息流的安全性（保密性）有很多研究（参见Sabelfeld和Myers出发点是假设计算使用机密输入。目标是确保不干扰策略[10]，这基本上意味着在两个仅在其机密输入方面不同的计算之间不能观察到输出的差异。已经提出了解决这个问题的各种方法，例如访问控制[3]和静态信息流控制[9]，并且开发了形式化和机制，例如。安全类型系统[20]和类型检查器[15]。所有这些研究都集中在软件系统的技术方面。其目的是确保系统的实施不会泄漏确认信息。然而，技术只是安全的一个方面在互动本研究由EPSRC赠款GR/S67494/01和GR/S67500/01资助。1 电子邮件地址：rimvydas@dcs.qmul.ac.uk2电子邮件地址：pc@dcs.qmul.ac.uk3电子邮件：a. ucl.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.05922R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21Fig. 1. 互动的循环除了计算机系统之外，还有另一个角色-它的人类用户。即使是完美设计和实施的系统也无法阻止用户无意中泄露他们所拥有的机密信息。用户可以出于多种原因违反安全性。然而，人机交互的研究[1，13]揭示了这种违规行为的系统性原因，包括认知超载，缺乏安全知识，以及计算机系统行为与用户心理模型之间的不匹配。即使在没有软件错误的情况下，当功能正确的行为与用户期望不一致时，安全性也可能被破坏[13]。用户和安全机制之间的关系由用户-以安全为中心，提供这项工作的大部分需要社会层面，考虑的问题，如用户的动机和理解的安全机制，工作实践，系统用户之间的关系，包括当局和社区的用户，和威胁的安全利用社会工程技术。我们的工作介于信息流安全的技术方面和以用户为中心的安全的社会方面之间。更具体地说，我们感兴趣的是信息流;然而，这个信息流的轨迹现在不在计算机系统中，而是在用户提供给它的输入中。我们没有考虑人机交互和安全性的社会方面。相反，我们关注的焦点是信息从人类用户进入计算机系统的认知过程我们建立在我们在可用性工作中开发的通用用户模型（认知架构）上[8]。它是从抽象的认知原则发展而来的，例如用户进入一个具有任务及其附属目标知识的交互认知架构后来被扩展[17]，包括从设备信号和环境对象到用户决定它们的含义的路径的抽象规范和解释（见图1）。以用户为中心的安全性提倡将这种用户行为模型转换为安全模型[21]：例如Ka-Ping从一个非正式的用户模型中推导出安全交互设计的指导方针（设计规则）[13]。设备模型输出输入环境模型世界状态解释用户模型输入存储器输出效果R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2123我们的认知架构已被证明可用于在可用性和任务完成情况下检测各种类型的系统性用户错误[8，17]。 在这里，我们的目的是表明，从这个架构中出现的行为也暴露出安全问题，从而促进用户交互设计的安全方面的改进。为了证明这一点，我们首先从安全的角度非正式地讨论了我们早期工作中处理的几个用户错误的例子[8]。然后，我们考虑使用模型检查工具SAL [14]来检测从我们的认知架构中出现的一些机密泄漏，并以用户对系统提示的解释为更具体地说，我们考虑了用户习惯和身份验证界面中输入字段的（相对）定位组合可能产生的安全这些例子很小，旨在说明我们认为更普遍适用的方法和想法总之，本文的主要贡献如下：• 对交互系统中机密泄漏认知方面的形式建模的调查。• 我们的框架的扩展，为可用性验证而开发，以处理用户交互中的安全问题。• 一个说明性的机密泄漏的例子，由认知解释引起，并通过使用我们的认知架构进行模型检查来检测相关工作Beckert和Beuster的工作[ 2 ]虽然是独立和平行进行的，但他们还开发了一个正式的用户模型，并将其与应用程序的规范和用户对该应用程序的假设相结合，他们的用户建模是基于一个既定的方法，GOMS [12]，这是他们工作的核心用户假设的建模与我们的然而，他们的Beckert和Beuster非正式地定义了三个HCI安全要求，然而，只有一个是正式的，而我们框架中的正确性属性也解决了剩下的两个。也不清楚它们是否为自动验证提供工具支持。另一方面，他们的方法支持分层模型：在处理大型系统时具有优势在安全关键系统的相关领域，Rushby等人 [18]关注模式错误和飞行员跟踪模式变化的能力。他们将系统的合理心理模型形式化，并使用Murφ验证工具对其进行分析。心智模型本质上是抽象的系统模型;它们不依赖于认知原则提供的结构。它们也不对用户解释进行建模。Cerone等人使用模型检查器来寻找新的行为模式，这些模式被实验数据的分析所遗漏。 他们的分类阶段24R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21表1SAL语言的一个片段x：T x有 T型λ（x：T）：e是x的函数，值为exJ= e更新：x的新值是表达式 e{x：T |p（x）} T 的子集，使得谓词p（x）成立a[i]thei-theelementofthearrayar.x记录 r的场xrWITH.x：= e记录 r，其中字段x被 e的值g→upd替换，如果g为真，则根据updc[] d在c和d[]（i：T）：ci 在ci之间的非确定性选择，其中i在范围T内模型类似于用户解释。Ka-Ping [13]给出了一系列设计规则，这些规则由非正式的用户模型来证明，并为提高交互系统的安全性而量身定制。由于规则是非正式的（许多规则可能太抽象而无法形式化），因此没有工具支持来验证设计是否遵守这些规则。2SAL中的认知结构我们的认知架构是抽象认知原理的高阶逻辑形式化，并具体化了认知上合理的行为[5]。该架构指定了可能的用户行为（动作的痕迹），这些行为可以根据认知科学的具体结果来判断。真正的用户可以在这个框架之外进行操作，架构对此没有任何说明它的预测能力受到人们根据特定原则行事的情况的限制。这种体系结构允许人们研究如果一个人以这种看似合理的方式行事会发生什么。所定义的行为既不是“正确的”，也不是“不正确的”。这可能取决于所讨论的环境和任务。我们并不试图对潜在的神经结构进行建模，也不试图对更高层次的认知结构（如信息处理）进行建模。相反，我们的模型是一个抽象的规范，旨在便于推理。我们依赖于认知原则，这些原则在Newell的条款[16]。他们的重点是用户的目标和知识。我们的原则的形式化是基于SAL模型检查环境[14]。它提供了一种高阶规范语言和工具，用于分析指定为参数化模块并同步或异步组成的状态机。我们使用的SAL符号见表1。我们还使用通常的符号表示合取、析取和集合成员运算符。图2给出了一个稍微简化的SAL规范，它定义了我们的用户模型，图中斜体的谓词是稍后解释的缩写。下面我们讨论认知原则以及它们在SAL规范（模块User）中的反映方式。非决定论 在任何情况下，任何一个认知上的plausi-可能会采取一些不好的行为不能假设任何具体的似是而非的R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2125过渡[]（i：GoalRange）：GoalCommit：gcommit[i]=readyNOT（gr）→finished=notf目标[i]。grd（in，in，env）[]INT[i];GTJ=TRUE[]（i：ReactRange）：ReactCommit：rcommit[i]=readyNOT（gr）→finished=notfreact[i]. grd（in，in，env）[]INT[i]nums;RRJ=TRUE[](i：GoalRange）：GoalTrans：gcommit[i]=committed→[]gcommitJ[i]=done;gcommitJ=doneGoalTransition（i）[]（i：ReactRange）：返回值rcommit[i]=committed→[]rcommitJ[i]=ready;rcommitJ=reactTransition（i）出口：PerceivedGoal（in，in）NOT（gr）finished=notf[]→完成J=okAbort：NOT（EnabledGoals（in，，env））NOT（EnabledReact（in，，env））NOT（PerceivedGoal（in，））→NOT（g）完成=notf[]finishedJ=IF Wait（in，min）然后不f否则中止ENDIF空闲：完成=notf →图二. SAL中的用户模型（简化）行为将是一个人将遵循的。SAL规范是一个过渡系统。非确定性由命名的保护命令（即转换）之间的非确定性选择[]表示 例如，目标-在图中提交2是由i索引的过渡族的名称。 每个守卫命令描述了用户可以执行的操作。26R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21精神对抗肉体的行为。用户承诺以一种在某个点之后不能撤销的一旦一个信号从大脑发送到运动系统采取行动，它就不能停止，即使它被关闭。一个人在采取行动之前就意识到这是错误的。因此，我们对身体和心理行为进行建模。每一个被建模的物理动作都与一个承诺执行它的内部心理动作相关联。在规范中，这是通过成对的保护命令来反映的：GoalCommit第一个模型承诺一个动作，第二个模型实际上正在做它（见下文）。用户目标。 用户利用任务的知识进入交互，并且特别是必须履行的任务相关子目标。这些子目标可能涉及必须传达给设备或项目的信息（例如银行卡）必须插入到设备中。如果有机会，人们可能会尝试实现这些目标，即使设备正在提示不同的动作。我们建模这样的知识作为用户的目标，代表了一个预先确定的部分计划，已经出现了从手中的任务的知识，独立的环境中，该任务被执行。没有固定的顺序是假设用户的目标将如何履行。要了解这在SAL中是如何建模的，请考虑受保护的命令GoalTrans用于执行先前已提交的用户操作：INT[i]nums;gcommit[i]=committed→intJ=int;GoalTransition（i）左为左为左，右为右。它表明，规则将仅在相关联的动作已经被提交的情况下激活，如由可提交的局部可变值的元素或已提交的值所指示的。如果规则被非确定性地选择为fire，则该值被更改为done，并且布尔变量gallery被设置为false，以指示现在没 有对 未完成 的物理 动作 的承诺 ，并且 用户 模型可 以选择 另一 个目标 。GoalTransition（i）表示与此特定操作i相关联的状态更新。用户目标被建模为一个数组goals，它是User模块的一个参数。用户模型的状态空间由三部分组成：输入变量in、输出变量out和全局变量（内存）env;环境由全局变量env建模。所有这些都是使用类型变量指定每一个目标都是由一个记录指定的领域grd，tout，tandem和tenv。下面将讨论该grdfield。剩下的字段是从旧状态到新状态的关系，描述了用户模型状态的两个组成部分（输出输出和内存恢复）和环境env是如何通过释放这个目标来更新的这些关系在通用用户模型被实例化时提供，用于指定GoalTransition（i）如下所示out J∈ {x：Out |return（i，i，i，i）;R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2127J∈{x：Memory|[i]. getsum（i，i，j）};env J∈{x：Env |goals [i].tenv（in，，env）（x）目标财产}由于我们正在对用户行为的认知方面进行建模，因此所有三个更新都取决于输入（感知）和记忆的初始值。此外，每次更新都取决于更新的组件的旧值存储器更新还取决于输出的新值（outJ），因为我们通常假设用户记得刚刚采取的动作env的更新还必须满足一个类属关系，即所有权。它具体规定了对财产的普遍物理限制，它们的价值，将占有和放弃占有物品的事件与占有物品数量（计数器）的相应增加或减少联系起来例如，它规定如果一个物品没有被放弃，那么用户仍然拥有它。拥有物品的计数器被建模为环境组件。我们省略了更多的细节，因为在本文中，所有权属性没有以任何方式使用。如果用于提交到用户目标的guarded命令GoalCommit被触发，它会将目标i的提交标记切换为committed，从而启用GoalTrans命令。从goals参数中提取的谓词grd指定何时有机会实现此用户目标。因为我们在GoalTrans命令中将done赋值给数组gcommit的相应元素，一旦触发，下面的命令将不再执行。如果用户模型释放了一个目标，它将不会再次这样做，除非有其他原因，如设备提示。反应性行为。用户可能会对外部刺激做出反应，做出刺激所建议的动作。例如，如果一个闪烁的灯亮了，如果注意到灯，用户可能会通过在相邻的插槽中插入硬币来做出反应。反应式操作由ReactCommit- ReactTrans对以与用户相同的方式建模目 标 ， 但 不 同 的 变 量 ， 例 如 用户模块的 react 参数而 不 是 goals 参 数 。ReactTransition（i）的定义方式与GoalTransition（i）相同一旦动作i被执行，数组元素rcommit[i]被重新分配为ready而不是done，因为如果提示，则可能重复响应动作基于目标的任务完成。用户间歇性地，但持续地，一旦他们的主要目标已经实现，就立即终止交互[6]，即使在实现主要目标的过程中产生的辅助任务尚未完成。现金点的例子是一个人带着现金离开，但留下了卡。在SAL在特定情况下，用户感知为交互的主要目标的条件由用户模块的参数PerceivedGoal然后，基于目标的完成被建模为受保护的命令退出，其简单地声明，一旦谓词PerceivedGoal变为真并且没有对用户目标和/或反应性动作的承诺，则用户可以完成交互。由于在启用的保护命令之间的选择是不确定的，因此可能仍然不采取此操作。任务完成是通过将局部变量finished设置为ok来建模的，而值notf表示任务未完成。基于无选项的任务终止。如 果 没有明显的行动，一个人可以采取这将有助于完成任务，那么这个人可以终止互动。例如，如果在售票机上，用户希望购买周季票，但是所呈现的选项不包括季票，则28R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21这个人可能会放弃，认为目标是无法实现的。在保护命令Abort中，无选项条件表示为谓词EnabledGoals和EnabledReact的否定。请注意，在这种情况下，一个人可能采取的行动是等待。然而，他们只会在给出一些认知上合理的理由（如显示的“请等待”消息）的情况下才会这样做。等待条件在规范中由谓词参数Wait表示。如果Wait为false，则finished设置为abort，以模拟用户放弃并终止任务。3验证用户交互在本节中，我们将讨论用户错误的示例，重点关注交互的安全方面。我们首先介绍要验证的属性。3.1正确性属性：可用性和安全性以前，我们的方法处理两种可用性属性。首先，我们要确保在任何可能的系统行为中，用户考虑到我们模型(1)F（ PerceivedGoal（ in， n））F的意思是“最终”。其次，在实现目标的过程中，经常会生成用户必须完成的辅助任务， 以完成 与其主要 目标相 关联的 任务。 如果子任 务的完 成被表 示为谓 词SecondaryGoal，则所需条件为（其中G表示(2)G（ PerceivedGoal（ in，） F（ SecondaryGoal（ in，，env）这表明，一旦感知到的目标已经实现，次要目标总是最终实现的通常次要目标可以表示为交互不变量[8]，它表示系统状态的某些属性，这些属性被扰动以实现主要目标，被恢复。在此之前，我们从纯可用性的角度来看待性质（2），将其应用于，例如，用户财产。然而，（2）的验证也可以用来检测安全问题。此外，我们将引入第三种正确性属性，与用户输入中的机密泄漏有关。直觉上，人们希望在所有系统状态下防止这种泄漏，因此我们的目标是安全属性。在信息流安全性方面[19]，为了简单起见，让我们有两个用户输入的保密级别，“高”和“低”。 解决某些安全方面的安全属性是， 在任何状态下，高输入都不会出现在低信道上布尔值，SecurityBreach，表示违反此规定的系统状态。 属性，声明它始终是如果没有安全漏洞，则：(3)G（ NOT（ SecurityBreach））我们将在第4节中讨论SecurityBreach如何设置为true，表示违规。R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2129请注意，前两个正确性属性都不能捕获被建模为SecurityBreach的机密泄漏。属性（1）是可用性属性;基本条件是用户实现主要目标。这一目标可能通过先犯错误然后撤销错误的行为来实现，这一事实无关紧要。然而，就安全性而言，撤消还不够好[13]：一个错误的操作可能已经泄露了机密信息虽然检查属性（2）可以揭示一些与完成后错误（参见be-low）相关的安全问题，但它仍然是一个活性属性。因此，它不要求系统在所有状态下都满足SecondaryGoal条件，只要求在主目标之后的某个点满足 办妥了一批多年3.2用户错误和安全错误操作是故障的直接原因，因为是特定操作导致了问题：例如，用户在错误字段中输入数据。然而，为了消除这个问题，我们必须考虑错误的根本原因。在我们的框架中，我们考虑的情况下，最终的原因是人类认知的方面（局限性），尚未在接口中解决。一个例子是，一个人在一个特定的字段中输入数据，因为界面设计建议它适合该数据。在Hollnagel的术语[ 11 ]中由于没有证据表明安全性错误是由不同的认知原因导致的可用性错误，我们的认知架构可以表现出导致安全性问题的行为，即使它是在没有考虑安全性的情况下开发的。其中一些错误与我们在早期工作中处理的可用性错误具有相同的认知原因[8]。接下来，我们讨论几种类型的用户错误，与安全性有关，但仍然可以在属性（1）和（2）表示的基于可用性的方法中检测到。从认知架构中出现的持续性用户错误是完成后错误[6]，其中用户在完成未完成的辅助任务时终止交互。人们发现即使在实验室条件下也会犯这样的错误[6]。这种错误的一个例子，也是一个安全漏洞，是当使用旧的取款机时，用户总是拿走现金，但留下了他们的银行卡。在我们的认知架构中，这种行为的出现是因为一个动作（退出）允许用户在目标实现后停止。使用我们的验证框架-工作，这是通过检查属性（2）来检测的。为此，SecondaryGoal会声明一个状态中用户所有物（包括银行卡）的总价值与交互之前相同。 一个类似例子在[8]中描述Blandford和Rugg [4]给出了一个现存的安全漏洞的例子，这是由于用户在离开工业打印机时忘记注销，使其容易受到破坏-30R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21使用者名用户名：进入用户名：使用者名进入图三.身份验证界面以前[17]我们也考虑了由于形状引起的对界面提示意义的混淆而导致的用户错误这个例子是一个用户试图使用ATM给电话卡充值。我们展示了基于我们的认知架构的模型检查如何识别用户对于请求电话号码或充值卡号码中的哪一个的困惑。检查的属性属于类型（1），即用户是否实现了主要目标。类似情况下的用户混淆也可能导致机密泄漏。例如，当要求输入卡号时，用户可能会混淆所请求的号码是银行卡还是电话卡。如果在界面提示充值卡号时输入银行卡卡号，则可能会显示输入的内容，这是一个安全漏洞。这个问题也可以通过分析为什么用户无法实现主要目标来检测。4案例研究：身份验证接口在本节中，我们扩展了我们以前的工作，并研究如何使用SAL中正式化的认知架构检测其他未考虑的安全问题。特别是，我们展示了用户习惯如何与某些设计相结合，可能导致对界面提示的错误解释，从而导致机密信息的泄漏。为了确定这种泄漏是否是可能的，我们在框架中引入了一个新的实体，通用模块测试器。 通过提供一个通道集 合 和一个安全性高实例化的模块然后检查该值是否可以出现在一个安全级别较低的频道上4.1的认证界面我们的示例涉及各种日常交互系统中存在的身份验证步骤在进行任何交易之前，用户必须通过提供用户名和登录密码来确定其身份。系统检查所提供的密码是否与与所提供的用户名相关联并存储在系统数据库中的密码相同从表面上看，人们可以期望认证界面的设计是简单的，例如像图3中的界面（左）。实际上，情况更为复杂。网上银行系统的界面窗口大小并不固定，用户可随时更改。这意味着输入字段的布局由算法决定。取决于R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2131娱乐（不完整数据）INIT不完全承认娱乐（正确输入）不完整消息登录显示DisplayedEnter娱乐（IncorrectData）娱乐（正确输入）登录消息不正确承认警告娱乐（<$CorrectInput）停止错误消息显示AbortMsg显示输入LastAttemptMsg见图4。认证过程该算法，图中所示的布局3（右）是可能的，当窗口大小减小。我们将论证这两个接口并不同样安全，并将展示如何使用我们的验证框架来检测第二个接口中的机密泄漏。我们假设高安全性通道与登录密码相关联，低安全性通道与用户名相关联。这可能意味着，例如，输入到名称框中的文本在屏幕上回显，而输入到密码框中的条目被隐藏。每当用户按下Enter按钮时，数据就会被发送。认证机制的操作由图4（ 错 误 输 出 被 省 略 ） 。 我 们 区 分 两 种 情 况 下 的 不 正 确 的 输 入 表 示 的 过 渡IncompleteData和IncorrectData。当按下Enter键并且输入框中缺少用户名或密码时，身份验证过程将进入INCOMPLEX状态界面将显示相应的错误消息一旦用户确认，身份验证过程将返回到INIT状态。转换IncorrectData表示当提供了用户名和密码，但其中一些数据不正确。后在这种情况下，过程进入应答状态其思想是，出于安全原因，在身份验证过程中止交互（STOP状态）之前，允许使用不正确的数据进行单次身份验证尝试。最后，如果用户提供了正确的数据，则身份验证成功，该数据由从INIT或INIT状态可到达的LOGIN状态SAL对认证过程的规范是图1中图表的直接翻译。四、类型={A，B}表示两个输入框。每个框都有许多属性：位置、安全级别、“可见性”、标签、输入的文本和显示的文本，以范围为0的数组建模。因此，position[j]是一个记录，坐标字段为x和y，表示盒子j的左上角。 其宽度和高度由常数dx和dy表示。属性级别[j]是j的安全级别，其为低或低。32R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21高;显示[j]表示j是否显示（可见）。 属性label[j]是类型为{NameLabel，PasswordLabel}的值。最后，value[j]和display[j]分别表示输入的文本和显示的文本，当输入的文本被隐藏时，它们可以不同。 数组值和布尔值EnterPressed和Acknowledged是身份验证过程的输入，而position、displayed、label和display 以 及 布 尔 值 DisplayedEnter 、 IncompleteMsg 、 IncorrectMsg 、LastAttemptMsg、LoginMsg和AbortMsg是其输出。4.2用户模型现在我们为身份验证任务实例化通用模块User。我们首先指定具体用户模型的状态空间。对于每个输入框j，我们假设一个人要么看到它，要么看不到它，并感知它的标签和显示的文本，分别由seen[j]，label[j]和value[j]确认按钮是否处于活动状态的选项由EnterActive表示。该人还感知是否给出错误、警告或认证消息，由ErrorMsg、WarningMsg和LoginMsg表示。变量InputName和InputPass记录了两个框中的哪一个提示输入用户名，哪一个提示输入密码。最后，name和password表示用户认为是用户名和密码的值。所有这些组件形成一个记录类型In，它用于实例化User中相应的类型变量。接下来，我们指定与用户可能采取的操作相关的变量。输入到框j中的文本由value[j]表示。布 尔 值EnterPressed和Acknowledged表示是否按下了Enter按钮和确认消息的按钮。 这些组件形成记录类型Out。 我们假设用户记住自己的用户名、用户名和登录密码、密码。它们还记录是否已经在框j中键入了信息，表示为entered[j]（在确认错误消息时重置为false），并跟踪是否存在身份验证失败，表示为失败。 这些构成了一个记录类型Mem，它还在Out类型的组件中记录了前一步中采取的操作。围绕我们系统的现实是由记录类型Env给出的。它包括用户名、名称和正确的密码、口令。我们假设用户的身份验证知识包括需要通信（1）用户名和（2）登录密码。这些知识被指定为用户目标（数组目标的元素），通过将action guard和更新提供给输出组件来实例化对于传达用户名的目标，防护措施是看到一个输入框，被视为名称框。输出操作是输入用户感觉到的名称grd：=λ（in，numb，env）：in.seen[in.InputName]tout：=λ（in，out0，）：λ（out）：out = Default（out0.value）WITH.value[in.InputName]：= in.name其中Default（x）是一个字段值设置为x，所有其他字段设置为false的记录，因此断言没有其他操作。内存更新（略）只是记录所采取的操作。作为一个例子，我们将指定最复杂R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2133内存更新如下。传送登录密码的操作也以类似方式指定。由于环境更新不会改变任何东西（在所有操作中），因此在这里省略了它们。我们假设用户可以通过按下它来对活动的Enter按钮做出反应 要做到这一点，用户必须不记得身份验证失败。或者，如果出现这样的故障，我们希望用户更加小心，只有在两个输入框都被填充时才按 En te r ：grd：=λ（in，max，env）：in.EnterActive∧（不（失败））（输入的[输入的InputName]输入的[输入的InputPass]））输出：=λ（输入，输出0，输出）：λ（输出）：out= Default（out0.value）WITH.EnterPressed：=TRUE我们还假设用户可以确认错误消息。只有当消息被解释为错误信号时才会发生这种情况如存储器所指示的，在前一步骤中也必须没有发生确认。通过确认错误消息，用户在存储器中记录了失败的身份验证尝试的事实，并且grd：=λ（in，out0，env）：in.ErrorMsgNOT（.out.Acknowledged）tout：=λ（in，out0，）：λ（out）：out= Default（out0.value）WITH.Acknowledged：=TRUE确认：=λ（in，mem0，out）：λ（）：= mem0 WITH.失败：=TRUEWITH.entered：= [[j：]] WITH.out：= out如前所述，将传递名称和密码的需求建模为用户目标。然而，用户在试图实现这些目标时犯错误是合理的，例如，输入错误密码或在某些框为空时按Enter键。由于用户习惯，也可能发生错误;根据以前的经验，用户可能期望名称的输入框在密码. 在这种情况下，一旦确认了错误消息，系统就会提示进行新的身份验证尝试。我们假设用户会响应此提示。响应被建模为两个反应性动作。在密码的情况下，动作保护是看到输入框（对于相应的用户目标）并且在前一步骤中没有输入密码，如存储器所指示的。输出操作与对应的用户目标相同。最后，内存更新记录了输入密码的事实grd：=λ（in，numb，env）：in.seen[in.InputPass]numbNOT（.entered[in.InputPass]）失败tout：=λ（in，out0，）：λ（out）：out= Default（out0.value）WITH.value[in.InputPass]：= in.password密码：=λ（in，mem0，out）：λ（） ：= mem0WITH.entered[in.InputPass]：= TRUE WITH.out：= out输入名称的反应操作类似于上面的操作。Goal和wait谓词是用于实例化User的最后一个参数34R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21module. LoginMsg的显示确认了身份验证，这是主要目标。我们还假设不存在用户会感知为等待的建议的信号。该等等同器械的具体说明如下：PerceivedGoal =λ（in，n）：in.LoginMsgWait =λ（in，n）：n最后，通过使用刚刚定义的参数（目标、反应动作、感知目标和等待条件）实例化通用用户模型来定义身份验证任务的用户模型UserAuthenticate4.3用户解释到目前为止，我们已经指定了一个认证接口，并开发了一个正式的用户模型。实际上，这两种规范的状态空间是不同的。界面状态的变化首先由用户注意，然后由用户解释。接下来，我们指定这个解释，从而连接不同的状态空间。 特殊的-fication作为一个新的SAL模块，解释。模块是一个连接器，它的输入变量是接口的输出变量，输出变量，它是UserAuthenticate的输入（感知）组件模块（记录在）。在认证任务中，用户解释的关键方面是对两个输入框的含义（功能）的它们的功能是通过标签来表示的，然而，我们假设人们可能不会对标签给予足够的注意。相反，用户可能会认为名字框是第一位的。优先级的感知取决于界面窗口中框的布局（坐标）形式上，我们定义输入框i在j之前的条件如下（这里pos是一个坐标数组precedes（i，j，pos）=（pos[i].x+ dx pos[j].x≠ pos[i].y≤ pos[j].y）<（pos[i].x≤pos[j].x<直觉上，这意味着j被放在i的右边和底部。因此，图3中左侧界面中的名称框在密码框之前，而右侧界面中的两个框都不在另一现在我们正式定义用户对输入框功能的解释，这取决于它们的布局和标签。我们区分三种情况。首先，用户可以从标签判断输入框的功能：ByLabel（l，x）=（i，j）：l[i]=NameLabell[j]=PasswordLabelx.InputName=ix.InputPass=j第二，如果i在j之前，那么i被认为是一个名字，j是一个密码框：ByPrecedence（pos，x）=（i，j）：先于（i，j，pos）x.InputName=ix.InputPass=j用户可能会感到困惑。当两个输入框都不在另一个之前或它们的标签相同时，这是可能的;在这种情况下，关于框的功能的判断是随机的：R. Ruk estecna setal. /《理论与计算科学》选编183（2007）2135定义在∈{x：In|如果否（gg）则x.输入活动=显示输入活动x.seen=显示的值x.label=标签的值x.value=显示的值x.ErrorMsg=（不完整消息∨错误消息）x.WarningMsg =LastAttemptMsg x.LoginMsg = LoginMsg x.name = IFx.WarningMsg THEN env.name ELSIF mem.nameENDIF x.password = IFx.WarningMsg THEN env.passwordELSIF密码ENDIF密码IF x.WarningMsgTHEN ByLabel（label，x）ELSIFMajorChanges（p，position，l，label）THENByLabel（label，x）∨ByPrecedence（position，x）∨Random（position，label，x）ELSEx.InputName=s.InputNamex.InputPass=s.InputPassENDIF否则x =s ENDIF}过渡sJ=in;pJ=位置;lJ=标签图五. SAL中的用户解释Random（pos，l，x）=（l[A]=l[B]（i，j）：NOT（precedes（i，j，pos）x.InputNamex.InputPass用户解释被建模为SAL定义，它允许人们描述系统不变量。直观地说，这意味着每当等式的右边的值改变时，等式的左边就被更新 我们假设，一旦用户对一个目标或反应性动作做出了精神承诺，对界面输出的解释不会改变，直到相关的物理动作被执行。如果没有承诺，用户直接感知到回车按钮，显示的输入框及其标签和显示的文本，以及界面充分和传播因此，图5中的前七个合取式简单地将接口变量重命名为中记录的相应字段。对于用户名和密码，用户依赖于内存，除非显示警告消息。 如果是这样，我们希望用户足够小心，正确的价值观。为了简单起见，这里我们不考虑这是如何实现的（也许它们是从笔记本中获取的），假设使用环境规范中的值。如前所述，两个框中的哪一个用于名称，哪一个用于密码的感知更加复杂;这种感知的结果分别被分配给InputName和InputLabel。我们假设，在收到警告消息后，用户会变得更加小心，并通过标签来解释输入框。 否则，如果在框，解释是在上述三种情况之间的任意选择。如果没有重大变化，则框的解释与上一步相同辅助变量s、p和l不旨在表示认知方面直观地说，它们和相关的TRANSITION部分，存储允许指定该用户解释的先前解释36R. Ruk estecna setal. /《理论与计算科学》选编183（2007）21不会改变最后，主要变更（pos0、pos、l0、l）为（i，j）：precedes（i，j，pos 0）precedes（i，j，pos）诚然，这种试图正式指定用户如何感知输入框的尝试已经暗示了潜在的问题，甚至在实际验证之前。然而，我们的目标是开发一个解释的通用模型，它将把规范化过程变成通用模型的简单实例化。4.4验证我们已经指定了身份验证接口及其用户模型。现在可以分析这个交互系统的正确性。我们从界面开始，对输入框的布局没有任何约束（除了它们不相交之外）。可用性属性（1），即用户最终达到预期目标，是由交互系统满足的接下来，我们继续分析系统的安全方面尽管每个具体系统的安全属性可以单独指定，但我们更喜欢采用通用的方法，就像用户模型本身一样。因此，我们引入一个通用模块，测试器。其思想是，该模块与交互系统组成，监控设备和用户之间的通信。当安全性被破坏时，它将变量SecurityBreach设置为true。监视哪些安全方面由模块的实例化确定。它有三个参数。 类型变量Chan