该论文关注的是一个长期被忽视但至关重要的问题：密码学协议形式化验证工具（尤其是 Tamarin、ProVerif 及同类协议验证器）在实际使用中的可用性问题。作者指出，尽管这类工具被广泛用于分析复杂安全协议（如 TLS、SSH、信号协议、认证与密钥交换协议等）的安全性质，但关于『真实用户如何使用这些工具、在哪些环节遇到困难』的实证研究仍相当匮乏，工具设计者往往缺乏来自一线的反馈依据。为此，作者开展了一项以人为中心的探索性研究（human-centered exploratory study），通过问卷调查的形式，系统性收集了具备实际使用经验的用户反馈。受访群体包括研究人员、研究生以及工业界从业者，均具有使用 Tamarin、ProVerif 或相关工具的动手经验，覆盖面兼顾学术与工程两侧。研究结果揭示了贯穿整个验证工作流的多个可用性障碍：其一，当验证过程出现不终止（non-termination）或性能瓶颈时，用户难以进行有效的调试与定位，缺乏可操作的诊断信息；其二，缺乏系统化方法将形式化模型与真实世界协议实现进行对照校验，用户很难判断『模型是否忠实反映了真实协议』，这直接影响验证结论的可信度；其三，当证明失败但没有给出具体攻击路径（concrete attack）时，用户普遍采取的经验性应对策略是简化模型、补充辅助引理（helper lemmas）、或反复回溯并调整建模抽象层次，整个过程高度依赖个人经验与试错，缺少方法学支撑。此外，受访者明确提出了对可操作诊断、更清晰的结果解释、可视化能力以及对重复性证明任务自动化的需求。作者的核心论断是：这些持续存在的可用性挑战，根源在于『协议层面的推理方式』与『验证器的形式化模型、证明过程及诊断输出』之间存在语义与认知上的鸿沟。基于上述发现，论文提炼出一组具体的设计优先级，用于提升密码协议验证工具的可访问性、可解释性与易用性。该工作属于典型的可用性/人机交互与形式化方法交叉研究，适合形式化验证工具开发者、协议安全研究者、以及需要将形式化验证引入工程流程的安全团队阅读。

该研究聚焦于在线平台内置隐私功能在实现匿名性方面的可用性问题，以经期与生育追踪（PFT）应用为研究场景。由于生殖健康数据具有高度敏感性，用户面临数据监控与隐私泄露的风险，对匿名保护功能（APFs）的需求尤为迫切。研究招募了32名参与者，对六款PFT应用进行了可用性测试，考察用户在使用匿名保护功能时的实际体验与感知。结果显示，这些功能的可用性显著影响用户对隐私安全的整体感知。主要可用性挑战包括：匿名保护功能缺乏透明度，用户难以理解其存在与工作原理；避免泄露个人身份信息（PII）的操作流程不直观，容易导致误操作。基于这些问题，作者提出了提升在线平台匿名功能可访问性与可用性的设计建议，旨在帮助非技术用户更有效地管理隐私。该研究将可用性测试方法引入生殖健康隐私场景，为隐私设计与人机交互领域提供了实证依据。适合隐私保护设计者、PFT应用开发者、信息安全与可用性交叉领域的研究人员阅读。

该研究围绕风险认证（Risk-based Authentication, RBA）通知的用户感知与反应展开。随着在线账户攻击日益频繁，许多服务引入RBA机制，通过判断登录上下文的风险等级触发额外验证或告警。然而，用户对这些通知的认知度偏低、影响行为的效果未知。论文通过设计问卷或控制实验，招募参与者评估不同类型的风险通知（如新设备登录确认、异地登录告警、异常活动提示），测量用户的信任程度、理解能力、焦虑感以及采取安全行动的意愿。实验结果表明，通知内容的明确性、来源可信度、上下文相关性和操作便捷性显著影响用户响应；过高的授权频率可能导致“通知疲劳”和习惯性点击。基于结果，作者提出多项可操作建议，如优化通知文案、提供明确的安全选项、结合用户历史行为个性化告警，以提升用户决策质量。该研究为人机交互（HCI）与账号安全策略的交叉领域提供了实证数据，适合安全产品设计师、用户行为研究者和认证方案开发人员阅读。

数字取证已成为现代刑事诉讼中的关键组成部分，但随着数据量的增长、技术的持续演进以及技术和法律相关方之间的复杂交互，其有效整合面临挑战。以往研究主要聚焦于数字取证工具和方法本身，对更广泛的流程和组织背景关注不足。本文借鉴可用性研究和以人为中心的安全视角，将数字取证定位为刑事诉讼中的一个社会技术系统。基于此，作者对德国北莱茵-威斯特法伦州的 101 名司法实务人员（包括检察官、法官和数字取证专家）进行了问卷调查，以探索该系统的现状和需求。调查结果显示，从业者对将数字取证更好地整合进工作流程有强烈需求，认为需要改进跨领域沟通，并使不同利益相关者的期望更加一致。此外，研究揭示了数字取证可用性的巨大改进潜力，例如通过加强跨学科合作、提供更便捷快速的证据数据和结果访问途径，以及改进相关人员的培训和教育。作者认为，这项研究为理解数字取证在司法系统中的实际应用提供了新的视角，并为后续研究和实践改进指明了方向。

该论文聚焦于时间受限的交互式认证系统（如基于USSD的金融服务）中的失败动态。这类系统受限于严格的会话时长和顺序用户交互，虽然更强的认证机制提升了安全性，但增加了交互复杂性和时间负担，可能导致交易完成率下降。作者首先通过分析认证复杂度、用户响应时间和网络往返时间之间的相互作用，定义了会话成功率的非线性下降现象，即“成功悬崖”（Success Cliff）——当复杂度超过某个临界阈值后，成功率急剧下降。然后，作者提出并实现了一个基于仿真的框架来研究这些失败动态。通过控制实验，论文量化了安全性与可用性之间的权衡，并识别了哪些条件下安全的认证工作流会变得操作不可靠。主要贡献包括：形式化定义成功悬崖、提出仿真方法论、以及为设计兼顾安全与可用性的时间受限认证系统提供指导。适合安全工程师、人机交互研究人员以及金融科技开发者阅读。

该论文提出并实现了一种基于孟加拉语的文本验证码（CAPTCHA）机制，旨在解决传统英语验证码对非英语母语用户存在的可用性问题。这是首个针对孟加拉语用户的文本验证码方案。作者设计了6种变体，并通过6000个挑战（每种变体约1000个）进行自动化OCR攻击测试，平均字符识别率仅为0-20%，表明其具有较强的安全性。同时，通过110名参与者的用户可用性评估，6种变体的成功率为56.25%至90.29%，平均响应时间为6.69至9.9秒，在文本验证码基准中表现突出。论文详细阐述了设计原理、实现细节以及实验结果，证明了该方案在安全性和可用性之间的良好平衡。研究为区域语言用户提供了更友好的安全防护手段，并为未来多语言验证码设计提供了参考。

该论文通过实地调查和半结构化访谈，深入研究了肯尼亚网吧（cybercafe）中用户和工作人员面临的安全与隐私挑战。研究在肯尼亚的两个城市（内罗毕和基苏木）进行，共调查了200名用户和26名网吧工作人员。主要发现包括：（1）高达80%的用户在创建或输入密码时依赖工作人员代为操作，工作人员因此掌握了大量用户的账户凭证；（2）网吧工作人员经常将用户凭证存储在不安全的电子表格或纸质记录中，甚至通过WhatsApp等聊天工具共享，存在严重的泄露风险；（3）用户普遍缺乏基本的安全意识，例如不验证网站HTTPS证书、不知道公共计算机的键盘记录风险；（4）网吧缺乏正式的安全策略，工作人员也未经培训；（5）用户出于成本、设备可及性等原因被迫使用网吧，缺乏替代选择。论文揭示了资源受限环境下安全设计与实际使用之间的巨大鸿沟，并提出了针对性的设计建议，例如构建无密码身份验证方案、提供临时会话机制等。该研究对于理解发展中国家数字鸿沟中的安全隐私问题具有重要价值。

本文采用混合研究方法，系统性地分析了云服务配置中的安全与隐私挑战。研究团队对2008年至2024年间约251,900篇与安全及隐私相关的Stack Overflow帖子进行了主题建模和定性分析，旨在映射云使用场景与其对应的安全配置问题。研究发现，配置错误的主要原因包括云平台本身的复杂性、文档不足以及缺乏针对用户环境的上下文感知工具。特别值得注意的是，身份验证和访问控制问题在所有识别出的使用场景中普遍存在，几乎贯穿云部署、集成和维护的各个阶段。该研究不仅揭示了技术性难题（如错误的IAM策略设置），还指出了人为因素（如开发人员对权限模型理解不足）。作者强调，需要开发可用性强、定制化且具备上下文感知能力的支持工具和资源，以帮助开发者安全地配置云服务。本文的主要贡献在于提供了一个全面的云安全配置挑战图谱，为后续研究设计更友好的配置工具提供了实证基础。适合云安全研究人员、DevSecOps从业者以及云服务提供商阅读。