From 76586442959fb076d0a6e9c56bba0b0cc315b1f3 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Fri, 26 Apr 2013 11:36:41 +0200 Subject: [PATCH] Rati Gelashvili reported a rare but annoying bug in the hash function handling. The fix requires a significant reworking of the function handling. This is a first attempt. Conflicts: src/knowledge.c src/knowledge.h Regression test suggests that the Hashfunction fix works. --- src/arachne.c | 2 +- src/compiler.c | 16 +- src/dotout.c | 6 +- src/knowledge.c | 192 ++++++++---------- src/knowledge.h | 16 +- src/main.c | 3 - src/parser.y | 9 +- ...ISO-9798-sasl.spdl --timer=60 --plain.time | 2 - ...tocols-andrew.spdl --timer=60 --plain.time | 2 +- ...chroeder-lowe.spdl --timer=60 --plain.time | 2 +- ...ham-schroeder.spdl --timer=60 --plain.time | 2 +- ...s-splice-as-hc.spdl --timer=60 --plain.out | 12 +- ...-splice-as-hc.spdl --timer=60 --plain.time | 2 +- ...cols-splice-as.spdl --timer=60 --plain.out | 12 +- ...ols-splice-as.spdl --timer=60 --plain.time | 2 +- ...ocols-woo-lam.spdl --timer=60 --plain.time | 2 +- ...lson-modified.spdl --timer=60 --plain.time | 2 - src/role.c | 2 +- src/scanner.l | 1 + src/specialterm.c | 2 +- src/system.c | 2 +- src/tac.h | 2 + src/term.c | 68 +++++-- src/term.h | 7 +- src/termlist.c | 63 +----- src/termlist.h | 1 - src/xmlout.c | 19 +- 27 files changed, 225 insertions(+), 226 deletions(-) delete mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time delete mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time diff --git a/src/arachne.c b/src/arachne.c index 35d0bcc..d6bca88 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -787,7 +787,7 @@ createDecryptionChain (const Binding b, const int run, const int index, indentDepth++; tdecr = keylist->term; - tkey = inverseKey (sys->know->inverses, TermKey (tdecr)); + tkey = inverseKey (sys->know, TermKey (tdecr)); smallrun = create_decryptor (tdecr, tkey); { Roledef rddecrypt; diff --git a/src/compiler.c b/src/compiler.c index cd8a726..d6c2a4c 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1101,7 +1101,7 @@ hashfunctions (Tac tcstart) error ("Bug in hashfunction generation code. Please contact the authors.\n"); } - knowledgeAddInverse (sys->know, hfuncs->term, hinvs->term); + knowledgeAddInverseKeys (sys->know, hfuncs->term, hinvs->term); hfuncs->term->stype = termlistAdd (NULL, TERM_Function); hinvs->term->stype = termlistAdd (NULL, TERM_Function); hfuncs = hfuncs->next; @@ -1157,8 +1157,12 @@ normalDeclaration (Tac tc) knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac)); break; case TAC_INVERSEKEYS: - knowledgeAddInverse (sys->know, tacTerm (tc->t1.tac), - tacTerm (tc->t2.tac)); + knowledgeAddInverseKeys (sys->know, tacTerm (tc->t1.tac), + tacTerm (tc->t2.tac)); + break; + case TAC_INVERSEKEYFUNCTIONS: + knowledgeAddInverseKeyFunctions (sys->know, tacTerm (tc->t1.tac), + tacTerm (tc->t2.tac)); break; case TAC_HASHFUNCTION: hashfunctions (tc); @@ -1568,8 +1572,14 @@ tacProcess (Tac tc) Term tacTerm (Tac tc) { + Term t; + switch (tc->op) { + case TAC_FCALL: + t = makeTermEncrypt (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac)); + t->helper.fcall = true; + return t; case TAC_ENCRYPT: return makeTermEncrypt (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac)); case TAC_TUPLE: diff --git a/src/dotout.c b/src/dotout.c index 555680c..e380fab 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -96,7 +96,7 @@ isIntruderChoice (const Term t) { // Chosen by intruder // However, if it is a rolename, this is not really what we mean - if (!(t->roleVar || isAgentType (t->stype))) + if (!(t->helper.roleVar || isAgentType (t->stype))) { // Not a role variable, and chosen by the intruder: that's it return true; @@ -187,12 +187,12 @@ explainVariable (Term t) if (realTermVariable (t)) { eprintf ("any "); - if (t->roleVar) + if (t->helper.roleVar) { eprintf ("agent "); } termPrintRemap (t); - if (!t->roleVar) + if (!t->helper.roleVar) { if (switches.match == 0 && t->stype != NULL) { diff --git a/src/knowledge.c b/src/knowledge.c index 2c2202a..51a0adb 100644 --- a/src/knowledge.c +++ b/src/knowledge.c @@ -30,19 +30,10 @@ #include "system.h" #include "debug.h" #include "error.h" +#include "specialterm.h" /* * Knowledge stuff - * - * Note that a really weird thing is going on involving unpropagated substitutions. - * Idea: - * - * 1. Substitute terms by filling in ->subst. - * Now, either: - * 2a. Undo this by knowledgeUndo. - * 2b. Propagate it, modifying the knowledge beyond repair by knowledgeSubstDo. Now inKnowledge works again. - * 2c. inKnowledge/knowledgeSet if something is in the knowledge: this does not consider the substitutions!, and - * they now have some overhead. */ //! Open knowledge code. @@ -81,7 +72,8 @@ emptyKnowledge () know = makeKnowledge (); know->basic = NULL; know->encrypt = NULL; - know->inverses = NULL; + know->inversekeys = NULL; + know->inversekeyfunctions = NULL; know->vars = NULL; know->publicfunctions = NULL; return know; @@ -110,7 +102,8 @@ knowledgeDuplicate (Knowledge know) newknow->basic = termlistShallow (know->basic); newknow->encrypt = termlistShallow (know->encrypt); newknow->vars = termlistShallow (know->vars); - newknow->inverses = know->inverses; + newknow->inversekeys = know->inversekeys; + newknow->inversekeyfunctions = know->inversekeyfunctions; newknow->publicfunctions = termlistShallow (know->publicfunctions); return newknow; } @@ -147,7 +140,8 @@ knowledgeDestroy (Knowledge know) termlistDestroy (know->basic); termlistDestroy (know->encrypt); termlistDestroy (know->vars); - // termlistDestroy(know->inverses); + // termlistDestroy(know->inversekeys); + // termlistDestroy(know->inversekeyfunctions); termlistDestroy (know->publicfunctions); free (know); } @@ -195,7 +189,7 @@ knowledgeAddTerm (Knowledge know, Term term) } if (term->type == ENCRYPT) { - Term invkey = inverseKey (know->inverses, TermKey (term)); + Term invkey = inverseKey (know, TermKey (term)); if (inKnowledge (know, invkey)) { /* we can decrypt it */ @@ -227,7 +221,7 @@ knowledgeSimplify (Knowledge know, Term key) { Termlist tldecrypts = NULL; Termlist scan = know->encrypt; - Term invkey = inverseKey (know->inverses, key); + Term invkey = inverseKey (know, key); while (scan != NULL) { @@ -257,6 +251,7 @@ knowledgeAddTermlist (Knowledge know, Termlist tl) while (tl != NULL) { + // Evil old fashioned code relies on lazy left-to-right parsing. Get rid of it. flag = knowledgeAddTerm (know, tl->term) || flag; tl = tl->next; } @@ -265,21 +260,18 @@ knowledgeAddTermlist (Knowledge know, Termlist tl) //! Add an inverse pair to the knowledge void -knowledgeAddInverse (Knowledge know, Term t1, Term t2) +knowledgeAddInverseKeys (Knowledge know, Term t1, Term t2) { - know->inverses = termlistAdd (know->inverses, t1); - know->inverses = termlistAdd (know->inverses, t2); - return; + know->inversekeys = termlistAdd (know->inversekeys, t1); + know->inversekeys = termlistAdd (know->inversekeys, t2); } -//! Set an inverse pair list for the knowledge. -/** - * List pointer is simply copied, so don't delete it later! - */ +//! Add an inverse pair to the knowledge void -knowledgeSetInverses (Knowledge know, Termlist tl) +knowledgeAddInverseKeyFunctions (Knowledge know, Term t1, Term t2) { - know->inverses = tl; + know->inversekeyfunctions = termlistAdd (know->inversekeyfunctions, t1); + know->inversekeyfunctions = termlistAdd (know->inversekeyfunctions, t2); } //! Is a term a part of the knowledge? @@ -341,6 +333,15 @@ knowledgePrint (Knowledge know) eprintf (" [Vars]: "); termlistPrint (know->vars); eprintf ("\n"); + eprintf (" [Inversekeys]: "); + termlistPrint (know->inversekeys); + eprintf ("\n"); + eprintf (" [Inversekeyfunctions]: "); + termlistPrint (know->inversekeyfunctions); + eprintf ("\n"); + eprintf (" [Publicfunctions]: "); + termlistPrint (know->publicfunctions); + eprintf ("\n"); } //! Print a knowledge set, short version (no newline) @@ -368,43 +369,6 @@ knowledgePrintShort (const Knowledge know) } } -//! Print the inverses list of a knowledge set. -void -knowledgeInversesPrint (Knowledge know) -{ - Termlist tl; - int after = 0; - - if (know == NULL) - { - eprintf ("Empty knowledge."); - return; - } - - tl = knowledgeGetInverses (know); - if (tl == NULL) - { - eprintf ("None."); - } - else - { - while (tl != NULL && tl->next != NULL) - { - if (after) - { - eprintf (","); - } - eprintf ("("); - termPrint (tl->term); - eprintf (","); - termPrint (tl->next->term); - eprintf (")"); - after = 1; - tl = tl->next->next; - } - } -} - //! Yield the set of representatives for the knowledge. /** * Note: this is a shallow copy, and needs to be termlistDelete'd. @@ -420,17 +384,11 @@ knowledgeSet (const Knowledge know) return termlistConcat (tl1, tl2); } -//! Get the inverses pointer of the knowledge. -/** - * Essentially the inverse function of knowledgeSetInverses() - */ -Termlist -knowledgeGetInverses (const Knowledge know) +//! Check for elements in the knowledge set +int +inKnowledgeSet (const Knowledge know, Term t) { - if (know == NULL) - return NULL; - else - return know->inverses; + return (inTermlist (know->basic, t) || inTermlist (know->encrypt, t)); } //! check whether any substitutions where made in a knowledge set. @@ -457,37 +415,6 @@ knowledgeSubstNeeded (const Knowledge know) return 0; } -//! Reconstruct a knowledge set. -/** - * This is useful after e.g. substitutions. - * Just rebuilds the knowledge in a new (shallow) copy. - *@return The pointer to the new knowledge. - *\sa knowledgeSubstNeeded() - */ -Knowledge -knowledgeReconstruction (const Knowledge know) -{ - Knowledge newknow = emptyKnowledge (); - - newknow->inverses = know->inverses; - knowledgeAddTermlist (newknow, know->basic); - knowledgeAddTermlist (newknow, know->encrypt); - return newknow; -} - -//! Propagate any substitutions just made. -/** - * This usually involves reconstruction of the complete knowledge, which is - * 'cheaper' than a thorough analysis, so we always make a copy. - *\sa knowledgeReconstruction() - */ -Knowledge -knowledgeSubstDo (const Knowledge know) -{ - /* otherwise a copy (for deletion) is returned. */ - return knowledgeReconstruction (know); -} - //! Add public function void knowledgeAddPublicFunction (const Knowledge know, const Term f) @@ -502,3 +429,62 @@ isKnowledgePublicFunction (const Knowledge know, const Term f) { return inTermlist (know->publicfunctions, f); } + +//! Give the inverse key term of a term. +/** + * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined + * by the termlist, which is a list of key1,key1inv, key2, key2inv, etc... + *@param inverses The list of inverses, typically from the knowledge. + *@param key Any term of which the inverse will be determined. + *@return A pointer to a duplicate of the inverse key term. Use termDelete to remove it. + *\sa termDuplicate(), knowledge::inverses + */ +Term +inverseKey (Knowledge know, Term key) +{ + Term f; + + key = deVar (key); + + /* inverse key function? */ + f = getTermFunction (key); + if (f != NULL) + { + Termlist tl; + + Term funKey (Term orig, Term f) + { + /* in: f'{op}, f + * out: f{op'} */ + return makeTermFcall (termDuplicate (TermOp (orig)), + termDuplicate (f)); + } + + tl = know->inversekeyfunctions; + while (tl != NULL && tl->next != NULL) + { + if (isTermEqual (TermKey (key), tl->term)) + return funKey (key, tl->next->term); + if (isTermEqual (TermKey (key), tl->next->term)) + return funKey (key, tl->term); + tl = tl->next->next; + } + } + else + { + /* scanning for a direct inverse */ + Termlist tl; + + /* scan the list */ + tl = know->inversekeys; + while (tl != NULL && tl->next != NULL) + { + if (isTermEqual (key, tl->term)) + return termDuplicate (tl->next->term); + if (isTermEqual (key, tl->next->term)) + return termDuplicate (tl->term); + tl = tl->next->next; + } + } + return termDuplicate (key); /* defaults to symmetrical */ +} diff --git a/src/knowledge.h b/src/knowledge.h index 18d15d1..d9fa009 100644 --- a/src/knowledge.h +++ b/src/knowledge.h @@ -33,8 +33,10 @@ struct knowledge Termlist basic; //! A list of terms encrypted, such that the inverse is not in the knowledge set. Termlist encrypt; - //! List of inverse pairs (thus length of list is even) - Termlist inverses; + //! List of inverse pairs (thus length of list is even) (add,sub) + Termlist inversekeys; + //! List of inverse pairs (thus length of list is even) (pk,sk) + Termlist inversekeyfunctions; //! List of open variables in the knowledge set. /** * This list is used to determine whether the knowledge needs to be rewritten. @@ -42,7 +44,7 @@ struct knowledge * and we need to reconstruct the knowledge set. */ Termlist vars; // special: denotes unsubstituted variables - //! A list of public functions + //! A list of hash functions Termlist publicfunctions; }; @@ -58,19 +60,19 @@ void knowledgeDelete (Knowledge know); void knowledgeDestroy (Knowledge know); int knowledgeAddTerm (Knowledge know, Term term); int knowledgeAddTermlist (Knowledge know, Termlist tl); -void knowledgeAddInverse (Knowledge know, Term t1, Term t2); -void knowledgeSetInverses (Knowledge know, Termlist tl); +void knowledgeAddInverseKeys (Knowledge know, Term t1, Term t2); +void knowledgeAddInverseKeyFunctions (Knowledge know, Term t1, Term t2); +int inKnowledgeSet (const Knowledge know, Term t); void knowledgeSimplify (Knowledge know, Term decryptkey); int inKnowledge (const Knowledge know, Term term); void knowledgePrint (Knowledge know); void knowledgePrintShort (const Knowledge know); -void knowledgeInversesPrint (Knowledge know); Termlist knowledgeSet (const Knowledge know); -Termlist knowledgeGetInverses (const Knowledge know); int knowledgeSubstNeeded (const Knowledge know); Knowledge knowledgeSubstDo (const Knowledge know); void knowledgeAddPublicFunction (const Knowledge know, const Term f); int isKnowledgePublicFunction (const Knowledge know, const Term f); +Term inverseKey (Knowledge know, Term key); //! Harnass macro for recursive procedures. #define mindwipe(k,recurse) \ diff --git a/src/main.c b/src/main.c index 8efbdd5..94b48f9 100644 --- a/src/main.c +++ b/src/main.c @@ -149,9 +149,6 @@ main (int argc, char **argv) termlistPrint (sys->untrusted); printf ("\n"); knowledgePrint (sys->know); - printf ("inverses: "); - knowledgeInversesPrint (sys->know); - printf ("\n"); locVarPrint (sys->locals); protocolsPrint (sys->protocols); diff --git a/src/parser.y b/src/parser.y index ad01666..4d8c01d 100644 --- a/src/parser.y +++ b/src/parser.y @@ -82,6 +82,7 @@ List findMacroDefinition(Symbol s) %token SECRET %token COMPROMISED %token INVERSEKEYS +%token INVERSEKEYFUNCTIONS %token UNTRUSTED %token USERTYPE %token SINGULAR @@ -356,6 +357,12 @@ declaration : secretpref CONST basictermlist typeinfo1 ';' t->t2.tac = $5; $$ = t; } + | INVERSEKEYFUNCTIONS '(' term ',' term ')' ';' + { Tac t = tacCreate(TAC_INVERSEKEYFUNCTIONS); + t->t1.tac = $3; + t->t2.tac = $5; + $$ = t; + } | COMPROMISED termlist ';' { Tac t = tacCreate(TAC_COMPROMISED); t->t1.tac= $2; @@ -456,7 +463,7 @@ term : ID '(' termlist ')' { Tac t = tacCreate(TAC_STRING); t->t1.sym = $1; - $$ = tacJoin(TAC_ENCRYPT,tacTuple($3),t,NULL); + $$ = tacJoin(TAC_FCALL,tacTuple($3),t,NULL); } | '{' termlist '}' key { diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time deleted file mode 100644 index 80f32ca..0000000 --- a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time +++ /dev/null @@ -1,2 +0,0 @@ -Passed wall time in seconds: -0 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time index 97d01d7..afe3b53 100644 --- a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -14 +15 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time index 37da462..0541820 100644 --- a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -23 +24 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time index 27fb100..d1a00da 100644 --- a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -28 +29 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out index cdd6305..20b5520 100644 --- a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out +++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out @@ -1,6 +1,6 @@ -claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds] time=60 -claim spliceAS-HC,I Niagree_9 - Ok [does not occur] time=60 -claim spliceAS-HC,I Nisynch_10 - Ok [does not occur] time=60 -claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds] time=60 -claim spliceAS-HC,R Niagree_11 - Ok [does not occur] time=60 -claim spliceAS-HC,R Nisynch_12 - Ok [does not occur] time=60 +claim spliceAS-HC,I Secret_7 N2 Fail [at least 7 attacks] +claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack] +claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack] +claim spliceAS-HC,R Secret_8 N2 Fail [at least 7 attacks] +claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack] +claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time index df21598..2eb5ce9 100644 --- a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -60 +6 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out index a8474fb..a91f153 100644 --- a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out +++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out @@ -1,6 +1,6 @@ -claim spliceAS,I Secret_7 N2 Ok [no attack within bounds] time=60 -claim spliceAS,I Niagree_9 - Ok [does not occur] time=60 -claim spliceAS,I Nisynch_10 - Ok [does not occur] time=60 -claim spliceAS,R Secret_8 N2 Ok [no attack within bounds] time=60 -claim spliceAS,R Niagree_11 - Ok [does not occur] time=60 -claim spliceAS,R Nisynch_12 - Ok [does not occur] time=60 +claim spliceAS,I Secret_7 N2 Fail [at least 7 attacks] +claim spliceAS,I Niagree_9 - Fail [at least 1 attack] +claim spliceAS,I Nisynch_10 - Fail [at least 1 attack] +claim spliceAS,R Secret_8 N2 Fail [at least 7 attacks] +claim spliceAS,R Niagree_11 - Fail [at least 1 attack] +claim spliceAS,R Nisynch_12 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time index df21598..2eb5ce9 100644 --- a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -60 +6 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time index b449a72..7ec870e 100644 --- a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time @@ -1,2 +1,2 @@ Passed wall time in seconds: -36 +37 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time deleted file mode 100644 index 80f32ca..0000000 --- a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time +++ /dev/null @@ -1,2 +0,0 @@ -Passed wall time in seconds: -0 diff --git a/src/role.c b/src/role.c index 139fa5f..70d4413 100644 --- a/src/role.c +++ b/src/role.c @@ -415,7 +415,7 @@ Readable (Knowledge know, Term t) return true; } // Right disjunct - inv = inverseKey (know->inverses, TermKey (t)); + inv = inverseKey (know, TermKey (t)); either = false; if (inKnowledge (know, inv)) { diff --git a/src/scanner.l b/src/scanner.l index 7fd1570..df6152f 100644 --- a/src/scanner.l +++ b/src/scanner.l @@ -171,6 +171,7 @@ claim { return CLAIMT; } run { return RUN; } secret { return SECRET; } inversekeys { return INVERSEKEYS; } +inversekeyfunctions { return INVERSEKEYFUNCTIONS; } untrusted { return UNTRUSTED; } compromised { return COMPROMISED; } usertype { return USERTYPE; } diff --git a/src/specialterm.c b/src/specialterm.c index 774ae87..aa67649 100644 --- a/src/specialterm.c +++ b/src/specialterm.c @@ -119,7 +119,7 @@ specialTermInit (const System sys) langcons (TERM_PK, "pk", TERM_Function); langcons (TERM_SK, "sk", TERM_Function); langcons (TERM_K, "k", TERM_Function); - knowledgeAddInverse (sys->know, TERM_PK, TERM_SK); + knowledgeAddInverseKeyFunctions (sys->know, TERM_PK, TERM_SK); knowledgeAddTerm (sys->know, TERM_PK); /* Define a prefix for labels for the match function */ diff --git a/src/system.c b/src/system.c index f7fa2ad..9ea0a88 100644 --- a/src/system.c +++ b/src/system.c @@ -504,7 +504,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, newt = makeTermType (GLOBAL, TermSymb (oldt), rid); } newt->stype = oldt->stype; // copy list of types - newt->roleVar = isrole; // set role status + newt->helper.roleVar = isrole; // set role status // Add to copy list TERMLISTADD (fromlist, oldt); diff --git a/src/tac.h b/src/tac.h index 0cbbaa0..2d303d1 100644 --- a/src/tac.h +++ b/src/tac.h @@ -32,6 +32,7 @@ enum tactypes TAC_SYM, TAC_TUPLE, TAC_ENCRYPT, + TAC_FCALL, TAC_VAR, TAC_CONST, TAC_FRESH, @@ -48,6 +49,7 @@ enum tactypes TAC_ROLEREF, TAC_SECRET, TAC_INVERSEKEYS, + TAC_INVERSEKEYFUNCTIONS, TAC_HASHFUNCTION, TAC_UNTRUSTED, TAC_COMPROMISED, diff --git a/src/term.c b/src/term.c index 6fb42bb..f9517b6 100644 --- a/src/term.c +++ b/src/term.c @@ -84,6 +84,9 @@ makeTerm () //! Create a fresh encrypted term from two existing terms. /** + * The first argument is the message, + * the second argument is the key. + * *@return A pointer to the new term. */ Term @@ -92,11 +95,32 @@ makeTermEncrypt (Term t1, Term t2) Term term = makeTerm (); term->type = ENCRYPT; term->stype = NULL; + term->helper.fcall = false; + term->subst = NULL; TermOp (term) = t1; TermKey (term) = t2; return term; } +Term +makeTermFcall (Term t1, Term t2) +//! Create a fresh function application term from two existing terms. +/** + * The first argument is the function argument, + * the second argument is the function (name). + * + * These behave like encryptions in most cases. + * + *@return A pointer to the new term. + */ +{ + Term t; + + t = makeTermEncrypt (t1, t2); + t->helper.fcall = true; + return t; +} + //! Create a fresh term tuple from two existing terms. /** *@return A pointer to the new term. @@ -128,7 +152,8 @@ makeTermTuple (Term t1, Term t2) tt = makeTerm (); tt->type = TUPLE; tt->stype = NULL; - tt->roleVar = 0; + tt->helper.roleVar = 0; + tt->subst = NULL; TermOp1 (tt) = t1; TermOp2 (tt) = t2; return tt; @@ -145,7 +170,16 @@ makeTermType (const int type, const Symbol symb, const int runid) Term term = makeTerm (); term->type = type; term->stype = NULL; - term->roleVar = 0; + if ((type == ENCRYPT) || (type == TUPLE)) + { + // Non-leaf + term->helper.fcall = false; + } + else + { + // Leaf + term->helper.roleVar = 0; + } term->subst = NULL; TermSymb (term) = symb; TermRunid (term) = runid; @@ -381,8 +415,7 @@ termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup, } if (realTermEncrypt (term)) { - if (isTermLeaf (TermKey (term)) - && inTermlist (TermKey (term)->stype, TERM_Function)) + if (term->helper.fcall) { /* function application */ termPrintCustom (TermKey (term), leftvar, rightvar, lefttup, @@ -695,8 +728,12 @@ termRunid (Term term, int runid) /* anything else, recurse */ if (realTermEncrypt (term)) { - return makeTermEncrypt (termRunid (TermOp (term), runid), - termRunid (TermKey (term), runid)); + Term t; + + t = makeTermEncrypt (termRunid (TermOp (term), runid), + termRunid (TermKey (term), runid)); + t->helper.fcall = term->helper.fcall; + return t; } else { @@ -1159,22 +1196,23 @@ term_encryption_level (const Term term) } else { + int l, r; + if (realTermTuple (t)) { - int l, r; - l = iter_maxencrypt (TermOp1 (t)); r = iter_maxencrypt (TermOp2 (t)); - if (l > r) - return l; - else - return r; } else { // encrypt - return 1 + iter_maxencrypt (TermOp (t)); + l = 1 + iter_maxencrypt (TermOp (t)); + r = iter_maxencrypt (TermKey (t)); } + if (l > r) + return l; + else + return r; } } @@ -1418,9 +1456,9 @@ Term getTermFunction (Term t) { t = deVar (t); - if (t != NULL) + if (realTermEncrypt (t)) { - if (realTermEncrypt (t) && isTermFunctionName (TermKey (t))) + if (t->helper.fcall) { return TermKey (t); } diff --git a/src/term.h b/src/term.h index fa65a72..c919f2b 100644 --- a/src/term.h +++ b/src/term.h @@ -47,7 +47,11 @@ struct term //! Data Type termlist (e.g. agent or nonce) /** Only for leaves. */ void *stype; // list of types - int roleVar; //!< only for leaf, arachne engine: role variable flag + union + { + int roleVar; //!< only for leaf, arachne engine: role variable flag + int fcall; //!< only for 'encryption' to mark actual function call f(t) + } helper; //! Substitution term. /** @@ -96,6 +100,7 @@ typedef struct term *Term; void termsInit (void); void termsDone (void); Term makeTermEncrypt (Term t1, Term t2); +Term makeTermFcall (Term t1, Term t2); Term makeTermTuple (Term t1, Term t2); Term makeTermType (const int type, const Symbol symb, const int runid); __inline__ Term deVarScan (Term t); diff --git a/src/termlist.c b/src/termlist.c index 7366eb1..7d25fdc 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -24,6 +24,7 @@ #include "debug.h" #include "error.h" #include "switches.h" +#include "knowledge.h" /* * Shared stuff @@ -618,68 +619,6 @@ termlistLength (Termlist tl) return i; } -//! Give the inverse key term of a term. -/** - * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined - * by the termlist, which is a list of key1,key1inv, key2, key2inv, etc... - *@param inverses The list of inverses, typically from the knowledge. - *@param key Any term of which the inverse will be determined. - *@return A pointer to a duplicate of the inverse key term. Use termDelete to remove it. - *\sa termDuplicate(), knowledge::inverses - */ - -Term -inverseKey (Termlist inverses, Term key) -{ - key = deVar (key); - - /* is this a function application? i.e. hash? */ - if (isTermLeaf (key) && inTermlist (key->stype, TERM_Function)) - { - /* functions cannot be inverted by default */ - return termDuplicate (TERM_Hidden); - } - /* check for the special case first: when it is effectively a function application */ - if (isTermEncrypt (key) && isTermLeaf (TermKey (key)) - && inTermlist (deVar (TermKey (key))->stype, TERM_Function)) - { - /* we are scanning for functions */ - /* scan the list */ - /* key is function application kk(op), or {op}kk */ - Term funKey (Term orig, Term newk) - { - /* in: {op}kk, nk - * out: {op'}nk */ - return makeTermEncrypt (termDuplicate (TermOp (orig)), - termDuplicate (newk)); - } - while (inverses != NULL && inverses->next != NULL) - { - - if (isTermEqual (TermKey (key), inverses->term)) - return funKey (key, inverses->next->term); - if (isTermEqual (TermKey (key), inverses->next->term)) - return funKey (key, inverses->term); - inverses = inverses->next->next; - } - } - else - { - /* scanning for a direct inverse */ - - /* scan the list */ - while (inverses != NULL && inverses->next != NULL) - { - if (isTermEqual (key, inverses->term)) - return termDuplicate (inverses->next->term); - if (isTermEqual (key, inverses->next->term)) - return termDuplicate (inverses->term); - inverses = inverses->next->next; - } - } - return termDuplicate (key); /* defaults to symmetrical */ -} - //! Create a term local to a run. /* * We assume that at this point, no variables have been instantiated yet that occur in this term. diff --git a/src/termlist.h b/src/termlist.h index 475e3c9..81189f7 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -66,7 +66,6 @@ Termlist termlistAddBasic (Termlist tl, Term t); Termlist termlistAddBasics (Termlist tl, Termlist scan); Termlist termlistMinusTerm (Termlist tl, Term t); int termlistLength (Termlist tl); -Term inverseKey (Termlist inverses, Term key); Term termLocal (const Term t, Termlist fromlist, Termlist tolist); Termlist termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist); diff --git a/src/xmlout.c b/src/xmlout.c index 83ab337..5e541f0 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -438,7 +438,7 @@ xmlInverses (const System sys) xmlPrint (""); xmlindent++; - invlist = sys->know->inverses; + invlist = sys->know->inversekeys; while (invlist != NULL && invlist->next != NULL) { xmlPrint (""); @@ -452,6 +452,23 @@ xmlInverses (const System sys) } xmlindent--; xmlPrint (""); + + xmlPrint (""); + xmlindent++; + invlist = sys->know->inversekeyfunctions; + while (invlist != NULL && invlist->next != NULL) + { + xmlPrint (""); + xmlindent++; + xmlOutTerm (NULL, invlist->term); + xmlOutTerm (NULL, invlist->next->term); + xmlindent--; + xmlPrint (""); + + invlist = invlist->next->next; + } + xmlindent--; + xmlPrint (""); } //! Show initial knowledge