NRL Protocol Analyzer

• Also in Prolog [Mea96a, Mea96b]

• State-transition rules of the form

  If:
  
  
  intruderknows()
  then:
  
  intruderlearns()
  EVENT:
  

• State transitions may be smaller (send only, compute only)

• Reduction rules for cryptographic operators

  • Pke(privkey(X), pke(pubkey(X), Y)) => Y
  • Narrowing procedure to solve equations with these operators

Previous slide

Next slide

Back to first slide

View graphic version