Showing 1–2 of 2 results for author: Ye, K Q

Verified Correctness and Security of mbedTLS HMAC-DRBG

Authors: Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel

Abstract: We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C program) correctly implements this functional specification. That proof composes with an existing C compiler correctness proof to guarantee, end-to-end, th… ▽ More We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C program) correctly implements this functional specification. That proof composes with an existing C compiler correctness proof to guarantee, end-to-end, that the machine language program gives strong pseudorandomness. All proofs (hybrid games, C program verification, compiler, and their composition) are machine-checked in the Coq proof assistant. Our proofs are modular: the hybrid game proof holds on any implementation of HMAC-DRBG that satisfies our functional specification. Therefore, our functional specification can serve as a high-assurance reference. △ Less

Submitted 28 August, 2017; originally announced August 2017.

Comments: Appearing in CCS '17

Geometric isomorphism and minimum aberration for factorial designs with quantitative factors

Authors: Shao-Wei Cheng, Kenny Q. Ye

Abstract: Factorial designs have broad applications in agricultural, engineering and scientific studies. In constructing and studying properties of factorial designs, traditional design theory treats all factors as nominal. However, this is not appropriate for experiments that involve quantitative factors. For designs with quantitative factors, level permutation of one or more factors in a design matrix c… ▽ More Factorial designs have broad applications in agricultural, engineering and scientific studies. In constructing and studying properties of factorial designs, traditional design theory treats all factors as nominal. However, this is not appropriate for experiments that involve quantitative factors. For designs with quantitative factors, level permutation of one or more factors in a design matrix could result in different geometric structures, and, thus, different design properties. In this paper indicator functions are introduced to represent factorial designs. A polynomial form of indicator functions is used to characterize the geometric structure of those designs. Geometric isomorphism is defined for classifying designs with quantitative factors. Based on indicator functions, a new aberration criteria is proposed and some minimum aberration designs are presented. △ Less

Submitted 29 March, 2005; originally announced March 2005.

Comments: Published at http://dx.doi.org/10.1214/009053604000000599 in the Annals of Statistics (http://www.imstat.org/aos/) by the Institute of Mathematical Statistics (http://www.imstat.org)

Report number: IMS-AOS-AOS257 MSC Class: 62K15; 62K20. (Primary)

Journal ref: Annals of Statistics 2004, Vol. 32, No. 5, 2168-2185