The Interrogator model
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The Interrogator is a protocol security analysis tool implemented in Prolog and based on a communicating-machine message transformation model with message modification threats. It supports a large and extendible class of symbolic encryption and data transformation operators with a novel equation-solving approach in the context of equational theories. The operator representation and equation-solving capability has a simple interface to the protocol and threat model.Keywords
This publication has 19 references indexed in Scilit:
- On unifying some cryptographic protocol logicsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Proof of soundness (integrity) of cryptographic protocolsJournal of Cryptology, 1994
- Applying Formal Methods to the Analysis of a Key Management ProtocolJournal of Computer Security, 1992
- A Proof Theory for General UnificationPublished by Springer Nature ,1991
- Unification in a combination of arbitrary disjoint equational theoriesJournal of Symbolic Computation, 1989
- Protocol failures in cryptosystemsProceedings of the IEEE, 1988
- The Interrogator: Protocol Secuity AnalysisIEEE Transactions on Software Engineering, 1987
- How to (Selectively) Broadcast A SecretPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1985
- The Interrogator A Tool for Cryptographic Protocol SecurityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1984
- A Software Protection SchemePublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982