The Interrogator model. 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 for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Li, Yongjian; Pang, Jun: An inductive approach to strand spaces (2013)
- Backes, Michael; Berg, Matthias; Unruh, Dominique: A formal language for cryptographic pseudocode (2008)
- Backes, Michael; Pfitzmann, Birgit: Limits of the BRSIM/UC soundness of Dolev-Yao-style XOR (2008) ioport
- Backes, Michael; Pfitzmann, Birgit; Waidner, Michael: The reactive simulatability (RSIM) framework for asynchronous systems (2007)
- Li, Xianxian; Huai, Jinpeng: Cryptographic protocol security analysis based on bounded constructing algorithm (2006)
- Backes, Michael: Unifying simulatability definitions in cryptographic systems under different timing assumptions (2005)
- Backes, Michael; Pfitzmann, Birgit; Waidner, Michael: Symmetric authentication in a simulatable Dolev --- Yao-style cryptographic library (2005) ioport
- Chen, Qingfeng; Zhang, Chengqi; Zhang, Shichao: ENDL: A logical framework for verifying secure transaction protocols (2005) ioport
- Zunino, Roberto; Degano, Pierpaolo: Weakening the perfect encryption assumption in Dolev-Yao adversaries (2005)
- Abadi, Martín; Gordon, Andrew D.: A calculus for cryptographic protocols: The spi calculus (1999)
- Low, Steven H.; Maxemchuk, Nicholas F.: A collusion problem and its solution (1998)