Security protocol verification using commonly-used model-checkers or symbolic protocol verifiers has several intrinsic limitations. Spin suffers the state explosion problem; Proverif may report false attacks. An alternative approach is to use Coq. However, the effort required to verify protocols in Coq is high for two main reasons: correct protocol and property specification is a non-trivial task, and security proofs lack automation. This work claims that (1) using Coq for verification of cryptographic protocols can sometimes yield better results than Spin and Proverif, and (2) the verification process in Coq can be greatly alleviated if specification and proof engineering techniques are applied. Our approach is evaluated by verifying several representative case studies. Preliminary results are encouraging, we were able to verify two protocols that give imprecise results in Spin and Proverif, respectively. Further, we have automated proofs of secrecy and authentication for an important class of protocols.

Reconstructing system-level behavior from silicon traces is a critical problem in post-silicon validation of System-on-Chip designs. Current industrial practice in this area is primarily manual, depending on collaborative insights of the architects, designers, and validators. This paper presents a trace analysis approach that exploits architectural models of system-level protocols to reconstruct design behavior from partially observed silicon traces in the presence of ambiguous and noisy data. The output of the approach is a set of all potential interpretations of a system's internal execution abstracted to system-level protocols. To support the trace analysis approach, a companion trace signal selection framework guided by system-level protocols is also presented, and its impacts on the complexity and accuracy of the analysis approach are discussed. That approach and the framework have been evaluated on a multi-core System-on-Chip prototype that implements a set of common industrial system-level protocols.