Biblio

Public key cryptographic primitive (e.g., the famous Diffie-Hellman key agreement, or public key encryption) has recently been used as a standard building block in authenticated key agreement (AKA) constructions for wireless sensor networks (WSNs) to provide perfect forward secrecy (PFS), where the expensive cryptographic operation (i.e., exponentiation calculation) is involved. However, realizing such complex computation on resource-constrained wireless sensors is inefficient and even impossible on some devices. In this work, we introduce a new AKA scheme with PFS for WSNs without using any public key cryptographic primitive. To achieve PFS, we rely on a new dynamic one-time authentication credential that is regularly updated in each session. In particular, each value of the authentication credential is wisely associated with at most one session key that enables us to fulfill the security goal of PFS. Furthermore, the proposed scheme enables the principals to identify whether they have been impersonated previously. We highlight that our scheme can be very efficiently implemented on sensors since only hash function and XOR operation are required.

Global Platform (GP)1 specifications accepted as de facto industry standards are widely used for the development of embedded operating system running on secure chip devices. A promising approach to demonstrating the implementation of an OS meets its specification is formal verification. However, most previous work on operating system verification targets high-level source programs proving the correspondence between abstract specification and high-level implementation but ignoring the machine-code level implementation parts. Thus, this kind of correspondence proofs stay in a shallow level. In this paper, we present a novel methodology for formal specifying and certifying the implementation of an embedded operating system strictly follows the GP specification. We establish a multiple abstraction layers framework that has four layers, from up to down, which are Formal Global Platform Layer (FGPL), Formal Specification High Layer (FSHL), Formal Specification Low Layer (FSLL) and Formal Assembly Machine Layer (FAML). To demonstrate the effectiveness of our methodology, we take the communication module of our Trust-E operating system (running on an extended CompCert ARM assembly machine model) as a case study and have successfully constructed a multi-layered proof, fully formalized in the Coq proof assistant. Some parts of the module are written in C and some are written in assembly; we certify that all codes implementation follow Global Platform specification.