secFleck: A Public Key Technology Platform for Wireless Sensor Networks

We describe the design and implementation of a public-key platform, secFleck, based on a commodity Trusted Platform Module (TPM) chip that extends the capability of a standard node. Unlike previous software public-key implementations this approach provides E- Commerce grade security; is computationally fast, energy efficient; and has low financial cost — all essential attributes for secure large-scale sen- sor networks. We describe the secFleck message security services such as confidentiality, authenticity and integrity, and present performance re- sults including computation time, energy consumption and cost. This is followed by examples, built on secFleck, of symmetric key management, secure RPC and secure software update.

Towards trusted wireless sensor networks

This article presents the design and implementation of a trusted sensor node that provides Internet-grade security at low system cost. We describe trustedFleck, which uses a commodity Trusted Platform Module (TPM) chip to extend the capabilities of a standard wireless sensor node to provide security services such as message integrity, confidentiality, authenticity, and system integrity based on RSA public-key and XTEA-based symmetric-key cryptography. In addition trustedFleck provides secure storage of private keys and provides platform configuration registers (PCRs) to store system configurations and detect code tampering. We analyze system performance using metrics that are important for WSN applications such as computation time, memory size, energy consumption and cost. Our results show that trustedFleck significantly outperforms previous approaches (e.g., TinyECC) in terms of these metrics while providing stronger security levels. Finally, we describe a number of examples, built on trustedFleck, of symmetric key management, secure RPC, secure software update, and remote attestation.

Poster Abstract : A public key technology platform for wireless sensor networks

Communication security for wireless sensor networks (WSN) is a challenge due to the limited computation and energy resources available at nodes. We describe the design and implementation of a public-key (PK) platform based on a standard Trusted Platform Module (TPM) chip that extends the capability of a standard node. The result facilitates message security services such as confidentiality, authenticity and integrity. We present results including computation time, energy consumption and cost.

Analysis of Object-Specific Authorization Protocol (OSAP) using coloured Petri nets

The use of Trusted Platform Module (TPM) is be- coming increasingly popular in many security sys- tems. To access objects protected by TPM (such as cryptographic keys), several cryptographic proto- cols, such as the Object Specific Authorization Pro- tocol (OSAP), can be used. Given the sensitivity and the importance of those objects protected by TPM, the security of this protocol is vital. Formal meth- ods allow a precise and complete analysis of crypto- graphic protocols such that their security properties can be asserted with high assurance. Unfortunately, formal verification of these protocols are limited, de- spite the abundance of formal tools that one can use. In this paper, we demonstrate the use of Coloured Petri Nets (CPN) - a type of formal technique, to formally model the OSAP. Using this model, we then verify the authentication property of this protocol us- ing the state space analysis technique. The results of analysis demonstrates that as reported by Chen and Ryan the authentication property of OSAP can be violated.

Security properties analysis in a TPM-based protocol

Security protocols are designed in order to provide security properties (goals). They achieve their goals using cryptographic primitives such as key agreement or hash functions. Security analysis tools are used in order to verify whether a security protocol achieves its goals or not. The analysed property by specific purpose tools are predefined properties such as secrecy (confidentiality), authentication or non-repudiation. There are security goals that are defined by the user in systems with security requirements. Analysis of these properties is possible with general purpose analysis tools such as coloured petri nets (CPN). This research analyses two security properties that are defined in a protocol that is based on trusted platform module (TPM). The analysed protocol is proposed by Delaune to use TPM capabilities and secrets in order to open only one secret from two submitted secrets to a recipient

Analysis of two authorization protocols using Colored Petri Nets

To prevent unauthorized access to protected trusted platform module (TPM) objects, authorization protocols, such as the object-specific authorization protocol (OSAP), have been introduced by the trusted computing group (TCG). By using OSAP, processes trying to gain access to the protected TPM objects need to prove their knowledge of relevant authorization data before access to the objects can be granted. Chen and Ryan’s 2009 analysis has demonstrated OSAP’s authentication vulnerability in sessions with shared authorization data. They also proposed the Session Key Authorization Protocol (SKAP) with fewer stages as an alternative to OSAP. Chen and Ryan’s analysis of SKAP using ProVerif proves the authentication property. The purpose of this paper was to examine the usefulness of Colored Petri Nets (CPN) and CPN Tools for security analysis. Using OSAP and SKAP as case studies, we construct intruder and authentication property models in CPN. CPN Tools is used to verify the authentication property using a Dolev–Yao-based model. Verification of the authentication property in both models using the state space tool produces results consistent with those of Chen and Ryan.

可信平台模块的形式化分析和测试

可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础,可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段,但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法,同时可信计算组织给出的TPM规范是描述性的,不利于产品的开发和测试.文中在分析可信平台模块目前存在的一些问题的基础上,以TPM密码子系统为例给出了该子系统的形式化规格说明,并且基于该规格说明,给出了扩展有限状态机模型,最后,将该有限状态机模型应用于测试用例的自动生成,并通过实验验证了形式化测试的有效性.

可信平台模块分析与测试技术研究

在可信计算平台的体系结构中，可信平台模块的基础性地位决定了其在可信计算平台的研究中居于中心的地位。本文对可信平台模块中可信机制特别是隐私性保护机制进行了详细的分析，并以可信平台模块作为建模的对象，对其进行形式化分析，探讨利用形式化模型生成测试用例，进行符合性测试的技术。本文主要取得了以下几个方面的成果： 1、针对现有的隐私性保护方案即BCC方案在多信任域环境下的不足，提出了一种多信任域内的直接匿名证明方案，该方案为直接匿名证明方案在多信任域的网络环境下的应用奠定了基础。 2、针对BCC方案匿名性机制中“验证着相关的完全或无”匿名性的缺陷，提出了带子群隐私保护的隐私性保护方案，该方案为小群体内应用隐私性保护方案提供了可行的解决方法，增强了现有隐私性保护方案匿名机制的灵活性。 3、提出了一种新的基于双线性映射的直接匿名证明方案，该方案的计算量小，签名长度短，为下一代基于椭圆曲线的可信平台模块提供了可行的隐私性保护方案。 4、针对目前可信平台模块符合性测试缺少自动化测试方案的现实，本文提出了一个新的针对可信平台模块的测试方案，该方案利用EFSM形式化模型生成测试用例，支持覆盖度的分析，可以实现测试的自动化，在符合性测试中可以帮助提高测试的覆盖程度与工作效率。 5、最后，本文首次对可信平台模块的本地化产品可信密码模块进行了系统的分析，指出了其中的AP授权协议的一些缺陷，并给出了改进意见，对可信密码模块和可信平台模块进行了详细的对比和分析，指出可信密码模块存在的不足和优势。 总的说来，本文的研究成果为可信平台模块的推广提供了有力的支撑，并且为我国可信密码模块的发展提供了借鉴。 关键词：可信平台模块、可信计算平台、 符合性测试、直接匿名证明

an integrity assurance mechanism for run-time programs

Chinese Assoc Cryptol Res, State Key Lab Informat Secur, Inst Software, Grad Univ Chinese Acad Sci, Natl Nat Sci Fdn China

An efficient anonymous remote attestation scheme for trusted computing based on improved CPK

 The platform remote attestation (RA) is one of the main features of trusted computing platform proposed by the trusted computing group (TCG). The privacy certificate authority (CA) solution of RA requires users to pay for multiple certificates, and the direct anonymous attestation (DAA) solution leads to inefficiency. TCG RA also suffers from limitations of platform configuration privacy. This paper proposed a RA scheme based on an improved combined public key cryptography (ICPK) (abbreviated to RA-ICPK). RA-ICPK is a certificate-less scheme without using public key infrastructure CA signature or DAA signature, which combines commitment scheme, zero-knowledge proof and ring signature (RS) to own the property of unforgeability and privacy. RA-ICPK is mainly based on elliptic curve cryptography without bilinear pair computing, and only carries out zero-knowledge proof one time. RA-ICPK need not depend on trusted third parties to check trusted platform modules identity and integrity values revocations. © 2014 Springer Science+Business Media New York

Certified pseudonyms colligated with master secret key

A pseudonym provides anonymity by protecting the identity of a legitimate user. A user with a pseudonym can interact with an unknown entity and be confident that his/her identity is secret even if the other entity is dishonest. In this work, we present a system that allows users to create pseudonyms from a trusted master public-secret key pair. The proposed system is based on the intractability of factoring and finding square roots of a quadratic residue modulo a composite number, where the composite number is a product of two large primes. Our proposal is different from previously published pseudonym systems, as in addition to standard notion of protecting privacy of an user, our system offers colligation between seemingly independent pseudonyms. This new property when combined with a trusted platform that stores a master secret key is extremely beneficial to an user as it offers a convenient way to generate a large number of pseudonyms using relatively small storage.

基于可信平台的安全审计日志

任何的安全系统，审计日志都是非常重要的一部分．因此必须保护好审计日志，保证审计日志的保密性和完整性．安全审计日志机制就是为了保护日志系统自身的安全性的，Schneier和Kelsey提出了一种机制来实现日志的防篡改，可以很好地保护系统生成的日志，但是该机制需要依赖于可信服务器．初步探索了可信平台上的安全审计日志机制，并且提出了一种新的日志机制来保护可信平台上生成的日志．该日志机制建立在微软提出的NGSCB平台上，不需要依赖于可信服务器．

基于可信平台的一种访问控制策略框架——TXACML

根据可信平台访问控制需求,提出一个可信平台属性分类规则,定义属性评估函数,可以实现可信平台数据安全分发和访问.同时针对XACML现有的策略合成算法不能有效满足可信平台自动方策略复合需求,设计了一个基于平台可信度的策略合成算法,该算法可以使策略的优先级和可信度保持一致,实现自动方策略复合.在此基础上,进一步对XACML实施扩展,形成可信平台策略语言框架TXACML(XACML based on trusted platform).采取TXACML对一个实例给出了策略描述和策略合成过程,验证了TXACML的有效性.

可信密码模块符合性测试方法研究

提出了一种可信密码模块(TCM)符合性测试的形式化方法,采用基于扩展有限状态机(EFSM)模型与测试向量相结合的方式对TCM的标准进行形式化建模.由于该建模方法结合TCM自身特点给出了命令依赖关系图的获取算法以及EFSM模型与测试向量获取算法,所以能够更好地对标准进行形式化建模,并用于测试用例的产生.通过测试结果分析以及与其他相关工作的对比,表明该方法能够有效地产生测试用例,并提高TCM符合性测试的错误检测率.

Secure tracking using trusted GNSS receivers and Galileo authentication services

This paper describes a secure framework for tracking applications that use the Galileo signal authentication services. First a number of limitations that affect the trust of critical tracking applications, even in presence of authenticated GNSS signals, are detailed. Requirements for secure tracking are then introduced; detailing how the integrity characteristics of the Galileo authentication could enhance the security of active tracking applications. This paper concludes with a discussion of our existing tracking technology using a Siemens TC45 GSM/GPRS module and future development utilizing our previously proposed trusted GNSS receiver.