Inductive Verification of Smart Card Protocols
Inductive Verification of Smart Card Protocols
复制标题
智能卡协议的感应验证
DOI：
10.3233/jcs-2003-11103
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
G. Bella
中科院分区：
文献类型：
--
作者：
G. Bella
现有的方法的基础上归纳和定理证明是量身定制的安全协议，利用智能卡的验证。智能卡是模拟操作，因此只有他们的功能，而不是他们的实施技术，是感兴趣的。间谍可以窃取某些智能卡，并克隆其他智能卡，同时学习它们存储的秘密。在通用性方面，该方法可扩展到在代理和智能卡之间假设安全或不安全手段的协议，以及PIN操作或PIN较少的智能卡。在可扩展性方面，新的，依赖于应用程序的智能卡功能可以很容易地包括在内。该方法在Shoup和Rubin设计的密钥分配协议上进行了演示[30]，并且研究对于要满足的协议目标来说在智能卡上所必需的假设。它被发现，如果智能卡的数据总线是不可靠的，以产生输出在一个未指定的顺序，那么协议不确认的对等体的目标的机密性，认证，和密钥分配，因为缺乏明确性。一个简单的修复介绍和证明。
An existing approach based on induction and theorem proving is tailored to the verification of security protocols that make use of smart cards. Smart cards are modelled operationally, hence only their functionalities, rather than their implementative technicalities, are of interest. The spy can steal certain smart cards, and clone others while learning their stored secrets. In terms of generality, the approach scales up to protocols that assume secure or insecure means between agents and smart cards, as well as to smart cards being PIN-operated or PIN-less. In terms of extensibility, new, application-dependent smart card functionalities can be easily included.The approach is demonstrated on the key distribution protocol designed by Shoup and Rubin [30], and the assumptions are studied that are necessary on the smart cards for the protocol goals to be met. It is found that, if the data buses of the smart cards are unreliable as to produce outputs in an unspecified order, then the protocol does not confirm to the peers its goals of confidentiality, authentication, and key distribution because of lack of explicitness. A simple fix is introduced and proved.