59bcb18fec
I've added a marked for the Athena problem case, and now no more false 'complete proof' results are produced. However, the tool reports, 'no attack within bounds', which is slightly inaccurate depending on the interpretatio of 'bounds'.
536 lines
12 KiB
C
536 lines
12 KiB
C
/*
|
|
* Scyther : An automatic verifier for security protocols.
|
|
* Copyright (C) 2007 Cas Cremers
|
|
*
|
|
* This program is free software; you can redistribute it and/or
|
|
* modify it under the terms of the GNU General Public License
|
|
* as published by the Free Software Foundation; either version 2
|
|
* of the License, or (at your option) any later version.
|
|
*
|
|
* This program is distributed in the hope that it will be useful,
|
|
* but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
* GNU General Public License for more details.
|
|
*
|
|
* You should have received a copy of the GNU General Public License
|
|
* along with this program; if not, write to the Free Software
|
|
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
|
|
*/
|
|
|
|
#include <stdlib.h>
|
|
#include <stdio.h>
|
|
#include "term.h"
|
|
#include "termlist.h"
|
|
#include "mgu.h"
|
|
#include "type.h"
|
|
#include "debug.h"
|
|
#include "specialterm.h"
|
|
#include "switches.h"
|
|
#include "arachne.h"
|
|
|
|
/*
|
|
Most General Unifier
|
|
|
|
Unification etc.
|
|
|
|
New version yields a termlist with substituted variables, which can later be reset to NULL.
|
|
*/
|
|
|
|
/**
|
|
* switches.match
|
|
* 0 typed
|
|
* 1 basic typeflaws
|
|
* 2 all typeflaws
|
|
*/
|
|
|
|
void
|
|
showSubst (Term t)
|
|
{
|
|
#ifdef DEBUG
|
|
if (!DEBUGL (5))
|
|
return;
|
|
|
|
indent ();
|
|
eprintf ("Substituting ");
|
|
termPrint (t);
|
|
eprintf (", typed ");
|
|
termlistPrint (t->stype);
|
|
if (realTermLeaf (t->subst))
|
|
{
|
|
eprintf ("->");
|
|
termlistPrint (t->subst->stype);
|
|
}
|
|
else
|
|
{
|
|
eprintf (", composite term");
|
|
}
|
|
if (t->type != VARIABLE)
|
|
{
|
|
eprintf (" (bound roleconstant)");
|
|
}
|
|
eprintf ("\n");
|
|
#endif
|
|
}
|
|
|
|
//! See if this is preferred substitution
|
|
/**
|
|
* By default, ta->tb will map. Returning 0 (false) will swap them.
|
|
*/
|
|
int
|
|
preferSubstitutionOrder (Term ta, Term tb)
|
|
{
|
|
if (termlistLength (ta->stype) == 1 && inTermlist (ta->stype, TERM_Agent))
|
|
{
|
|
/**
|
|
* If the first one is an agent type, we prefer swapping.
|
|
*/
|
|
return 0;
|
|
}
|
|
|
|
// Per default, leave it as it is.
|
|
return 1;
|
|
}
|
|
|
|
//! See if a substitution is valid
|
|
__inline__ int
|
|
goodsubst (Term tvar, Term tsubst)
|
|
{
|
|
Term tbuf;
|
|
int res;
|
|
|
|
tbuf = tvar->subst;
|
|
tvar->subst = tsubst;
|
|
|
|
res = checkTypeTerm (tvar);
|
|
|
|
tvar->subst = tbuf;
|
|
return res;
|
|
}
|
|
|
|
//! Undo all substitutions in a list of variables.
|
|
/**
|
|
* The termlist should contain only variables.
|
|
*/
|
|
void
|
|
termlistSubstReset (Termlist tl)
|
|
{
|
|
while (tl != NULL)
|
|
{
|
|
tl->term->subst = NULL;
|
|
tl = tl->next;
|
|
}
|
|
}
|
|
|
|
//! Most general unifier iteration
|
|
/**
|
|
* Try to determine the most general unifier of two terms, if so calls function.
|
|
*
|
|
* The callback receives a list of variables, that were previously open, but are now closed
|
|
* in such a way that the two terms unify.
|
|
*
|
|
* The callback must return true for the iteration to proceed: if it returns false, a single call would abort the scan.
|
|
* The return value shows this: it is false if the scan was aborted, and true if not.
|
|
*/
|
|
int
|
|
unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
|
|
{
|
|
int callsubst (Termlist tl, Term t, Term tsubst)
|
|
{
|
|
int proceed;
|
|
|
|
t->subst = tsubst;
|
|
#ifdef DEBUG
|
|
showSubst (t);
|
|
#endif
|
|
tl = termlistAdd (tl, t);
|
|
proceed = callback (tl);
|
|
tl = termlistDelTerm (tl);
|
|
t->subst = NULL;
|
|
return proceed;
|
|
}
|
|
|
|
/* added for speed */
|
|
t1 = deVar (t1);
|
|
t2 = deVar (t2);
|
|
if (t1 == t2)
|
|
{
|
|
return callback (tl);
|
|
}
|
|
|
|
if (!(hasTermVariable (t1) || hasTermVariable (t2)))
|
|
{
|
|
// None has a variable
|
|
if (isTermEqual (t1, t2))
|
|
{
|
|
// Equal!
|
|
return callback (tl);
|
|
}
|
|
else
|
|
{
|
|
// Can never be fixed, no variables
|
|
return true;
|
|
}
|
|
}
|
|
|
|
/*
|
|
* Distinguish a special case where both are unbound variables that will be
|
|
* connected, and I want to give one priority over the other for readability.
|
|
*
|
|
* Because t1 and t2 have been deVar'd means that if they are variables, they
|
|
* are also unbound.
|
|
*/
|
|
|
|
if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
|
|
{
|
|
/* Both are unbound variables. Decide.
|
|
*
|
|
* The plan: t1->subst will point to t2. But maybe we prefer the other
|
|
* way around?
|
|
*/
|
|
if (preferSubstitutionOrder (t2, t1))
|
|
{
|
|
Term t3;
|
|
|
|
// Swappy.
|
|
t3 = t1;
|
|
t1 = t2;
|
|
t2 = t3;
|
|
}
|
|
return callsubst (tl, t1, t2);
|
|
}
|
|
|
|
/* symmetrical tests for single variable.
|
|
*/
|
|
|
|
if (realTermVariable (t2))
|
|
{
|
|
if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
|
|
return true;
|
|
else
|
|
{
|
|
return callsubst (tl, t2, t1);
|
|
}
|
|
}
|
|
if (realTermVariable (t1))
|
|
{
|
|
if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
|
|
return true;
|
|
else
|
|
{
|
|
return callsubst (tl, t1, t2);
|
|
}
|
|
}
|
|
|
|
/* left & right are compounds with variables */
|
|
if (t1->type != t2->type)
|
|
return true;
|
|
|
|
/* identical compound types */
|
|
|
|
/* encryption first */
|
|
if (realTermEncrypt (t1))
|
|
{
|
|
int unify_combined_enc (Termlist tl)
|
|
{
|
|
// now the keys are unified (subst in this tl)
|
|
// and we try the inner terms
|
|
return unify (TermOp (t1), TermOp (t2), tl, callback);
|
|
}
|
|
|
|
return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
|
|
}
|
|
|
|
/* tupling second
|
|
non-associative version ! TODO other version */
|
|
if (isTermTuple (t1))
|
|
{
|
|
int unify_combined_tup (Termlist tl)
|
|
{
|
|
// now the keys are unified (subst in this tl)
|
|
// and we try the inner terms
|
|
return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
|
|
}
|
|
return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
|
|
}
|
|
|
|
return true;
|
|
}
|
|
|
|
|
|
//! Subterm unification
|
|
/**
|
|
* Try to unify (a subterm of) tbig with tsmall.
|
|
*
|
|
* Callback is called with a list of substitutions, and a list of terms that
|
|
* need to be decrypted in order for this to work.
|
|
*
|
|
* E.g. subtermUnify ( {{m}k1}k2, m ) yields a list : {{m}k1}k2, {m}k1 (where
|
|
* the {m}k1 is the last added node to the list)
|
|
*
|
|
* The callback should return true for the iteration to proceed, or false to abort.
|
|
* The final result is this flag.
|
|
*
|
|
* This is the actual procedure used by the Arachne algorithm in archne.c
|
|
*/
|
|
int
|
|
subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
|
|
int (*callback) (Termlist, Termlist))
|
|
{
|
|
int proceed;
|
|
|
|
int keycallback (Termlist tl)
|
|
{
|
|
return callback (tl, keylist);
|
|
}
|
|
|
|
proceed = true;
|
|
|
|
// Devar
|
|
tbig = deVar (tbig);
|
|
tsmall = deVar (tsmall);
|
|
|
|
// Three options:
|
|
// 1. simple unification
|
|
proceed = proceed && unify (tbig, tsmall, tl, keycallback);
|
|
|
|
// [2/3]: complex
|
|
if (switches.intruder)
|
|
{
|
|
// 2. interm unification
|
|
// Only if there is an intruder
|
|
if (realTermTuple (tbig))
|
|
{
|
|
proceed = proceed
|
|
&& subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback);
|
|
proceed = proceed
|
|
&& subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback);
|
|
}
|
|
|
|
// 3. unification with encryption needed
|
|
if (realTermEncrypt (tbig))
|
|
{
|
|
// extend the keylist
|
|
keylist = termlistAdd (keylist, tbig);
|
|
proceed = proceed
|
|
&& subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback);
|
|
// remove last item again
|
|
keylist = termlistDelTerm (keylist);
|
|
}
|
|
}
|
|
|
|
// Athena problem case: open variable about to be unified.
|
|
/**
|
|
* In this case we really need to consider the problematic Athena case for untyped variables.
|
|
*/
|
|
if (isTermVariable (tbig))
|
|
{
|
|
// Check the type: can it contain tuples, encryptions?
|
|
if (isOpenVariable (tbig))
|
|
{
|
|
// This one needs to be pursued by further constraint adding
|
|
/**
|
|
* Currently, this is not implemented yet. TODO.
|
|
* This is actually the main Athena problem that we haven't solved yet.
|
|
*/
|
|
// Mark that we don't have a full proof.
|
|
markNoFullProof ();
|
|
}
|
|
}
|
|
|
|
return proceed;
|
|
}
|
|
|
|
|
|
//! Most general unifier.
|
|
/**
|
|
* Try to determine the most general unifier of two terms.
|
|
* Resulting termlist must be termlistDelete'd.
|
|
*
|
|
*@return Returns a list of variables, that were previously open, but are now closed
|
|
* in such a way that the two terms unify. Returns \ref MGUFAIL if it is impossible.
|
|
* The termlist should be deleted.
|
|
*/
|
|
Termlist
|
|
termMguTerm (Term t1, Term t2)
|
|
{
|
|
/* added for speed */
|
|
t1 = deVar (t1);
|
|
t2 = deVar (t2);
|
|
if (t1 == t2)
|
|
return NULL;
|
|
|
|
if (!(hasTermVariable (t1) || hasTermVariable (t2)))
|
|
{
|
|
if (isTermEqual (t1, t2))
|
|
{
|
|
return NULL;
|
|
}
|
|
else
|
|
{
|
|
return MGUFAIL;
|
|
}
|
|
}
|
|
|
|
/*
|
|
* Distinguish a special case where both are unbound variables that will be
|
|
* connected, and I want to give one priority over the other for readability.
|
|
*
|
|
* Because t1 and t2 have been deVar'd means that if they are variables, they
|
|
* are also unbound.
|
|
*/
|
|
|
|
if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
|
|
{
|
|
/* Both are unbound variables. Decide.
|
|
*
|
|
* The plan: t1->subst will point to t2. But maybe we prefer the other
|
|
* way around?
|
|
*/
|
|
if (preferSubstitutionOrder (t2, t1))
|
|
{
|
|
Term t3;
|
|
|
|
// Swappy.
|
|
t3 = t1;
|
|
t1 = t2;
|
|
t2 = t3;
|
|
}
|
|
t1->subst = t2;
|
|
#ifdef DEBUG
|
|
showSubst (t1);
|
|
#endif
|
|
return termlistAdd (NULL, t1);
|
|
}
|
|
|
|
/* symmetrical tests for single variable.
|
|
*/
|
|
|
|
if (realTermVariable (t2))
|
|
{
|
|
if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
|
|
return MGUFAIL;
|
|
else
|
|
{
|
|
t2->subst = t1;
|
|
#ifdef DEBUG
|
|
showSubst (t2);
|
|
#endif
|
|
return termlistAdd (NULL, t2);
|
|
}
|
|
}
|
|
if (realTermVariable (t1))
|
|
{
|
|
if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
|
|
return MGUFAIL;
|
|
else
|
|
{
|
|
t1->subst = t2;
|
|
#ifdef DEBUG
|
|
showSubst (t1);
|
|
#endif
|
|
return termlistAdd (NULL, t1);
|
|
}
|
|
}
|
|
|
|
/* left & right are compounds with variables */
|
|
if (t1->type != t2->type)
|
|
return MGUFAIL;
|
|
|
|
/* identical compounds */
|
|
/* encryption first */
|
|
if (realTermEncrypt (t1))
|
|
{
|
|
Termlist tl1, tl2;
|
|
|
|
tl1 = termMguTerm (TermKey (t1), TermKey (t2));
|
|
if (tl1 == MGUFAIL)
|
|
{
|
|
return MGUFAIL;
|
|
}
|
|
else
|
|
{
|
|
tl2 = termMguTerm (TermOp (t1), TermOp (t2));
|
|
if (tl2 == MGUFAIL)
|
|
{
|
|
termlistSubstReset (tl1);
|
|
termlistDelete (tl1);
|
|
return MGUFAIL;
|
|
}
|
|
else
|
|
{
|
|
return termlistConcat (tl1, tl2);
|
|
}
|
|
}
|
|
}
|
|
|
|
/* tupling second
|
|
non-associative version ! TODO other version */
|
|
if (isTermTuple (t1))
|
|
{
|
|
Termlist tl1, tl2;
|
|
|
|
tl1 = termMguTerm (TermOp1 (t1), TermOp1 (t2));
|
|
if (tl1 == MGUFAIL)
|
|
{
|
|
return MGUFAIL;
|
|
}
|
|
else
|
|
{
|
|
tl2 = termMguTerm (TermOp2 (t1), TermOp2 (t2));
|
|
if (tl2 == MGUFAIL)
|
|
{
|
|
termlistSubstReset (tl1);
|
|
termlistDelete (tl1);
|
|
return MGUFAIL;
|
|
}
|
|
else
|
|
{
|
|
return termlistConcat (tl1, tl2);
|
|
}
|
|
}
|
|
}
|
|
return MGUFAIL;
|
|
}
|
|
|
|
//! Check if role terms might match in some way
|
|
/**
|
|
* Interesting case: role names are variables here, so they always match. We catch that case by inspecting the variable list.
|
|
*/
|
|
int
|
|
checkRoletermMatch (const Term t1, const Term t2, const Termlist notmapped)
|
|
{
|
|
Termlist tl;
|
|
|
|
// simple clause or combined
|
|
tl = termMguTerm (t1, t2);
|
|
if (tl == MGUFAIL)
|
|
{
|
|
return false;
|
|
}
|
|
else
|
|
{
|
|
int result;
|
|
Termlist vl;
|
|
|
|
result = true;
|
|
// Reset variables
|
|
termlistSubstReset (tl);
|
|
// Check variable list etc: should not contain mapped role names
|
|
vl = tl;
|
|
while (vl != NULL)
|
|
{
|
|
// This term should not be in the notmapped list
|
|
if (inTermlist (notmapped, vl->term))
|
|
{
|
|
result = false;
|
|
break;
|
|
}
|
|
vl = vl->next;
|
|
|
|
}
|
|
// Remove list
|
|
termlistDelete (tl);
|
|
return result;
|
|
}
|
|
}
|