Maude-NPA

State space reduction in the Maude-NRL protocol analyzer. The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate completeness, so that failure to find attacks still guarantees security. In this paper we describe some state space reduction techniques that we have implemented in Maude-NPA. We also provide completeness proofs, and experimental evaluations of their effect on the performance of Maude-NPA.


References in zbMATH (referenced in 27 articles , 1 standard article )

Showing results 1 to 20 of 27.
Sorted by year (citations)

1 2 next

  1. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  2. Meseguer, José: Generalized rewrite theories, coherence completion, and symbolic methods (2020)
  3. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele; Rocha-Oliveira, Ana Cristina: A formalisation of nominal (\alpha)-equivalence with A, C, and AC function symbols (2019)
  4. Li, Di Long; Tiu, Alwen: Combining proverif and automated theorem provers for security protocol verification (2019)
  5. Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude (2018)
  6. Basin, David; Cremers, Cas; Meadows, Catherine: Model checking security protocols (2018)
  7. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal (\alpha)-equivalence with A and AC function symbols (2017)
  8. Ayala-Rincón, Mauricio; Fernández, Maribel; Nantes-Sobrinho, Daniele: Intruder deduction problem for locally stable theories with normal forms and inverses (2017)
  9. Baelde, David; Delaune, Stéphanie; Hirschi, Lucca: A reduced semantics for deciding trace equivalence (2017)
  10. Dreier, Jannik; Duménil, Charles; Kremer, Steve; Sasse, Ralf: Beyond subterm-convergent equational theories in automated verification of stateful protocols (2017)
  11. Chadha, Rohit; Cheval, Vincent; Ciobâcă, Ştefan; Kremer, Steve: Automated verification of equivalence properties of cryptographic protocols (2016)
  12. Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude (2015)
  13. Clavel, Manuel; Durán, Francisco; Eker, Steven; Escobar, Santiago; Lincoln, Patrick; Martí-Oliet, Narciso; Talcott, Carolyn: Two decades of Maude (2015)
  14. Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia: Symbolic protocol analysis with disequality constraints modulo equational theories (2015)
  15. Klein, Dominik: Key-secrecy of PACE with OTS/CafeOBJ (2015) ioport
  16. Martí-Oliet, Narciso; Ölveczky, Peter Csaba; Talcott, Carolyn: José Meseguer: scientist and friend extraordinaire (2015)
  17. Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia: State space reduction in the Maude-NRL protocol analyzer (2014)
  18. Liu, Zhiqiang; Lynch, Christopher: Efficient general AGH-unification (2014)
  19. Hendrix, Joe; Meseguer, José: Order-sorted equational unification revisited (2012)
  20. Meseguer, José: Twenty years of rewriting logic (2012)

1 2 next