Active Intruders with Caps

Siva Anatharaman (1) , Hai Lin , Chris Lynch , Paliath Narendran (2) , Michael Rusinowitch (3)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 University at Albany [SUNY]
3 CASSIS - Combination of approaches to the security of infinite states systems

We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. By modeling each protocol step as a rigid Horn clause, and the intruder abilities as an equational theory over a convergent rewrite system, the problem of active intrusion is formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: we look for a cap to be placed on a given set of terms, so that it unifies with a given term modulo the equational theory.

Domaines: Logique en informatique [cs.LO]

Siva Anatharaman, Hai Lin, Chris Lynch, Paliath Narendran, Michael Rusinowitch. Active Intruders with Caps. FCS-ARSPA-WITS'08, Jun 2008, Pittsburgh, United States. ⟨inria-00330532⟩