Biblio

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

A method for the multiple faults diagnosis in linear analog circuits is presented in this paper. The proposed approach is based upon the concept named by the indirect compensation theorem. This theorem is reducing the procedure of fault diagnosis in the analog circuit to the symbolic analysis process. An extension of the indirect compensation theorem for the linear subcircuit is proposed. The indirect compensation provides equivalent replacement of the n-ports subcircuit by n norators and n fixators of voltages and currents. The proposed multiple faults diagnosis techniques can be used for evaluation of any kind of terminal characteristics of the two-port network. For calculation of the circuit determinant expressions, the Generalized Parameter Extraction Method is implemented. The main advantage of the analysis method is that it is cancellation free. It requires neither matrix nor ordinary graph description of the circuit. The process of symbolic circuit analysis is automated by the freeware computer program Cirsym which can be used online. The experimental results are presented to show the efficiency and reliability of the proposed technique.