Published in

Formal Aspects in Security and Trust, p. 129-144

DOI: 10.1007/0-387-24098-5_10

Links

Tools

Export citation

Search in Google Scholar

Complementing Computational Protocol Analysis with Formal Specifications

Journal article published in 1969 by Kim-Kwang Raymond Choo ORCID, Colin A. Boyd, Yvonne Hitchcock, Greg M. Maitland
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Green circle
Postprint: archiving allowed
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

The computational proof model of Bellare and Rogaway for cryptographic protocol analysis is complemented by providing a formal specification of the actions of the adversary and the protocol entities. This allows a matching model to be used in both a machine-generated analysis and a human-generated computational proof. Using a protocol of Jakobsson and Pointcheval as a case study, it is demonstrated that flaws in the protocol could have been found with this approach, providing evidence that the combination of human and computer analysis can be more effective than either alone. As well as finding the known flaw, previously unknown flaws in the protocol are discovered by the automatic analysis. Full Text at Springer, may require registration or fee