一、简介

     Scavel 协议可信性验证系统(Protocol Credibility Verification system,PCVs)，是系统可信性自动验证国家地方联合工程实验室在系统可信性验证相关理论与技术方面积累大量原创性研究成果的基础上, 开发的基于符号模型检测且以定理证明和逻辑推理原创科研成果为核心的协议验证系统。

二、功能

      (1)构建协议的形式化模型、安全性质

      (2)验证协议的安全性

三、特点

      (1)支持机密性、认证性、不可链接性、等价性、隐私性、匿名性等性质;

      (2)支持车联网、物联网、工业互联网、智能电网等多关键信息基础设施领域协议;
      (3)支持常见攻击类型验证，如去同步攻击、重放攻击、假冒攻击、中间人攻击等。

四、适用性

      (1)支持 Windows 操作系统

      (2)支持 Kylin、Neokylin 系统。