--- TEST of Assignment 2 in INF5130 --- Tested with Maude 2.6 together with --- full-maude 2.6, which can be found at the following link --- http://maude.cs.uiuc.edu/download/current/FM2.6/full-maude26.maude --- also tested with Maude 2.5 together with --- full-maude 2.5, which can be found at the following link --- http://maude.cs.uiuc.edu/versions/2.5/FM2.5/full-maude25.maude load full-maude --- Assignment 2: iterative bounded depth-first search. --- Requirements: --- 1. output the successul path as a sequence --- t0 => t1 => t2 => t3 => ... => tn of meta-terms IN ORDER! --- 2. should always terminate when there is no infinite path from the initial --- state --- 3. This should not impede significantly the efficiency of the algorithm --- during search ... --- 4. Must of course be able to have conditions on the pattern! --- HERE COMES YOUR SPECIFICATION OF ITERATIVE DEPTH-FIRST SEARCH! in itDepthFirst.fm --- EXAMPLE of testing. You should test MORE examples!!! --- --------------------------------------------------------- --- 1st case: nonterminating system: (mod TEST is sort S . ops f g h : S S -> S [ctor] . ops a b : -> S [ctor] . vars X Y : S . rl [l1] : f(X, Y) => g(X, f(Y, X)) . rl [l2] : a => b . rl [l3] : g(X, f(Y, X)) => X . endm) --- first, find a case where it should terminate in 0 steps: (fmod TEST-TEST is protecting META-LEVEL{TEST} . protecting ITERATIVE-BOUNDED-DEPTH-FIRST-SEARCH . endfm) (red itDepthFirstSearch(META-TEST, 'f['a.S, 'b.S], 'f['X:S, 'Y:S], nil) .) --- now, should reach b from f(a, a) in 4 steps: (red itDepthFirstSearch(META-TEST, 'f['a.S, 'a.S], 'b.S, nil) .) --- should of course never reach 'a from any b: --- red itDepthFirstSearch(META-TEST, 'f['b.S, 'b.S], 'a.S, nil) . --- Now, for a terminating system: (mod TEST-TERM is sort S . ops f g h : S S -> S [ctor] . ops a b : -> S [ctor] . vars X Y : S . rl [l1] : f(X, X) => g(X, g(X, X)) . rl [l2] : a => b . rl [l3] : g(X, f(Y, X)) => X . endm) (fmod TEST-TEST-TERM is protecting META-LEVEL{TEST-TERM} . protecting ITERATIVE-BOUNDED-DEPTH-FIRST-SEARCH . endfm) (red itDepthFirstSearch(META-TEST-TERM, 'f['a.S, 'a.S], 'a.S, nil) .) --- ----------------------------------------------------------------- --- ----------------------------------------------------------------- --- N S P K analysis --- ----------------------------------------------------------------- --- ----------------------------------------------------------------- --- read the file nspk.fm from the course website. --- This is exactly the same file as used in INF3230! in nspk.fm (fmod TEST-NSPK is protecting META-LEVEL{TEST-INTRUSION} . protecting ITERATIVE-BOUNDED-DEPTH-FIRST-SEARCH . endfm) --- This is the main test, which we want answered. Just like in INF3230! ***( (red itDepthFirstSearch(META-TEST-INTRUSION, upTerm(TEST-INTRUSION, intruderInit), upTerm(TEST-INTRUSION, C:Configuration < "Bank" : Responder | respSessions : trustedConnection("Peter") RS:RespSessions, ATTS:AttributeSet >), nil) .) )*** --- Other important tests: --- --------------------------------------------------------------- --- 1. The initial state is always reachable from intruderInit. --- This must of course be the case: ***( (red itDepthFirstSearch(META-TEST-INTRUSION, upTerm(TEST-INTRUSION, intruderInit), upTerm(TEST-INTRUSION, < "Peter" : Initiator | initSessions : notInitiated("Walker"), nonceCtr : 1 > < "Bank" : Responder | respSessions : emptySession, nonceCtr : 1 > < "Walker" : Intruder | initSessions : notInitiated("Bank"), respSessions : emptySession, nonceCtr : 1, agentsSeen : "Bank" ; "Walker", noncesSeen : emptyNonceSet, encrMsgsSeen : emptyEncrMsg >), nil) .) )*** --- 2. It may be the case that the main test does not succeed. --- One thing which should succeed is the approach taken in --- INF3230, to split the search in two parts. --- 2a. The first search goes from the initial state to a state in --- which the bank has a respSession with "Peter", even if "Peter" --- did not want to contact the bank. ***( (red itDepthFirstSearch(META-TEST-INTRUSION, upTerm(TEST-INTRUSION, intruderInit), upTerm(TEST-INTRUSION, C:Configuration < "Bank" : Responder | respSessions : responded("Peter", N:Nonce) RS:RespSessions, ATTS:AttributeSet >), nil) .) )*** --- This should be really quick! --- 2b. The second part of the search is from the previous state, found by --- the search command above, and to the undesirable state: ***( (red itDepthFirstSearch(META-TEST-INTRUSION, upTerm(TEST-INTRUSION, < "Walker" : Intruder | nonceCtr : 1, initSessions : notInitiated("Bank"), respSessions : emptySession, encrMsgsSeen : emptyEncrMsg, noncesSeen : nonce("Peter", 1), agentsSeen : ("Bank" ; "Peter" ; "Walker") > < "Peter" : Initiator | nonceCtr : 2, initSessions : initiated("Walker", nonce("Peter",1)) > (msg encrypt nonce("Peter",1); nonce("Bank",1) with pubKey("Peter") from "Bank" to "Peter") < "Bank" : Responder | respSessions : responded("Peter", nonce("Bank", 1)), nonceCtr : 2 >), upTerm(TEST-INTRUSION, C:Configuration < "Bank" : Responder | respSessions : trustedConnection("Peter") RS:RespSessions, ATTS:AttributeSet >), nil) .) )*** --- 3. We don't give up! Let's start from the state where both --- guys who wanted to start initiating a session have done --- so. Since we have asynchronous communication, this does --- in no way reduce the possibilities ... ***( (red itDepthFirstSearch(META-TEST-INTRUSION, upTerm(TEST-INTRUSION, < "Bank" : Responder | nonceCtr : 1, respSessions : emptySession > < "Peter" : Initiator | initSessions : initiated("Walker", nonce("Peter",1)), nonceCtr : 2 > < "Walker" : Intruder | agentsSeen : ("Bank" ; "Walker"), encrMsgsSeen : emptyEncrMsg, initSessions : initiated("Bank", nonce("Walker",1)), nonceCtr : 2, noncesSeen : nonce("Walker",1), respSessions : emptySession > (msg encrypt nonce("Walker",1); "Walker" with pubKey("Bank") from "Walker" to "Bank") (msg encrypt nonce("Peter",1); "Peter" with pubKey("Walker") from "Peter" to "Walker")), upTerm(TEST-INTRUSION, C:Configuration < "Bank" : Responder | respSessions : trustedConnection("Peter") RS:RespSessions, ATTS:AttributeSet >), nil) .) )***