A Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols

The verification of security protocols has attracted a lot of interest in the formal methods community, yielding two main verification approaches: i) state exploration, e.g. FDR [Gavin Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. In TACAs'96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pages 147–166, London, UK, 1996. Springer-Verlag] and OFMC [A.D. Basin, S. Mödersheim, and L. Viganò. An on-the-fly model-checker for security protocol analysis. In D. Gollmann and E. Snekkenes, editors, ESORICS'03: 8th European Symposium on Research in Computer Security, number 2808 in Lecture Notes in Computer Science, pages 253–270, Gjøvik, Norway, 2003. Springer-Verlag]; and ii) theorem proving, e.g. the Isabelle inductive method [Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal in Computer Security, 6(1-2):85–128, 1998] and Coral [G. Steel, A. Bundy, and M. Maidl. Attacking the asokan-ginzboorg protocol for key distribution in an ad-hoc bluetooth network using coral. In H. König, M. Heiner, and A. Wolisz, editors, IFIP TC6 /WG 6.1: Proceedings of 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems, volume 2767, pages 1–10, Berlin, Germany, 2003. FORTE 2003 (work in progress papers)]. Complementing formal methods, Abadi and Needham's principles aim to guide the design of security protocols in order to make them simple and, hopefully, correct [M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, 1996]. We are interested in a problem related to verification but far less explored: the correction of faulty security protocols. Experience has shown that the analysis of counterexamples or failed proof attempts often holds the key to the completion of proofs and for the correction of a faulty model. In this paper, we introduce a method for patching faulty security protocols that are susceptible to an interleaving-replay attack. Our method makes use of Abadi and Needham's principles for the prudent engineering practice for cryptographic protocols in order to guide the location of the fault in a protocol as well as the proposition of candidate patches. We have run a test on our method with encouraging results. The test set includes 21 faulty security protocols borrowed from the Clark-Jacob library [J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. Technical report, Department of Computer Science, University of York, November 1997. A complete specification of the Clark-Jacob library in CAPSL is available at http://www.cs.sri.com/millen/capsl/].     

Compositionality of Statically Scheduled IP

Timing Closure in presence of long global wire interconnects is one of the main current issues in System-on-Chip design. One proposed solution to the Timing Closure problem is Latency-Insensitive Design (LID) [Luca Carloni, Kenneth McMillan, and Alberto Sangiovanni-Vincentelli. Theory of latency-insensitive design. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 20(no. 9):pp. 1059–1076, 2001; Mario R. Casu and Luca Macchiarulo. A new approach to latency insensitive design. In DAC'04: Proceedings of the 41st annual conference on Design automation, pages 576–581, New York, NY, USA, 2004. ACM Press].It was noticed in [Mario R. Casu and Luca Macchiarulo. A new approach to latency insensitive design. In DAC '04: Proceedings of the 41st annual conference on Design automation, pages 576–581, New York, NY, USA, 2004. ACM Press] that, in many cases, the dynamically scheduled synchronisations introduced by latency-insensitive protocols could be computed off-line as a static periodic schedule. We showed in [Julien Boucaron, Jean-Vivien Millo, and Robert De Simone. Latency-insensitive design and central repetitive scheduling. In Formal Methods and Models for Co-Design, 2006. MEMOCODE'06. Proceedings. Fourth ACM and IEEE International Conference on, pages 175–183, Piscataway, NJ, USA, 2006. IEEE Press; Julien Boucaron, Jean-Vivien Millo, and Robert De Simone. Formal methods of scheduling for latency-insensitive designs. EURASIP journal on embedded system, 2007 (not yet published)] how this schedule could then be used to further optimize the protocol resources when they are found redundant. The purpose of the present paper is to study how the larger blocks, obtained as synchronous components interconnected by LID protocols optimized by static schedule informations, can be again made to operate with an environment that provides also I/O connections at its own (synchronous or GALS) rate.We also consider the case of multirate SoC, using results from SDF (Synchronous DataFlow) theory [Edward A. Lee and David G. Messerschmitt. Synchronous data flow. Proceeding of the IEEE, vol. 75(no. 9):pp. 1235–1245, 1987].     

Supporting Function Calls within PELCR

In [M. Pedicini and F. Quaglia. A parallel implementation for optimal lambda-calculus reduction PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 3–14, ACM, 2000, M. Pedicini and F. Quaglia. PELCR: Parallel environment for optimal lambda-calculus reduction. CoRR, cs.LO/0407055, accepted for publication on TOCL, ACM, 2005], PELCR has been introduced as an implementation derived from the Geometry of Interaction in order to perform virtual reduction on parallel/distributed computing systems.In this paper we provide an extension of PELCR with computational effects based on directed virtual reduction [V. Danos, M. Pedicini, and L. Regnier. Directed virtual reductions. In M. Bezem D. van Dalen, editor, LNCS 1258, pages 76–88. EACSL, Springer Verlag, 1997], namely a restriction of virtual reduction [V. Danos and L. Regnier. Local and asynchronous beta-reduction (an analysis of Girard's EX-formula). LICS, pages 296–306. IEEE Computer Society Press, 1993], which is a particular way to compute the Geometry of Interaction [J.-Y. Girard. Geometry of interaction 1: Interpretation of system F. In R. Ferro, et al. editors Logic Colloquium '88, pages 221–260. North-Holland, 1989] in analogy with Lamping's optimal reduction [J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. of 17th Annual ACM Symposium on Principles of Programming Languages. ACM, San Francisco, California, pages 16–30, 1990]. Moreover, the proposed solution preserves scalability of the parallelism arising from local and asynchronous reduction as studied in [M. Pedicini and F. Quaglia. PELCR: Parallel environment for optimal lambda-calculus reduction. CoRR, cs.LO/0407055, accepted for publication on TOCL, ACM, 2005].     

Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols

In this paper, we first define bisimulation-based non-deterministic admissible interference (BNAI), derive its process-theoretic characterisation and present a compositional verification method with respect to the main operators over communicating processes, generalising in this way the similar trace-based results obtained [J. Univ. Comput. Sci. 6 (2000) 1054] into the finer notion of observation-based bisimulation [Logic and Models of Concurrent Systems, 1985]. Like its trace-based version, BNAI admits information flow between secrecy levels only through a downgrader (e.g. a cryptosystem), but is phrased into a generalisation of observational equivalence [Communication and Concurrency, 1989]. We then describe an admissible interference-based method for the analysis of cryptographic protocols, extending, in a non-trivial way, the non-interference-based approach presented by Focardi et al. [Proceedings of DERA/RHUL Workshop on Secure Architectures and Information Flow, 2000]. Confidentiality and authentication for cryptoprotocols are defined in terms of BNAI and their respective bisimulation-based proof methods are derived. Finally, as a significant illustration of the method, we consider simple case studies: the paradigmatic examples of the Wide Mouthed Frog protocol [ACM Trans. Comput. Syst. 8 (1990) 18] and the Woo and Lam one-way authentication protocol [IEEE Comput. 25 (1992) 39]. The original idea of this methodology is to prove that the intruder may interfere with the protocol only through selected channels considered as admissible when leading to harmless interference.     

Symmetric authentication in a simulatable Dolev–Yao-style cryptographic library

Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev–Yao models. However, until recently it was not known whether a Dolev–Yao model could be implemented with real cryptography in a provably secure way under active attacks. For public-key encryption and signatures, this was recently shown, if one accepts a few additions to a typical Dolev–Yao model such as an operation that returns the length of a term.Here we extend this Dolev–Yao-style model, its realization, and the security proof to include a first symmetric primitive message authentication. This adds a major complication: we must deal with the exchange of secret keys. For symmetric authentication, we can allow this at any time, before or after the keys are first used for authentication, while working only with standard cryptographic assumptions.     

Safely composing security protocols

Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys. In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication. This work has been partly supported by the RNTL project POSé and the ARA SSIA Formacrypt.     

用BAN逻辑方法分析TLS协议

密码协议的形式化正在成为国际上研究的热点，通过形式化分析密码协议来判断密码协议是否安全可靠。BAN逻辑是最早提出、最为重要的一种安全协议分析方法，被广泛地用于密码协议的安全性证明。文章介绍了BAN逻辑和TLS协议，用BAN逻辑分析TLS协议，从而证明TLS协议的双方认证协议是完整的、没有漏洞的。     

A Compact Linear Translation for Bounded Model Checking

We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to the Separated Normal Form encoding proposed in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and extended to past time in [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)]: an initial phase involves putting LTL formulae into a normal form based on linear-time fixpoint characterisations of temporal operators.As with [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)] and [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200], the size of propositional formulae produced is linear in the model checking bound, but the constant of proportionality appears to be lower.A denotational approach is taken in the presentation which is significantly more rigorous than that in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)], and which provides an elegant alternative way of viewing fixpoint based translations in [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200] and [Biere, A., A. Cimatti, E. M. Clarke, O. Strichman and Y. Zhu, Bounded model checking, Advances in Computers 58 (2003)].     

无线传感器网中基于动态簇的密钥管理方案

提出一种能根据路由节点的剩余能量动态选择簇头的低能耗动态簇组网模型,并设计了相应的密钥管理方案.与以往的密钥管理方案相比,该方案给出一种新型密钥链,能确保某个传感节点预置密钥的丢失不威胁其他节点的安全性;提出三种以Hash函数为主的轻量级密码协议,能以低能耗的方式完成网络节点间的认证与簇密钥的分配;给出密码协议安全性的形式化分析,确保了协议本身的安全性.分析表明,该方案能够支持网络的扩展,并具有较好的安全性.     

一种基于非对称密码学的分布式认证方案

网络安全技术,特别是网络环境中的身份认证协议及系统,对于应用的安全起着非常重要的作用,并已经成为影响网络进一步发展的重要因素。在开放网络中真正安全可靠的是密码学身份认证协议,根据密码学基础可分为基于对称密码和非对称密码两大类。通过对经典的kerberos系统的分析,给出了与非对称密码系统结合的改进方法,增强了其安全性和可扩展性。     

OpenID身份认证系统的认证等级模型研究

以OpenID为现有的切入点,分析了现代分布式认证体系中,依赖站点和用户对认证协议安全性方面的需求,提出了对OpenID协议的扩展,根据不同的认证需求定义了4种不同的认证等级,从匿名性、完整性和不可伪造性3个特性上对认证等级进行了研究,并给出了解决方法和密码学算法。同时,协议能够通过满足完整性和不可伪造性,提高用户对依赖站点的信任度。这一认证等级的提出,可以为各类网络服务的定位提供参考,也为用户在选择依赖站点的判断上,提供了安全性方面的衡量标准。     

RFID超轻量级认证协议RCIA形式化分析与改进

无线射频识别（RFID）是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。     

Discounting Infinite Games But How and Why?

In a recent paper de Alfaro, Henzinger and Majumdar [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] observed that discounting successive payments, the procedure that is employed in the classical stochastic game theory since the seminal paper of Shapley [L.S. Shapley. Stochastic games. Proceedings Nat. Acad. of Science USA, 39:1095–1100, 1953], is also pertinent in the context of much more recent theory of stochastic parity games [L. de Alfaro and R. Majumdar. Quantitative solution to omega-regular games. In STOC'01, pages 675–683. ACM Press, 2001. final version to appear in Journal of Computer and System Sciences, L. de Alfaro, T.A. Henzinger, and O. Kupferman. Concurrent reachability games. In FOCS'98, pages 564–575. IEEE Computer Society Press, 1998, L. de Alfaro and T.A. Henzinger. Concurrent ω-regular games. In LICS'00, pages 142–154. IEEE Computer Society Press, 2000] which were proposed as a tool for verification of probabilistic systems. We show that, surprisingly perhaps, the particular discounting used in [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] is in fact very close to the original ideas of Shapley. This observation allows to realize that the specific discounting of [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] suffers in fact from some needless restrictions. We advocate that dropping the constraints imposed in [Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In ICALP 2003, volume 2719 of LNCS, pages 1022–1037. Springer, 2003] leads to a more general and elegant theory that includes parity and mean payoff games as particular limit cases.     

基于Petri网的密码协议分析

在Federico提出的一种密码协议进程语言的基础上,建立了便于进行密码协议分析的简化Petri网模型,给出了协议满足秘密性的充要条件,并以NS公钥协议为例,用Petri网模型,结合归纳方法和串空间分析方法从密钥、新鲜数和协议主体三个方面的秘密性分析了该协议的秘密性,简化了协议秘密性的分析。     

适应受限环境的认证协议及其SVO逻辑分析

针对认证协议在受限通信网络环境中的应用和安全问题,提出一种基于椭圆曲线密码技术的认证协议,使用对称密码为协议中的交互信息提供机密性,在协议最后生成参与者共享的会话密钥。采用扩展的SVO逻辑对推荐协议进行形式化分析,结果证明该协议的安全性符合要求。     

On the Relative Soundness of the Free Algebra Model for Public Key Encryption

Formal systems for cryptographic protocol analysis typically model cryptosystems in terms of free algebras. Modeling the behavior of a cryptosystem in terms of rewrite rules is more expressive, however, and there are some attacks that can only be discovered when rewrite rules are used. But free algebras are more efficient, and appear to be sound for “most” protocols. In [J. Millen, “On the freedom of decryption”, Information Processing Letters 86 (6) (June 2003) 329–333] Millen formalizes this intuition for shared key cryptography and provides conditions under which it holds; that is, conditions under which security for a free algebra version of the protocol implies security of the version using rewrite rules. Moreover, these conditions fit well with accepted best practice for protocol design. However, he left public key cryptography as an open problem. In this paper, we show how Millen's approach can be extended to public key cryptography, giving conditions under which security for the free algebra model implies security for the rewrite rule model. As in the case for shared key cryptography, our conditions correspond to standard best practice for protocol design.     

On the decidability of cryptographic protocols with open-ended data structures

Formal analysis of cryptographic protocols has concentrated mainly on protocols with closed-ended data structures, i.e., protocols where the messages exchanged between principals have fixed and finite format. In many protocols, however, the data structures used are open-ended, i.e., messages have an unbounded number of data fields. In this paper, decidability issues for such protocols are studied. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.     

基于形式方法的Andrew RPC认证协议的分析与改进

密码协议安全性分析是网络安全的一个难题，运用形式方法对密码协议进行分析一直是该领域的研究热点。运用BAN逻辑对Andrew RPC（Remote Procedure Call）认证协议进行了形式分析，发现了协议中存在的安全缺陷。对协议进行改进，并给出改进后的安全协议。     

认证协议安全性的非形式化分析

安全协议特别是认证协议的非形式化分析在复杂的现代通信中变得尤其重要.本文指出著名的Abadi安全协议设计原则和Lin等文献中关于漏洞的分析以及使协议更安全的建议存在不准确性,从而使我们能够给出其协议修正版本的攻击.通过对安全协议不安全实质的分析,文章指出实现安全认证协议的必要条件:主体的活现性和新鲜性标志符的新鲜性和关联性.最后,以问答式认证协议为例,指出了保证主体的活现性和新鲜性标志符的新鲜性和关联性的方法.     

基于CCS的加密协议分析

加密协议的分析需要形式化的方法和工具.该文定义了加密协议描述语言PEP (principals+environment=protocol),并说明对于一类加密协议,其PEP描述可以转化为有穷的基本CCS进程,由此可以在基于CCS的CWB(concurrency workbench)工具中分析加密协议的性质.此方法的优点在于隐式地刻画攻击者的行为,试图通过模型检查(model checking)发现协议潜在的安全漏洞,找到攻击协议的途径.