/****************************** Program "mobike.m" compiled by "Murphi Release 3.1" Murphi Last Modefied Date: "Jan 29 1999" Murphi Last Compiled date: "Jan 8 2004" ******************************/ /******************** Parameter ********************/ #define MURPHI_VERSION "Murphi Release 3.1" #define MURPHI_DATE "Jan 29 1999" #define PROTOCOL_NAME "mobike" #define BITS_IN_WORLD 9567 /******************** Include ********************/ #include "mu_prolog.inc" /******************** Decl declaration ********************/ class mu_1_InitiatorId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_InitiatorId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_InitiatorId& val) { if (val.defined()) return ( s << mu_1_InitiatorId::values[ int(val) - 1 ] ); else return ( s << "Undefined" ); }; mu_1_InitiatorId (char *name, int os): mu__byte(1, 1, 1, name, os) {}; mu_1_InitiatorId (void): mu__byte(1, 1, 1) {}; mu_1_InitiatorId (int val): mu__byte(1, 1, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -1]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 1] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_InitiatorId& a, mu_1_InitiatorId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_InitiatorId::values[] = { "InitiatorId_1",NULL }; /*** end scalarset declaration ***/ mu_1_InitiatorId mu_1_InitiatorId_undefined_var; class mu_1_InitiatorIdP: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_InitiatorIdP& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_InitiatorIdP& val) { if (val.defined()) return ( s << mu_1_InitiatorIdP::values[ int(val) - 2 ] ); else return ( s << "Undefined" ); }; mu_1_InitiatorIdP (char *name, int os): mu__byte(2, 2, 1, name, os) {}; mu_1_InitiatorIdP (void): mu__byte(2, 2, 1) {}; mu_1_InitiatorIdP (int val): mu__byte(2, 2, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -2]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 2] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_InitiatorIdP& a, mu_1_InitiatorIdP& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_InitiatorIdP::values[] = { "InitiatorIdP_1",NULL }; /*** end scalarset declaration ***/ mu_1_InitiatorIdP mu_1_InitiatorIdP_undefined_var; class mu_1_ResponderId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_ResponderId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_ResponderId& val) { if (val.defined()) return ( s << mu_1_ResponderId::values[ int(val) - 3 ] ); else return ( s << "Undefined" ); }; mu_1_ResponderId (char *name, int os): mu__byte(3, 3, 1, name, os) {}; mu_1_ResponderId (void): mu__byte(3, 3, 1) {}; mu_1_ResponderId (int val): mu__byte(3, 3, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -3]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 3] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_ResponderId& a, mu_1_ResponderId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_ResponderId::values[] = { "ResponderId_1",NULL }; /*** end scalarset declaration ***/ mu_1_ResponderId mu_1_ResponderId_undefined_var; class mu_1_IntruderId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_IntruderId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_IntruderId& val) { if (val.defined()) return ( s << mu_1_IntruderId::values[ int(val) - 4 ] ); else return ( s << "Undefined" ); }; mu_1_IntruderId (char *name, int os): mu__byte(4, 4, 1, name, os) {}; mu_1_IntruderId (void): mu__byte(4, 4, 1) {}; mu_1_IntruderId (int val): mu__byte(4, 4, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -4]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 4] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_IntruderId& a, mu_1_IntruderId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_IntruderId::values[] = { "IntruderId_1",NULL }; /*** end scalarset declaration ***/ mu_1_IntruderId mu_1_IntruderId_undefined_var; class mu_1_SpiId: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1_SpiId& val) { return mu__byte::operator=((int) val); }; mu_1_SpiId (char *name, int os): mu__byte(0, 10, 4, name, os) {}; mu_1_SpiId (void): mu__byte(0, 10, 4) {}; mu_1_SpiId (int val): mu__byte(0, 10, 4, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_SpiId mu_1_SpiId_undefined_var; class mu_1_Random: public mu__long { public: inline int operator=(int val) { return mu__long::operator=(val); }; inline int operator=(const mu_1_Random& val) { return mu__long::operator=((int) val); }; mu_1_Random (char *name, int os): mu__long(0, 268435455, 29, name, os) {}; mu_1_Random (void): mu__long(0, 268435455, 29) {}; mu_1_Random (int val): mu__long(0, 268435455, 29, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_Random mu_1_Random_undefined_var; class mu_1_Integer: public mu__long { public: inline int operator=(int val) { return mu__long::operator=(val); }; inline int operator=(const mu_1_Integer& val) { return mu__long::operator=((int) val); }; mu_1_Integer (char *name, int os): mu__long(0, 99999, 17, name, os) {}; mu_1_Integer (void): mu__long(0, 99999, 17) {}; mu_1_Integer (int val): mu__long(0, 99999, 17, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_Integer mu_1_Integer_undefined_var; class mu_1_AgentId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_AgentId& val) { return value(val.value()); }; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_AgentId& val) { if (val.defined()) return ( s << mu_1_AgentId::values[ val.indexvalue() ] ); else return ( s << "Undefined" ); }; // note thate lb and ub are not used if we have byte compacted state. mu_1_AgentId (char *name, int os): mu__byte(0, 3, 3, name, os) {}; mu_1_AgentId (void): mu__byte(0, 3, 3) {}; mu_1_AgentId (int val): mu__byte(0, 3, 3, "Parameter or function result.", 0) { operator=(val); }; int value() const { int val = mu__byte::value(); // val == -1 if value undefined // we can return it since no enum/scalarsetid will have value -1 if (val == -1) return -1; if (val <= 0) return val+1; if (val <= 1) return val+1; if (val <= 2) return val+1; if (val <= 3) return val+1; } inline int value(int val) { if (val == -1) { undefine(); return -1; } if ((val >= 1) && (val <= 1)) return (mu__byte::value(val-1)+1); if ((val >= 2) && (val <= 2)) return (mu__byte::value(val-1)+1); if ((val >= 3) && (val <= 3)) return (mu__byte::value(val-1)+1); if ((val >= 4) && (val <= 4)) return (mu__byte::value(val-1)+1); } inline int indexvalue() const { return mu__byte::value(); }; inline int unionassign(int val) { return mu__byte::value(val); }; char * Name() { return values[ indexvalue() ]; }; friend int CompareWeight(mu_1_AgentId& a, mu_1_AgentId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void print() { if (defined()) cout << name << ':' << values[ indexvalue() ] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; }; char *mu_1_AgentId::values[] = {"InitiatorId_1","InitiatorIdP_1","ResponderId_1","IntruderId_1",NULL }; /*** end union declaration ***/ mu_1_AgentId mu_1_AgentId_undefined_var; class mu_1_MessageType: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_MessageType& val) { return value(val.value()); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_MessageType& val) { if (val.defined()) return ( s << mu_1_MessageType::values[ int(val) - 5] ); else return ( s << "Undefined" ); }; mu_1_MessageType (char *name, int os): mu__byte(5, 15, 4, name, os) {}; mu_1_MessageType (void): mu__byte(5, 15, 4) {}; mu_1_MessageType (int val): mu__byte(5, 15, 4, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -5]; }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; virtual void print() { if (defined()) cout << name << ":" << values[ value() -5] << '\n'; else cout << name << ":Undefined\n"; }; }; char *mu_1_MessageType::values[] = {"PRE_MOBIKE_1","MOBIKE_1","MOBIKE_2","MOBIKE_3","MOBIKE_4","MOBIKE_5","MOBIKE_6","MOBIKE_7","MOBIKE_8","MOBIKE_ADDR_CHANGE","MOBIKE_DONE",NULL }; /*** end of enum declaration ***/ mu_1_MessageType mu_1_MessageType_undefined_var; class mu_1_Ke { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_Random mu_random; mu_1_Ke ( char *n, int os ) { set_self(n,os); }; mu_1_Ke ( void ) {}; virtual ~mu_1_Ke(); friend int CompareWeight(mu_1_Ke& a, mu_1_Ke& b) { int w; w = CompareWeight(a.mu_random, b.mu_random); if (w!=0) return w; return 0; } friend int Compare(mu_1_Ke& a, mu_1_Ke& b) { int w; w = Compare(a.mu_random, b.mu_random); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_random.MultisetSort(); } void print_statistic() { mu_random.print_statistic(); } void clear() { mu_random.clear(); }; void undefine() { mu_random.undefine(); }; void reset() { mu_random.reset(); }; void print() { mu_random.print(); }; void print_diff(state *prevstate) { mu_random.print_diff(prevstate); }; void to_state(state *thestate) { mu_random.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Ke& operator= (const mu_1_Ke& from) { mu_random.value(from.mu_random.value()); return *this; }; }; void mu_1_Ke::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Ke::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Ke::set_self(char *n, int os) { name = n; mu_random.set_self_2(name, ".random", os + 0 ); } mu_1_Ke::~mu_1_Ke() { } /*** end record declaration ***/ mu_1_Ke mu_1_Ke_undefined_var; class mu_1_SessionKey { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_Random mu_random; mu_1_SessionKey ( char *n, int os ) { set_self(n,os); }; mu_1_SessionKey ( void ) {}; virtual ~mu_1_SessionKey(); friend int CompareWeight(mu_1_SessionKey& a, mu_1_SessionKey& b) { int w; w = CompareWeight(a.mu_random, b.mu_random); if (w!=0) return w; return 0; } friend int Compare(mu_1_SessionKey& a, mu_1_SessionKey& b) { int w; w = Compare(a.mu_random, b.mu_random); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_random.MultisetSort(); } void print_statistic() { mu_random.print_statistic(); } void clear() { mu_random.clear(); }; void undefine() { mu_random.undefine(); }; void reset() { mu_random.reset(); }; void print() { mu_random.print(); }; void print_diff(state *prevstate) { mu_random.print_diff(prevstate); }; void to_state(state *thestate) { mu_random.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_SessionKey& operator= (const mu_1_SessionKey& from) { mu_random.value(from.mu_random.value()); return *this; }; }; void mu_1_SessionKey::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_SessionKey::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_SessionKey::set_self(char *n, int os) { name = n; mu_random.set_self_2(name, ".random", os + 0 ); } mu_1_SessionKey::~mu_1_SessionKey() { } /*** end record declaration ***/ mu_1_SessionKey mu_1_SessionKey_undefined_var; class mu_1_Spi { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_Ke mu_ke; mu_1_Ke mu_peer_ke; mu_1_AgentId mu_peer; mu_1_SpiId mu_peer_spi_id; mu_1_SpiId mu_spi_id; mu_1_Random mu_nonce; mu_1_Random mu_peer_nonce; mu_1_Integer mu_msgid; mu_1_Integer mu_peer_msgid; mu_1_Random mu_cookie; mu_1_Random mu_exponent; mu_1_SessionKey mu_session_key; mu_1_MessageType mu_state; mu_0_boolean mu_in_use; mu_1_Spi ( char *n, int os ) { set_self(n,os); }; mu_1_Spi ( void ) {}; virtual ~mu_1_Spi(); friend int CompareWeight(mu_1_Spi& a, mu_1_Spi& b) { int w; w = CompareWeight(a.mu_ke, b.mu_ke); if (w!=0) return w; w = CompareWeight(a.mu_peer_ke, b.mu_peer_ke); if (w!=0) return w; w = CompareWeight(a.mu_peer, b.mu_peer); if (w!=0) return w; w = CompareWeight(a.mu_peer_spi_id, b.mu_peer_spi_id); if (w!=0) return w; w = CompareWeight(a.mu_spi_id, b.mu_spi_id); if (w!=0) return w; w = CompareWeight(a.mu_nonce, b.mu_nonce); if (w!=0) return w; w = CompareWeight(a.mu_peer_nonce, b.mu_peer_nonce); if (w!=0) return w; w = CompareWeight(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = CompareWeight(a.mu_peer_msgid, b.mu_peer_msgid); if (w!=0) return w; w = CompareWeight(a.mu_cookie, b.mu_cookie); if (w!=0) return w; w = CompareWeight(a.mu_exponent, b.mu_exponent); if (w!=0) return w; w = CompareWeight(a.mu_session_key, b.mu_session_key); if (w!=0) return w; w = CompareWeight(a.mu_state, b.mu_state); if (w!=0) return w; w = CompareWeight(a.mu_in_use, b.mu_in_use); if (w!=0) return w; return 0; } friend int Compare(mu_1_Spi& a, mu_1_Spi& b) { int w; w = Compare(a.mu_ke, b.mu_ke); if (w!=0) return w; w = Compare(a.mu_peer_ke, b.mu_peer_ke); if (w!=0) return w; w = Compare(a.mu_peer, b.mu_peer); if (w!=0) return w; w = Compare(a.mu_peer_spi_id, b.mu_peer_spi_id); if (w!=0) return w; w = Compare(a.mu_spi_id, b.mu_spi_id); if (w!=0) return w; w = Compare(a.mu_nonce, b.mu_nonce); if (w!=0) return w; w = Compare(a.mu_peer_nonce, b.mu_peer_nonce); if (w!=0) return w; w = Compare(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = Compare(a.mu_peer_msgid, b.mu_peer_msgid); if (w!=0) return w; w = Compare(a.mu_cookie, b.mu_cookie); if (w!=0) return w; w = Compare(a.mu_exponent, b.mu_exponent); if (w!=0) return w; w = Compare(a.mu_session_key, b.mu_session_key); if (w!=0) return w; w = Compare(a.mu_state, b.mu_state); if (w!=0) return w; w = Compare(a.mu_in_use, b.mu_in_use); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_ke.MultisetSort(); mu_peer_ke.MultisetSort(); mu_peer.MultisetSort(); mu_peer_spi_id.MultisetSort(); mu_spi_id.MultisetSort(); mu_nonce.MultisetSort(); mu_peer_nonce.MultisetSort(); mu_msgid.MultisetSort(); mu_peer_msgid.MultisetSort(); mu_cookie.MultisetSort(); mu_exponent.MultisetSort(); mu_session_key.MultisetSort(); mu_state.MultisetSort(); mu_in_use.MultisetSort(); } void print_statistic() { mu_ke.print_statistic(); mu_peer_ke.print_statistic(); mu_peer.print_statistic(); mu_peer_spi_id.print_statistic(); mu_spi_id.print_statistic(); mu_nonce.print_statistic(); mu_peer_nonce.print_statistic(); mu_msgid.print_statistic(); mu_peer_msgid.print_statistic(); mu_cookie.print_statistic(); mu_exponent.print_statistic(); mu_session_key.print_statistic(); mu_state.print_statistic(); mu_in_use.print_statistic(); } void clear() { mu_ke.clear(); mu_peer_ke.clear(); mu_peer.clear(); mu_peer_spi_id.clear(); mu_spi_id.clear(); mu_nonce.clear(); mu_peer_nonce.clear(); mu_msgid.clear(); mu_peer_msgid.clear(); mu_cookie.clear(); mu_exponent.clear(); mu_session_key.clear(); mu_state.clear(); mu_in_use.clear(); }; void undefine() { mu_ke.undefine(); mu_peer_ke.undefine(); mu_peer.undefine(); mu_peer_spi_id.undefine(); mu_spi_id.undefine(); mu_nonce.undefine(); mu_peer_nonce.undefine(); mu_msgid.undefine(); mu_peer_msgid.undefine(); mu_cookie.undefine(); mu_exponent.undefine(); mu_session_key.undefine(); mu_state.undefine(); mu_in_use.undefine(); }; void reset() { mu_ke.reset(); mu_peer_ke.reset(); mu_peer.reset(); mu_peer_spi_id.reset(); mu_spi_id.reset(); mu_nonce.reset(); mu_peer_nonce.reset(); mu_msgid.reset(); mu_peer_msgid.reset(); mu_cookie.reset(); mu_exponent.reset(); mu_session_key.reset(); mu_state.reset(); mu_in_use.reset(); }; void print() { mu_ke.print(); mu_peer_ke.print(); mu_peer.print(); mu_peer_spi_id.print(); mu_spi_id.print(); mu_nonce.print(); mu_peer_nonce.print(); mu_msgid.print(); mu_peer_msgid.print(); mu_cookie.print(); mu_exponent.print(); mu_session_key.print(); mu_state.print(); mu_in_use.print(); }; void print_diff(state *prevstate) { mu_ke.print_diff(prevstate); mu_peer_ke.print_diff(prevstate); mu_peer.print_diff(prevstate); mu_peer_spi_id.print_diff(prevstate); mu_spi_id.print_diff(prevstate); mu_nonce.print_diff(prevstate); mu_peer_nonce.print_diff(prevstate); mu_msgid.print_diff(prevstate); mu_peer_msgid.print_diff(prevstate); mu_cookie.print_diff(prevstate); mu_exponent.print_diff(prevstate); mu_session_key.print_diff(prevstate); mu_state.print_diff(prevstate); mu_in_use.print_diff(prevstate); }; void to_state(state *thestate) { mu_ke.to_state(thestate); mu_peer_ke.to_state(thestate); mu_peer.to_state(thestate); mu_peer_spi_id.to_state(thestate); mu_spi_id.to_state(thestate); mu_nonce.to_state(thestate); mu_peer_nonce.to_state(thestate); mu_msgid.to_state(thestate); mu_peer_msgid.to_state(thestate); mu_cookie.to_state(thestate); mu_exponent.to_state(thestate); mu_session_key.to_state(thestate); mu_state.to_state(thestate); mu_in_use.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Spi& operator= (const mu_1_Spi& from) { mu_ke = from.mu_ke; mu_peer_ke = from.mu_peer_ke; mu_peer.value(from.mu_peer.value()); mu_peer_spi_id.value(from.mu_peer_spi_id.value()); mu_spi_id.value(from.mu_spi_id.value()); mu_nonce.value(from.mu_nonce.value()); mu_peer_nonce.value(from.mu_peer_nonce.value()); mu_msgid.value(from.mu_msgid.value()); mu_peer_msgid.value(from.mu_peer_msgid.value()); mu_cookie.value(from.mu_cookie.value()); mu_exponent.value(from.mu_exponent.value()); mu_session_key = from.mu_session_key; mu_state.value(from.mu_state.value()); mu_in_use.value(from.mu_in_use.value()); return *this; }; }; void mu_1_Spi::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Spi::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Spi::set_self(char *n, int os) { name = n; mu_ke.set_self_2(name, ".ke", os + 0 ); mu_peer_ke.set_self_2(name, ".peer_ke", os + 29 ); mu_peer.set_self_2(name, ".peer", os + 58 ); mu_peer_spi_id.set_self_2(name, ".peer_spi_id", os + 61 ); mu_spi_id.set_self_2(name, ".spi_id", os + 65 ); mu_nonce.set_self_2(name, ".nonce", os + 69 ); mu_peer_nonce.set_self_2(name, ".peer_nonce", os + 98 ); mu_msgid.set_self_2(name, ".msgid", os + 127 ); mu_peer_msgid.set_self_2(name, ".peer_msgid", os + 144 ); mu_cookie.set_self_2(name, ".cookie", os + 161 ); mu_exponent.set_self_2(name, ".exponent", os + 190 ); mu_session_key.set_self_2(name, ".session_key", os + 219 ); mu_state.set_self_2(name, ".state", os + 248 ); mu_in_use.set_self_2(name, ".in_use", os + 252 ); } mu_1_Spi::~mu_1_Spi() { } /*** end record declaration ***/ mu_1_Spi mu_1_Spi_undefined_var; class mu_1_Auth { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_Integer mu_msgid; mu_1_Ke mu_ke; mu_1_Random mu_nonce; mu_1_SpiId mu_spi; mu_1_Random mu_peer_nonce; mu_1_AgentId mu_id_p; mu_1_Integer mu_shared_secret; mu_1_Auth ( char *n, int os ) { set_self(n,os); }; mu_1_Auth ( void ) {}; virtual ~mu_1_Auth(); friend int CompareWeight(mu_1_Auth& a, mu_1_Auth& b) { int w; w = CompareWeight(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = CompareWeight(a.mu_ke, b.mu_ke); if (w!=0) return w; w = CompareWeight(a.mu_nonce, b.mu_nonce); if (w!=0) return w; w = CompareWeight(a.mu_spi, b.mu_spi); if (w!=0) return w; w = CompareWeight(a.mu_peer_nonce, b.mu_peer_nonce); if (w!=0) return w; w = CompareWeight(a.mu_id_p, b.mu_id_p); if (w!=0) return w; w = CompareWeight(a.mu_shared_secret, b.mu_shared_secret); if (w!=0) return w; return 0; } friend int Compare(mu_1_Auth& a, mu_1_Auth& b) { int w; w = Compare(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = Compare(a.mu_ke, b.mu_ke); if (w!=0) return w; w = Compare(a.mu_nonce, b.mu_nonce); if (w!=0) return w; w = Compare(a.mu_spi, b.mu_spi); if (w!=0) return w; w = Compare(a.mu_peer_nonce, b.mu_peer_nonce); if (w!=0) return w; w = Compare(a.mu_id_p, b.mu_id_p); if (w!=0) return w; w = Compare(a.mu_shared_secret, b.mu_shared_secret); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_msgid.MultisetSort(); mu_ke.MultisetSort(); mu_nonce.MultisetSort(); mu_spi.MultisetSort(); mu_peer_nonce.MultisetSort(); mu_id_p.MultisetSort(); mu_shared_secret.MultisetSort(); } void print_statistic() { mu_msgid.print_statistic(); mu_ke.print_statistic(); mu_nonce.print_statistic(); mu_spi.print_statistic(); mu_peer_nonce.print_statistic(); mu_id_p.print_statistic(); mu_shared_secret.print_statistic(); } void clear() { mu_msgid.clear(); mu_ke.clear(); mu_nonce.clear(); mu_spi.clear(); mu_peer_nonce.clear(); mu_id_p.clear(); mu_shared_secret.clear(); }; void undefine() { mu_msgid.undefine(); mu_ke.undefine(); mu_nonce.undefine(); mu_spi.undefine(); mu_peer_nonce.undefine(); mu_id_p.undefine(); mu_shared_secret.undefine(); }; void reset() { mu_msgid.reset(); mu_ke.reset(); mu_nonce.reset(); mu_spi.reset(); mu_peer_nonce.reset(); mu_id_p.reset(); mu_shared_secret.reset(); }; void print() { mu_msgid.print(); mu_ke.print(); mu_nonce.print(); mu_spi.print(); mu_peer_nonce.print(); mu_id_p.print(); mu_shared_secret.print(); }; void print_diff(state *prevstate) { mu_msgid.print_diff(prevstate); mu_ke.print_diff(prevstate); mu_nonce.print_diff(prevstate); mu_spi.print_diff(prevstate); mu_peer_nonce.print_diff(prevstate); mu_id_p.print_diff(prevstate); mu_shared_secret.print_diff(prevstate); }; void to_state(state *thestate) { mu_msgid.to_state(thestate); mu_ke.to_state(thestate); mu_nonce.to_state(thestate); mu_spi.to_state(thestate); mu_peer_nonce.to_state(thestate); mu_id_p.to_state(thestate); mu_shared_secret.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Auth& operator= (const mu_1_Auth& from) { mu_msgid.value(from.mu_msgid.value()); mu_ke = from.mu_ke; mu_nonce.value(from.mu_nonce.value()); mu_spi.value(from.mu_spi.value()); mu_peer_nonce.value(from.mu_peer_nonce.value()); mu_id_p.value(from.mu_id_p.value()); mu_shared_secret.value(from.mu_shared_secret.value()); return *this; }; }; void mu_1_Auth::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Auth::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Auth::set_self(char *n, int os) { name = n; mu_msgid.set_self_2(name, ".msgid", os + 0 ); mu_ke.set_self_2(name, ".ke", os + 17 ); mu_nonce.set_self_2(name, ".nonce", os + 46 ); mu_spi.set_self_2(name, ".spi", os + 75 ); mu_peer_nonce.set_self_2(name, ".peer_nonce", os + 79 ); mu_id_p.set_self_2(name, ".id_p", os + 108 ); mu_shared_secret.set_self_2(name, ".shared_secret", os + 111 ); } mu_1_Auth::~mu_1_Auth() { } /*** end record declaration ***/ mu_1_Auth mu_1_Auth_undefined_var; class mu_1_Message { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_AgentId mu_source; mu_1_AgentId mu_dest; mu_1_Integer mu_msgid; mu_1_SpiId mu_init_spi; mu_1_SpiId mu_resp_spi; mu_1_MessageType mu_mType; mu_1_Ke mu_ke_i; mu_1_Ke mu_ke_r; mu_1_Random mu_nonce_i; mu_1_Random mu_nonce_r; mu_1_AgentId mu_id_i; mu_1_AgentId mu_id_r; mu_1_Auth mu_auth; mu_0_boolean mu_mobike_s; mu_1_AgentId mu_upd_addr; mu_1_Random mu_cookie; mu_1_AgentId mu_no_nats_allowed_source; mu_1_AgentId mu_no_nats_allowed_dest; mu_1_SessionKey mu_session_key; mu_0_boolean mu_from_intruder; mu_1_Message ( char *n, int os ) { set_self(n,os); }; mu_1_Message ( void ) {}; virtual ~mu_1_Message(); friend int CompareWeight(mu_1_Message& a, mu_1_Message& b) { int w; w = CompareWeight(a.mu_source, b.mu_source); if (w!=0) return w; w = CompareWeight(a.mu_dest, b.mu_dest); if (w!=0) return w; w = CompareWeight(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = CompareWeight(a.mu_init_spi, b.mu_init_spi); if (w!=0) return w; w = CompareWeight(a.mu_resp_spi, b.mu_resp_spi); if (w!=0) return w; w = CompareWeight(a.mu_mType, b.mu_mType); if (w!=0) return w; w = CompareWeight(a.mu_ke_i, b.mu_ke_i); if (w!=0) return w; w = CompareWeight(a.mu_ke_r, b.mu_ke_r); if (w!=0) return w; w = CompareWeight(a.mu_nonce_i, b.mu_nonce_i); if (w!=0) return w; w = CompareWeight(a.mu_nonce_r, b.mu_nonce_r); if (w!=0) return w; w = CompareWeight(a.mu_id_i, b.mu_id_i); if (w!=0) return w; w = CompareWeight(a.mu_id_r, b.mu_id_r); if (w!=0) return w; w = CompareWeight(a.mu_auth, b.mu_auth); if (w!=0) return w; w = CompareWeight(a.mu_mobike_s, b.mu_mobike_s); if (w!=0) return w; w = CompareWeight(a.mu_upd_addr, b.mu_upd_addr); if (w!=0) return w; w = CompareWeight(a.mu_cookie, b.mu_cookie); if (w!=0) return w; w = CompareWeight(a.mu_no_nats_allowed_source, b.mu_no_nats_allowed_source); if (w!=0) return w; w = CompareWeight(a.mu_no_nats_allowed_dest, b.mu_no_nats_allowed_dest); if (w!=0) return w; w = CompareWeight(a.mu_session_key, b.mu_session_key); if (w!=0) return w; w = CompareWeight(a.mu_from_intruder, b.mu_from_intruder); if (w!=0) return w; return 0; } friend int Compare(mu_1_Message& a, mu_1_Message& b) { int w; w = Compare(a.mu_source, b.mu_source); if (w!=0) return w; w = Compare(a.mu_dest, b.mu_dest); if (w!=0) return w; w = Compare(a.mu_msgid, b.mu_msgid); if (w!=0) return w; w = Compare(a.mu_init_spi, b.mu_init_spi); if (w!=0) return w; w = Compare(a.mu_resp_spi, b.mu_resp_spi); if (w!=0) return w; w = Compare(a.mu_mType, b.mu_mType); if (w!=0) return w; w = Compare(a.mu_ke_i, b.mu_ke_i); if (w!=0) return w; w = Compare(a.mu_ke_r, b.mu_ke_r); if (w!=0) return w; w = Compare(a.mu_nonce_i, b.mu_nonce_i); if (w!=0) return w; w = Compare(a.mu_nonce_r, b.mu_nonce_r); if (w!=0) return w; w = Compare(a.mu_id_i, b.mu_id_i); if (w!=0) return w; w = Compare(a.mu_id_r, b.mu_id_r); if (w!=0) return w; w = Compare(a.mu_auth, b.mu_auth); if (w!=0) return w; w = Compare(a.mu_mobike_s, b.mu_mobike_s); if (w!=0) return w; w = Compare(a.mu_upd_addr, b.mu_upd_addr); if (w!=0) return w; w = Compare(a.mu_cookie, b.mu_cookie); if (w!=0) return w; w = Compare(a.mu_no_nats_allowed_source, b.mu_no_nats_allowed_source); if (w!=0) return w; w = Compare(a.mu_no_nats_allowed_dest, b.mu_no_nats_allowed_dest); if (w!=0) return w; w = Compare(a.mu_session_key, b.mu_session_key); if (w!=0) return w; w = Compare(a.mu_from_intruder, b.mu_from_intruder); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_source.MultisetSort(); mu_dest.MultisetSort(); mu_msgid.MultisetSort(); mu_init_spi.MultisetSort(); mu_resp_spi.MultisetSort(); mu_mType.MultisetSort(); mu_ke_i.MultisetSort(); mu_ke_r.MultisetSort(); mu_nonce_i.MultisetSort(); mu_nonce_r.MultisetSort(); mu_id_i.MultisetSort(); mu_id_r.MultisetSort(); mu_auth.MultisetSort(); mu_mobike_s.MultisetSort(); mu_upd_addr.MultisetSort(); mu_cookie.MultisetSort(); mu_no_nats_allowed_source.MultisetSort(); mu_no_nats_allowed_dest.MultisetSort(); mu_session_key.MultisetSort(); mu_from_intruder.MultisetSort(); } void print_statistic() { mu_source.print_statistic(); mu_dest.print_statistic(); mu_msgid.print_statistic(); mu_init_spi.print_statistic(); mu_resp_spi.print_statistic(); mu_mType.print_statistic(); mu_ke_i.print_statistic(); mu_ke_r.print_statistic(); mu_nonce_i.print_statistic(); mu_nonce_r.print_statistic(); mu_id_i.print_statistic(); mu_id_r.print_statistic(); mu_auth.print_statistic(); mu_mobike_s.print_statistic(); mu_upd_addr.print_statistic(); mu_cookie.print_statistic(); mu_no_nats_allowed_source.print_statistic(); mu_no_nats_allowed_dest.print_statistic(); mu_session_key.print_statistic(); mu_from_intruder.print_statistic(); } void clear() { mu_source.clear(); mu_dest.clear(); mu_msgid.clear(); mu_init_spi.clear(); mu_resp_spi.clear(); mu_mType.clear(); mu_ke_i.clear(); mu_ke_r.clear(); mu_nonce_i.clear(); mu_nonce_r.clear(); mu_id_i.clear(); mu_id_r.clear(); mu_auth.clear(); mu_mobike_s.clear(); mu_upd_addr.clear(); mu_cookie.clear(); mu_no_nats_allowed_source.clear(); mu_no_nats_allowed_dest.clear(); mu_session_key.clear(); mu_from_intruder.clear(); }; void undefine() { mu_source.undefine(); mu_dest.undefine(); mu_msgid.undefine(); mu_init_spi.undefine(); mu_resp_spi.undefine(); mu_mType.undefine(); mu_ke_i.undefine(); mu_ke_r.undefine(); mu_nonce_i.undefine(); mu_nonce_r.undefine(); mu_id_i.undefine(); mu_id_r.undefine(); mu_auth.undefine(); mu_mobike_s.undefine(); mu_upd_addr.undefine(); mu_cookie.undefine(); mu_no_nats_allowed_source.undefine(); mu_no_nats_allowed_dest.undefine(); mu_session_key.undefine(); mu_from_intruder.undefine(); }; void reset() { mu_source.reset(); mu_dest.reset(); mu_msgid.reset(); mu_init_spi.reset(); mu_resp_spi.reset(); mu_mType.reset(); mu_ke_i.reset(); mu_ke_r.reset(); mu_nonce_i.reset(); mu_nonce_r.reset(); mu_id_i.reset(); mu_id_r.reset(); mu_auth.reset(); mu_mobike_s.reset(); mu_upd_addr.reset(); mu_cookie.reset(); mu_no_nats_allowed_source.reset(); mu_no_nats_allowed_dest.reset(); mu_session_key.reset(); mu_from_intruder.reset(); }; void print() { mu_source.print(); mu_dest.print(); mu_msgid.print(); mu_init_spi.print(); mu_resp_spi.print(); mu_mType.print(); mu_ke_i.print(); mu_ke_r.print(); mu_nonce_i.print(); mu_nonce_r.print(); mu_id_i.print(); mu_id_r.print(); mu_auth.print(); mu_mobike_s.print(); mu_upd_addr.print(); mu_cookie.print(); mu_no_nats_allowed_source.print(); mu_no_nats_allowed_dest.print(); mu_session_key.print(); mu_from_intruder.print(); }; void print_diff(state *prevstate) { mu_source.print_diff(prevstate); mu_dest.print_diff(prevstate); mu_msgid.print_diff(prevstate); mu_init_spi.print_diff(prevstate); mu_resp_spi.print_diff(prevstate); mu_mType.print_diff(prevstate); mu_ke_i.print_diff(prevstate); mu_ke_r.print_diff(prevstate); mu_nonce_i.print_diff(prevstate); mu_nonce_r.print_diff(prevstate); mu_id_i.print_diff(prevstate); mu_id_r.print_diff(prevstate); mu_auth.print_diff(prevstate); mu_mobike_s.print_diff(prevstate); mu_upd_addr.print_diff(prevstate); mu_cookie.print_diff(prevstate); mu_no_nats_allowed_source.print_diff(prevstate); mu_no_nats_allowed_dest.print_diff(prevstate); mu_session_key.print_diff(prevstate); mu_from_intruder.print_diff(prevstate); }; void to_state(state *thestate) { mu_source.to_state(thestate); mu_dest.to_state(thestate); mu_msgid.to_state(thestate); mu_init_spi.to_state(thestate); mu_resp_spi.to_state(thestate); mu_mType.to_state(thestate); mu_ke_i.to_state(thestate); mu_ke_r.to_state(thestate); mu_nonce_i.to_state(thestate); mu_nonce_r.to_state(thestate); mu_id_i.to_state(thestate); mu_id_r.to_state(thestate); mu_auth.to_state(thestate); mu_mobike_s.to_state(thestate); mu_upd_addr.to_state(thestate); mu_cookie.to_state(thestate); mu_no_nats_allowed_source.to_state(thestate); mu_no_nats_allowed_dest.to_state(thestate); mu_session_key.to_state(thestate); mu_from_intruder.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Message& operator= (const mu_1_Message& from) { mu_source.value(from.mu_source.value()); mu_dest.value(from.mu_dest.value()); mu_msgid.value(from.mu_msgid.value()); mu_init_spi.value(from.mu_init_spi.value()); mu_resp_spi.value(from.mu_resp_spi.value()); mu_mType.value(from.mu_mType.value()); mu_ke_i = from.mu_ke_i; mu_ke_r = from.mu_ke_r; mu_nonce_i.value(from.mu_nonce_i.value()); mu_nonce_r.value(from.mu_nonce_r.value()); mu_id_i.value(from.mu_id_i.value()); mu_id_r.value(from.mu_id_r.value()); mu_auth = from.mu_auth; mu_mobike_s.value(from.mu_mobike_s.value()); mu_upd_addr.value(from.mu_upd_addr.value()); mu_cookie.value(from.mu_cookie.value()); mu_no_nats_allowed_source.value(from.mu_no_nats_allowed_source.value()); mu_no_nats_allowed_dest.value(from.mu_no_nats_allowed_dest.value()); mu_session_key = from.mu_session_key; mu_from_intruder.value(from.mu_from_intruder.value()); return *this; }; }; void mu_1_Message::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Message::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Message::set_self(char *n, int os) { name = n; mu_source.set_self_2(name, ".source", os + 0 ); mu_dest.set_self_2(name, ".dest", os + 3 ); mu_msgid.set_self_2(name, ".msgid", os + 6 ); mu_init_spi.set_self_2(name, ".init_spi", os + 23 ); mu_resp_spi.set_self_2(name, ".resp_spi", os + 27 ); mu_mType.set_self_2(name, ".mType", os + 31 ); mu_ke_i.set_self_2(name, ".ke_i", os + 35 ); mu_ke_r.set_self_2(name, ".ke_r", os + 64 ); mu_nonce_i.set_self_2(name, ".nonce_i", os + 93 ); mu_nonce_r.set_self_2(name, ".nonce_r", os + 122 ); mu_id_i.set_self_2(name, ".id_i", os + 151 ); mu_id_r.set_self_2(name, ".id_r", os + 154 ); mu_auth.set_self_2(name, ".auth", os + 157 ); mu_mobike_s.set_self_2(name, ".mobike_s", os + 285 ); mu_upd_addr.set_self_2(name, ".upd_addr", os + 287 ); mu_cookie.set_self_2(name, ".cookie", os + 290 ); mu_no_nats_allowed_source.set_self_2(name, ".no_nats_allowed_source", os + 319 ); mu_no_nats_allowed_dest.set_self_2(name, ".no_nats_allowed_dest", os + 322 ); mu_session_key.set_self_2(name, ".session_key", os + 325 ); mu_from_intruder.set_self_2(name, ".from_intruder", os + 354 ); } mu_1_Message::~mu_1_Message() { } /*** end record declaration ***/ mu_1_Message mu_1_Message_undefined_var; class mu_1__type_0 { public: mu_0_boolean array[ 4 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_0 (char *n, int os) { set_self(n, os); }; mu_1__type_0 ( void ) {}; virtual ~mu_1__type_0 (); mu_0_boolean& operator[] (int index) /* const */ { if ( ( index >= 1 ) && ( index <= 1 ) ) return array[ index - (1) ]; if ( ( index >= 2 ) && ( index <= 2 ) ) return array[ index - (1) ]; if ( ( index >= 3 ) && ( index <= 3 ) ) return array[ index - (1) ]; if ( ( index >= 4 ) && ( index <= 4 ) ) return array[ index - (1) ]; if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s. (Internal Error in Type Checking.",index, name); return array[0]; } mu_1__type_0& operator= (const mu_1__type_0& from) { for (int i = 0; i < 4; i++) array[i].value(from.array[i].value()); return *this; } friend int CompareWeight(mu_1__type_0& a, mu_1__type_0& b) { int w; for (int i=0; i<4; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_0& a, mu_1__type_0& b) { int w; for (int i=0; i<4; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<4; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<4; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 4; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 4; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 4; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 4; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 4; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 4; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_0::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_0::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_0::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"InitiatorId_1", i * 2 + os);i++; array[i].set_self_ar(n,"InitiatorIdP_1", i * 2 + os);i++; array[i].set_self_ar(n,"ResponderId_1", i * 2 + os);i++; array[i].set_self_ar(n,"IntruderId_1", i * 2 + os);i++; } mu_1__type_0::~mu_1__type_0() { } /*** end array declaration ***/ mu_1__type_0 mu_1__type_0_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_1_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_1_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_1_id () : mu__byte(0,9,0) {}; mu_1__type_1_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_1 { public: mu_1_Message array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_1 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_1 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_1 (); mu_1_Message& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_1& operator= (const mu_1__type_1& from) { for (int i = 0; i < 10; i++) { array[i] = from.array[i]; valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_1& a, mu_1__type_1& b) { return 0; } friend int Compare(mu_1__type_1& a, mu_1__type_1& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_1_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Message temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_1::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_1::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_1::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 356 + os); k = os + i * 356; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_1::~mu_1__type_1() { } /*** end multiset declaration ***/ mu_1__type_1 mu_1__type_1_undefined_var; class mu_1_Intruder { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1__type_0 mu_nonces; mu_1__type_1 mu_messages; mu_1_Intruder ( char *n, int os ) { set_self(n,os); }; mu_1_Intruder ( void ) {}; virtual ~mu_1_Intruder(); friend int CompareWeight(mu_1_Intruder& a, mu_1_Intruder& b) { int w; w = CompareWeight(a.mu_nonces, b.mu_nonces); if (w!=0) return w; w = CompareWeight(a.mu_messages, b.mu_messages); if (w!=0) return w; return 0; } friend int Compare(mu_1_Intruder& a, mu_1_Intruder& b) { int w; w = Compare(a.mu_nonces, b.mu_nonces); if (w!=0) return w; w = Compare(a.mu_messages, b.mu_messages); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_nonces.MultisetSort(); mu_messages.MultisetSort(); } void print_statistic() { mu_nonces.print_statistic(); mu_messages.print_statistic(); } void clear() { mu_nonces.clear(); mu_messages.clear(); }; void undefine() { mu_nonces.undefine(); mu_messages.undefine(); }; void reset() { mu_nonces.reset(); mu_messages.reset(); }; void print() { mu_nonces.print(); mu_messages.print(); }; void print_diff(state *prevstate) { mu_nonces.print_diff(prevstate); mu_messages.print_diff(prevstate); }; void to_state(state *thestate) { mu_nonces.to_state(thestate); mu_messages.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Intruder& operator= (const mu_1_Intruder& from) { mu_nonces = from.mu_nonces; mu_messages = from.mu_messages; return *this; }; }; void mu_1_Intruder::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Intruder::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Intruder::set_self(char *n, int os) { name = n; mu_nonces.set_self_2(name, ".nonces", os + 0 ); mu_messages.set_self_2(name, ".messages", os + 8 ); } mu_1_Intruder::~mu_1_Intruder() { } /*** end record declaration ***/ mu_1_Intruder mu_1_Intruder_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_2_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_2_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_2_id () : mu__byte(0,0,0) {}; mu_1__type_2_id (int val) : mu__byte(0,0,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_2 { public: mu_1_Message array[ 1 ]; int max_size; int current_size; public: mu_0_boolean valid[ 1 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_2 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_2 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_2 (); mu_1_Message& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 0) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_2& operator= (const mu_1__type_2& from) { { array[0] = from.array[0]; valid[0].value(from.valid[0].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_2& a, mu_1__type_2& b) { return 0; } friend int Compare(mu_1__type_2& a, mu_1__type_2& b) { int w; for (int i=0; i<1; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 1; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 1; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 1; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 1; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 1; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 1; i++) if (valid[i].value()) current_size++; if (max_size= 1) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 1; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_2_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Message temp; // compact int i,j; for (i = 0, j = 0; i < 1; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 1; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 1; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_2::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_2::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_2::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 1; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 356 + os); k = os + i * 356; for(i = 0; i < 1; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_2::~mu_1__type_2() { } /*** end multiset declaration ***/ mu_1__type_2 mu_1__type_2_undefined_var; class mu_1__type_3 { public: mu_1_Spi array[ 11 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_3 (char *n, int os) { set_self(n, os); }; mu_1__type_3 ( void ) {}; virtual ~mu_1__type_3 (); mu_1_Spi& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 0 ) && ( index <= 10 ) ) return array[ index - 0 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("%d not in index range of %s.", index, name); return array[0]; } #else return array[ index - 0 ]; #endif }; mu_1__type_3& operator= (const mu_1__type_3& from) { for (int i = 0; i < 11; i++) array[i] = from.array[i]; return *this; } friend int CompareWeight(mu_1__type_3& a, mu_1__type_3& b) { int w; for (int i=0; i<11; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_3& a, mu_1__type_3& b) { int w; for (int i=0; i<11; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<11; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<11; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 11; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 11; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 11; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 11; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 11; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 11; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_3::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_3::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_3::set_self( char *n, int os) { char* s; name = n; for(int i = 0; i < 11; i++) { array[i].set_self_ar(n, s=tsprintf("%d",i + 0), i * 254 + os); delete[] s; } }; mu_1__type_3::~mu_1__type_3() { } /*** end array declaration ***/ mu_1__type_3 mu_1__type_3_undefined_var; class mu_1__type_4 { public: mu_1_Spi array[ 11 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_4 (char *n, int os) { set_self(n, os); }; mu_1__type_4 ( void ) {}; virtual ~mu_1__type_4 (); mu_1_Spi& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 0 ) && ( index <= 10 ) ) return array[ index - 0 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("%d not in index range of %s.", index, name); return array[0]; } #else return array[ index - 0 ]; #endif }; mu_1__type_4& operator= (const mu_1__type_4& from) { for (int i = 0; i < 11; i++) array[i] = from.array[i]; return *this; } friend int CompareWeight(mu_1__type_4& a, mu_1__type_4& b) { int w; for (int i=0; i<11; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_4& a, mu_1__type_4& b) { int w; for (int i=0; i<11; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<11; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<11; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 11; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 11; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 11; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 11; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 11; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 11; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_4::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_4::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_4::set_self( char *n, int os) { char* s; name = n; for(int i = 0; i < 11; i++) { array[i].set_self_ar(n, s=tsprintf("%d",i + 0), i * 254 + os); delete[] s; } }; mu_1__type_4::~mu_1__type_4() { } /*** end array declaration ***/ mu_1__type_4 mu_1__type_4_undefined_var; class mu_1__type_5 { public: mu_1_Intruder array[ 1 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_5 (char *n, int os) { set_self(n, os); }; mu_1__type_5 ( void ) {}; virtual ~mu_1__type_5 (); mu_1_Intruder& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 4 ) && ( index <= 4 ) ) return array[ index - 4 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s: IntruderId is internally represented from 4 to 4.\nInternal Error in Type checking.",index, name); return array[0]; } #else return array[ index - 4 ]; #endif }; mu_1__type_5& operator= (const mu_1__type_5& from) { array[0] = from.array[0]; return *this; } friend int CompareWeight(mu_1__type_5& a, mu_1__type_5& b) { int w; for (int i=0; i<1; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_5& a, mu_1__type_5& b) { int w; for (int i=0; i<1; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<1; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<1; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 1; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 1; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 1; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 1; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 1; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 1; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_5::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_5::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_5::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"IntruderId_1", i * 3588 + os);i++; } mu_1__type_5::~mu_1__type_5() { } /*** end array declaration ***/ mu_1__type_5 mu_1__type_5_undefined_var; const int mu_NO_NATS_ALLOWED = 1; const int mu_NumInitiators = 1; const int mu_NumResponders = 1; const int mu_NumInitiators_p = 1; const int mu_NumIntruders = 1; const int mu_NetworkSize = 1; const int mu_MaxKnowledge = 10; const int mu_MaxRandom = 268435455; const int mu_MaxSpis = 10; const int mu_SharedSecret = 12345; const int mu_Generator = 2; const int mu_Prime = 7919; const int mu_InitiatorId_1 = 1; const int mu_InitiatorIdP_1 = 2; const int mu_ResponderId_1 = 3; const int mu_IntruderId_1 = 4; const int mu_PRE_MOBIKE_1 = 5; const int mu_MOBIKE_1 = 6; const int mu_MOBIKE_2 = 7; const int mu_MOBIKE_3 = 8; const int mu_MOBIKE_4 = 9; const int mu_MOBIKE_5 = 10; const int mu_MOBIKE_6 = 11; const int mu_MOBIKE_7 = 12; const int mu_MOBIKE_8 = 13; const int mu_MOBIKE_ADDR_CHANGE = 14; const int mu_MOBIKE_DONE = 15; /*** Variable declaration ***/ mu_1__type_2 mu_net("net",0); /*** Variable declaration ***/ mu_1__type_3 mu_initiator_spi("initiator_spi",358); /*** Variable declaration ***/ mu_1__type_4 mu_responder_spi("responder_spi",3152); /*** Variable declaration ***/ mu_1_Random mu_next_random("next_random",5946); /*** Variable declaration ***/ mu_1_SpiId mu_initiator_num_spis("initiator_num_spis",5975); /*** Variable declaration ***/ mu_1__type_5 mu_int("int",5979); mu_1_Random mu_new_random() { /*** Variable declaration ***/ mu_1_Random mu_tmp("tmp",0); if (mu_next_random.isundefined()) mu_tmp.undefine(); else mu_tmp = mu_next_random; mu_next_random = (mu_next_random) + (1); return mu_tmp; Error.Error("The end of function new_random reached without returning values."); }; /*** end function declaration ***/ mu_1_Ke mu_make_ke(const mu_1_Random& mu_exponent) { /*** Variable declaration ***/ mu_1_Ke mu_tmp_ke("tmp_ke",0); /*** Variable declaration ***/ mu_1_Random mu_tmp_exp("tmp_exp",29); if (mu_exponent.isundefined()) mu_tmp_exp.undefine(); else mu_tmp_exp = mu_exponent; if ( (mu_tmp_exp) == (0) ) { Error.Error("Error: make_ke: exponent not allowed to be 0\n"); } else { mu_tmp_ke.mu_random = mu_Generator; { bool mu__while_expr_7; mu__while_expr_7 = (mu_tmp_exp) > (1); int mu__counter_6 = 0; while (mu__while_expr_7) { if ( ++mu__counter_6 > args->loopmax.value ) Error.Error("Too many iterations in while loop."); { mu_tmp_ke.mu_random = (mu_tmp_ke.mu_random) * (mu_Generator); mu_tmp_exp = (mu_tmp_exp) - (1); }; mu__while_expr_7 = (mu_tmp_exp) > (1); } }; mu_tmp_ke.mu_random = (mu_tmp_ke.mu_random) % (mu_Prime); } return mu_tmp_ke; Error.Error("The end of function make_ke reached without returning values."); }; /*** end function declaration ***/ mu_1_SessionKey mu_make_session_key(mu_1_Ke& mu_ke_peer,const mu_1_Random& mu_exponent) { /*** Variable declaration ***/ mu_1_SessionKey mu_tmp_sk("tmp_sk",0); /*** Variable declaration ***/ mu_1_Random mu_tmp_exp("tmp_exp",29); if (mu_exponent.isundefined()) mu_tmp_exp.undefine(); else mu_tmp_exp = mu_exponent; if ( (mu_tmp_exp) == (0) ) { Error.Error("Error: make_session_key: exponent not allowed to be 0\n"); } else { mu_tmp_sk.mu_random = mu_ke_peer.mu_random; { bool mu__while_expr_9; mu__while_expr_9 = (mu_tmp_exp) > (1); int mu__counter_8 = 0; while (mu__while_expr_9) { if ( ++mu__counter_8 > args->loopmax.value ) Error.Error("Too many iterations in while loop."); { mu_tmp_sk.mu_random = (mu_tmp_sk.mu_random) * (mu_Generator); mu_tmp_exp = (mu_tmp_exp) - (1); }; mu__while_expr_9 = (mu_tmp_exp) > (1); } }; mu_tmp_sk.mu_random = (mu_tmp_sk.mu_random) % (mu_Prime); } return mu_tmp_sk; Error.Error("The end of function make_session_key reached without returning values."); }; /*** end function declaration ***/ mu_1_Spi mu_initiator_new_spi() { { for(int mu_i = 0; mu_i <= 10; mu_i++) { bool mu__boolexpr10; if (!((mu_i) != (0))) mu__boolexpr10 = FALSE ; else { mu__boolexpr10 = ((mu_initiator_spi[mu_i].mu_in_use) == (mu_false)) ; } if ( mu__boolexpr10 ) { mu_initiator_spi[mu_i].mu_in_use = mu_true; mu_initiator_num_spis = (mu_initiator_num_spis) + (1); return mu_initiator_spi[mu_i]; } }; }; Error.Error("Error: initiator: no more spis available"); Error.Error("The end of function initiator_new_spi reached without returning values."); }; /*** end function declaration ***/ mu_1_Spi mu_responder_new_spi() { { for(int mu_i = 0; mu_i <= 10; mu_i++) { bool mu__boolexpr11; if (!((mu_i) != (0))) mu__boolexpr11 = FALSE ; else { mu__boolexpr11 = ((mu_responder_spi[mu_i].mu_in_use) == (mu_false)) ; } if ( mu__boolexpr11 ) { mu_responder_spi[mu_i].mu_in_use = mu_true; return mu_responder_spi[mu_i]; } }; }; Error.Error("Error: responder: no more spis available"); Error.Error("The end of function responder_new_spi reached without returning values."); }; /*** end function declaration ***/ /******************** The world ********************/ void world_class::clear() { mu_net.clear(); mu_initiator_spi.clear(); mu_responder_spi.clear(); mu_next_random.clear(); mu_initiator_num_spis.clear(); mu_int.clear(); } void world_class::undefine() { mu_net.undefine(); mu_initiator_spi.undefine(); mu_responder_spi.undefine(); mu_next_random.undefine(); mu_initiator_num_spis.undefine(); mu_int.undefine(); } void world_class::reset() { mu_net.reset(); mu_initiator_spi.reset(); mu_responder_spi.reset(); mu_next_random.reset(); mu_initiator_num_spis.reset(); mu_int.reset(); } void world_class::print() { static int num_calls = 0; /* to ward off recursive calls. */ if ( num_calls == 0 ) { num_calls++; mu_net.print(); mu_initiator_spi.print(); mu_responder_spi.print(); mu_next_random.print(); mu_initiator_num_spis.print(); mu_int.print(); num_calls--; } } void world_class::print_statistic() { static int num_calls = 0; /* to ward off recursive calls. */ if ( num_calls == 0 ) { num_calls++; mu_net.print_statistic(); mu_initiator_spi.print_statistic(); mu_responder_spi.print_statistic(); mu_next_random.print_statistic(); mu_initiator_num_spis.print_statistic(); mu_int.print_statistic(); num_calls--; } } void world_class::print_diff( state *prevstate ) { if ( prevstate != NULL ) { mu_net.print_diff(prevstate); mu_initiator_spi.print_diff(prevstate); mu_responder_spi.print_diff(prevstate); mu_next_random.print_diff(prevstate); mu_initiator_num_spis.print_diff(prevstate); mu_int.print_diff(prevstate); } else print(); } void world_class::to_state(state *newstate) { mu_net.to_state( newstate ); mu_initiator_spi.to_state( newstate ); mu_responder_spi.to_state( newstate ); mu_next_random.to_state( newstate ); mu_initiator_num_spis.to_state( newstate ); mu_int.to_state( newstate ); } void world_class::setstate(state *thestate) { } /******************** Rule declarations ********************/ /******************** RuleBase0 ********************/ class RuleBase0 { public: int Priority() { return 90; } char * Name(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_1_id mu_msg_index; mu_msg_index.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 4); r = r / 4; static mu_1_AgentId mu_j; mu_j.unionassign(r % 4); r = r / 4; return tsprintf("intruder sends recorded message, i:%s, msg_index:%s, k:%s, j:%s", mu_i.Name(), mu_msg_index.Name(), mu_k.Name(), mu_j.Name()); } bool Condition(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_1_id mu_msg_index; mu_msg_index.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 4); r = r / 4; static mu_1_AgentId mu_j; mu_j.unionassign(r % 4); r = r / 4; if (!mu_int[mu_i].mu_messages.in(mu_msg_index)) { return FALSE; } bool mu__boolexpr12; if (!((mu_j) != (mu_k))) mu__boolexpr12 = FALSE ; else { /*** begin multisetcount 3 declaration ***/ int mu__intexpr13 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr13++; } if (mu_l == 1-1) break; } } /*** end multisetcount 3 declaration ***/ mu__boolexpr12 = ((mu__intexpr13) < (mu_NetworkSize)) ; } return mu__boolexpr12; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 0; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_1_id mu_msg_index; mu_msg_index.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 4); r = r / 4; static mu_1_AgentId mu_j; mu_j.unionassign(r % 4); r = r / 4; while (what_rule < 160 && mu_msg_index.value()<10 ) { if ( ( TRUE ) ) { bool mu__boolexpr14; if (!((mu_j) != (mu_k))) mu__boolexpr14 = FALSE ; else { /*** begin multisetcount 3 declaration ***/ int mu__intexpr15 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr15++; } if (mu_l == 1-1) break; } } /*** end multisetcount 3 declaration ***/ mu__boolexpr14 = ((mu__intexpr15) < (mu_NetworkSize)) ; } if (mu__boolexpr14) { if ( ( TRUE && mu_int[mu_i].mu_messages.in(mu_msg_index) ) ) return; else what_rule++; } else what_rule += 10; } else what_rule += 10; r = what_rule - 0; mu_i.value((r % 1) + 4); r = r / 1; mu_msg_index.value((r % 10) + 0); r = r / 10; mu_k.unionassign(r % 4); r = r / 4; mu_j.unionassign(r % 4); r = r / 4; } } void Code(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_1_id mu_msg_index; mu_msg_index.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 4); r = r / 4; static mu_1_AgentId mu_j; mu_j.unionassign(r % 4); r = r / 4; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); { mu_1_Message& mu_outM = mu_int[mu_i].mu_messages[mu_msg_index]; mu_outM.mu_from_intruder = mu_true; mu_outM.mu_source = mu_j; mu_outM.mu_dest = mu_k; mu_net.multisetadd(mu_outM); } mu_int[mu_i].mu_messages.multisetremove(mu_msg_index); }; bool UnFair() { return FALSE; } }; /******************** RuleBase1 ********************/ class RuleBase1 { public: int Priority() { return 10; } char * Name(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; return tsprintf("intruder intercepts, i:%s, j:%s", mu_i.Name(), mu_j.Name()); } bool Condition(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } bool mu__boolexpr16; if (!(!((mu_net[mu_j].mu_source>=4 && mu_net[mu_j].mu_source<=4)))) mu__boolexpr16 = FALSE ; else { mu__boolexpr16 = (!(mu_net[mu_j].mu_from_intruder)) ; } return mu__boolexpr16; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 160; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; while (what_rule < 161 && mu_j.value()<1 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { bool mu__boolexpr17; if (!(!((mu_net[mu_j].mu_source>=4 && mu_net[mu_j].mu_source<=4)))) mu__boolexpr17 = FALSE ; else { mu__boolexpr17 = (!(mu_net[mu_j].mu_from_intruder)) ; } if (mu__boolexpr17) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 160; mu_i.value((r % 1) + 4); r = r / 1; mu_j.value((r % 1) + 0); r = r / 1; } } void Code(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 4); r = r / 1; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_temp("temp",0); { mu_1_Message& mu_msg = mu_net[mu_j]; if ( (mu_msg.mu_dest) == (mu_i) ) { } else { { mu_1__type_1& mu_messages = mu_int[mu_i].mu_messages; mu_temp = mu_msg; /*** begin multisetcount 2 declaration ***/ int mu__intexpr18 = 0; { mu_1__type_1_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_messages.valid[(int)mu_l].value()) { bool mu__boolexpr19; bool mu__boolexpr20; bool mu__boolexpr21; bool mu__boolexpr22; if (!((mu_messages[mu_l].mu_source) == (mu_temp.mu_source))) mu__boolexpr22 = FALSE ; else { mu__boolexpr22 = ((mu_messages[mu_l].mu_dest) == (mu_temp.mu_dest)) ; } if (!(mu__boolexpr22)) mu__boolexpr21 = FALSE ; else { mu__boolexpr21 = ((mu_messages[mu_l].mu_mType) == (mu_temp.mu_mType)) ; } if (!(mu__boolexpr21)) mu__boolexpr20 = FALSE ; else { bool mu__boolexpr23; if (!((mu_messages[mu_l].mu_mType) == (mu_MOBIKE_1))) mu__boolexpr23 = TRUE ; else { mu__boolexpr23 = ((mu_messages[mu_l].mu_nonce_i) == (mu_temp.mu_nonce_i)) ; } mu__boolexpr20 = (mu__boolexpr23) ; } if (!(mu__boolexpr20)) mu__boolexpr19 = FALSE ; else { bool mu__boolexpr24; if (!((mu_messages[mu_l].mu_mType) == (mu_MOBIKE_2))) mu__boolexpr24 = TRUE ; else { mu__boolexpr24 = ((mu_messages[mu_l].mu_nonce_r) == (mu_temp.mu_nonce_r)) ; } mu__boolexpr19 = (mu__boolexpr24) ; } if ( mu__boolexpr19 ) mu__intexpr18++; } if (mu_l == 10-1) break; } } /*** end multisetcount 2 declaration ***/ if ( (mu__intexpr18) == (0) ) { mu_int[mu_i].mu_messages.multisetadd(mu_temp); cout << "Intruder picking up message "; mu_temp.mu_mType.print(); } } } mu_net.multisetremove(mu_j); } }; bool UnFair() { return FALSE; } }; /******************** RuleBase2 ********************/ class RuleBase2 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_SpiId mu_j; mu_j.value((r % 11) + 0); r = r / 11; return tsprintf("responder sub process, i:%s, j:%s", mu_i.Name(), mu_j.Name()); } bool Condition(unsigned r) { static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_SpiId mu_j; mu_j.value((r % 11) + 0); r = r / 11; bool mu__boolexpr25; bool mu__boolexpr26; if (!((mu_responder_spi[mu_j].mu_in_use) == (mu_true))) mu__boolexpr26 = FALSE ; else { mu__boolexpr26 = ((mu_responder_spi[mu_j].mu_state) == (mu_MOBIKE_7)) ; } if (!(mu__boolexpr26)) mu__boolexpr25 = FALSE ; else { /*** begin multisetcount 1 declaration ***/ int mu__intexpr27 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr27++; } if (mu_l == 1-1) break; } } /*** end multisetcount 1 declaration ***/ mu__boolexpr25 = ((mu__intexpr27) < (mu_NetworkSize)) ; } return mu__boolexpr25; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 161; static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_SpiId mu_j; mu_j.value((r % 11) + 0); r = r / 11; while (what_rule < 172 ) { if ( ( TRUE ) ) { bool mu__boolexpr28; bool mu__boolexpr29; if (!((mu_responder_spi[mu_j].mu_in_use) == (mu_true))) mu__boolexpr29 = FALSE ; else { mu__boolexpr29 = ((mu_responder_spi[mu_j].mu_state) == (mu_MOBIKE_7)) ; } if (!(mu__boolexpr29)) mu__boolexpr28 = FALSE ; else { /*** begin multisetcount 1 declaration ***/ int mu__intexpr30 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr30++; } if (mu_l == 1-1) break; } } /*** end multisetcount 1 declaration ***/ mu__boolexpr28 = ((mu__intexpr30) < (mu_NetworkSize)) ; } if (mu__boolexpr28) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 161; mu_i.value((r % 1) + 3); r = r / 1; mu_j.value((r % 11) + 0); r = r / 11; } } void Code(unsigned r) { static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_SpiId mu_j; mu_j.value((r % 11) + 0); r = r / 11; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",356); mu_spi.undefine(); mu_outM.undefine(); mu_spi = mu_responder_spi[mu_j]; mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_mType = mu_MOBIKE_7; mu_outM.mu_init_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_spi_id; mu_outM.mu_cookie = mu_new_random( ); mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_cookie = mu_outM.mu_cookie; mu_spi.mu_msgid = mu_outM.mu_msgid; mu_spi.mu_state = mu_MOBIKE_8; mu_responder_spi[mu_j] = mu_spi; }; bool UnFair() { return FALSE; } }; /******************** RuleBase3 ********************/ class RuleBase3 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; return tsprintf("responder main process, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } return (mu_net[mu_j].mu_dest) == (mu_i); } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 172; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; while (what_rule < 173 && mu_j.value()<1 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { if ((mu_net[mu_j].mu_dest) == (mu_i)) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 172; mu_j.value((r % 1) + 0); r = r / 1; mu_i.value((r % 1) + 3); r = r / 1; } } void Code(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_ResponderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Message mu_inM("inM",356); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",712); /*** Variable declaration ***/ mu_1_SpiId mu_spi_id("spi_id",966); /*** Variable declaration ***/ mu_1_Auth mu_auth("auth",970); /*** Variable declaration ***/ mu_0_boolean mu_continue_MOBIKE("continue_MOBIKE",1098); mu_inM.undefine(); mu_spi.undefine(); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_continue_MOBIKE = mu_true; mu_spi_id = mu_inM.mu_resp_spi; mu_spi = mu_responder_spi[mu_spi_id]; switch ((int) mu_inM.mu_mType) { case mu_MOBIKE_1: mu_spi = mu_responder_new_spi( ); mu_spi.mu_peer = mu_inM.mu_source; mu_spi.mu_peer_spi_id = mu_inM.mu_init_spi; mu_spi.mu_peer_ke = mu_inM.mu_ke_i; mu_spi.mu_peer_nonce = mu_inM.mu_nonce_i; mu_spi.mu_peer_msgid = 0; mu_spi.mu_exponent = mu_new_random( ); if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "responder: mismatch of msgid\n"; } else { mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_mType = mu_MOBIKE_2; mu_outM.mu_ke_r = mu_make_ke( mu_spi.mu_exponent ); mu_outM.mu_nonce_r = mu_new_random( ); mu_outM.mu_init_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_spi_id; mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = 0; mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_session_key = mu_make_session_key( mu_inM.mu_ke_i, mu_spi.mu_exponent ); cout << "Responder: session_key: "; mu_spi.mu_session_key.print(); mu_spi.mu_msgid = mu_outM.mu_msgid; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_nonce = mu_outM.mu_nonce_r; mu_spi.mu_ke = mu_outM.mu_ke_r; mu_spi.mu_state = mu_MOBIKE_3; mu_responder_spi[mu_spi.mu_spi_id] = mu_spi; } break; case mu_MOBIKE_3: bool mu__boolexpr31; bool mu__boolexpr32; bool mu__boolexpr33; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr33 = FALSE ; else { mu__boolexpr33 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr33)) mu__boolexpr32 = FALSE ; else { mu__boolexpr32 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_init_spi)) ; } if (!(mu__boolexpr32)) mu__boolexpr31 = FALSE ; else { mu__boolexpr31 = ((mu_spi.mu_state) == (mu_MOBIKE_3)) ; } if ( mu__boolexpr31 ) { if ( mu_NO_NATS_ALLOWED ) { if ( (mu_inM.mu_no_nats_allowed_source) != (mu_inM.mu_source) ) { cout << "NO_NATS_ALLOWED, but the MOBIKE_3's "; cout << "source address changed\n"; mu_continue_MOBIKE = mu_false; } if ( (mu_inM.mu_no_nats_allowed_dest) != (mu_inM.mu_dest) ) { cout << "NO_NATS_ALLOWED, but the MOBIKE_3's "; cout << "dest address changed\n"; mu_continue_MOBIKE = mu_false; } } if ( (mu_inM.mu_id_i) != (mu_spi.mu_peer) ) { cout << "responder: incorrect id_i\n"; mu_continue_MOBIKE = mu_false; } if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "responder: mismatch of msgid\n"; mu_continue_MOBIKE = mu_false; } mu_auth.undefine(); mu_auth = mu_inM.mu_auth; bool mu__boolexpr34; bool mu__boolexpr35; bool mu__boolexpr36; bool mu__boolexpr37; bool mu__boolexpr38; bool mu__boolexpr39; if ((mu_auth.mu_ke.mu_random) != (mu_spi.mu_peer_ke.mu_random)) mu__boolexpr39 = TRUE ; else { mu__boolexpr39 = ((mu_auth.mu_nonce) != (mu_spi.mu_peer_nonce)) ; } if (mu__boolexpr39) mu__boolexpr38 = TRUE ; else { mu__boolexpr38 = ((mu_auth.mu_spi) != (mu_spi.mu_peer_spi_id)) ; } if (mu__boolexpr38) mu__boolexpr37 = TRUE ; else { mu__boolexpr37 = ((mu_auth.mu_peer_nonce) != (mu_spi.mu_nonce)) ; } if (mu__boolexpr37) mu__boolexpr36 = TRUE ; else { mu__boolexpr36 = ((mu_auth.mu_id_p) != (mu_spi.mu_peer)) ; } if (mu__boolexpr36) mu__boolexpr35 = TRUE ; else { mu__boolexpr35 = ((mu_auth.mu_msgid) != ((mu_spi.mu_peer_msgid) - (1))) ; } if (mu__boolexpr35) mu__boolexpr34 = TRUE ; else { mu__boolexpr34 = ((mu_auth.mu_shared_secret) != (mu_SharedSecret)) ; } if ( mu__boolexpr34 ) { cout << "responder: invalid auth payload\n"; mu_continue_MOBIKE = mu_false; } if ( mu_continue_MOBIKE ) { mu_auth.undefine(); mu_auth.mu_ke = mu_spi.mu_ke; mu_auth.mu_nonce = mu_spi.mu_nonce; mu_auth.mu_peer_nonce = mu_spi.mu_peer_nonce; mu_auth.mu_spi = mu_spi.mu_spi_id; mu_auth.mu_id_p = mu_i; mu_auth.mu_shared_secret = mu_SharedSecret; mu_auth.mu_msgid = mu_spi.mu_msgid; mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_mType = mu_MOBIKE_4; mu_outM.mu_init_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_spi_id; mu_outM.mu_id_r = mu_i; mu_outM.mu_auth = mu_auth; mu_outM.mu_mobike_s = mu_true; mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_msgid = mu_outM.mu_msgid; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_state = mu_MOBIKE_5; mu_responder_spi[mu_spi.mu_spi_id] = mu_spi; } } else { cout << "responder received unsolicited MOBIKE_3 message\n"; } break; case mu_MOBIKE_5: bool mu__boolexpr40; bool mu__boolexpr41; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr41 = FALSE ; else { mu__boolexpr41 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_init_spi)) ; } if (!(mu__boolexpr41)) mu__boolexpr40 = FALSE ; else { mu__boolexpr40 = ((mu_spi.mu_state) == (mu_MOBIKE_5)) ; } if ( mu__boolexpr40 ) { if ( mu_NO_NATS_ALLOWED ) { if ( (mu_inM.mu_no_nats_allowed_source) != (mu_inM.mu_source) ) { cout << "NO_NATS_ALLOWED, but the MOBIKE_5's "; cout << "source address changed\n"; mu_continue_MOBIKE = mu_false; } if ( (mu_inM.mu_no_nats_allowed_dest) != (mu_inM.mu_dest) ) { cout << "NO_NATS_ALLOWED, but the MOBIKE_5's "; cout << "dest address changed\n"; mu_continue_MOBIKE = mu_false; } } if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "responder: mismatch of msgid\n"; mu_continue_MOBIKE = mu_false; } if ( mu_continue_MOBIKE ) { mu_spi.mu_peer = mu_inM.mu_source; mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_mType = mu_MOBIKE_6; mu_outM.mu_init_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_spi_id; mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_msgid = mu_outM.mu_msgid; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_state = mu_MOBIKE_7; mu_responder_spi[mu_spi.mu_spi_id] = mu_spi; } } else { cout << "responder received unsolicited MOBIKE_5 message\n"; } break; case mu_MOBIKE_8: bool mu__boolexpr42; bool mu__boolexpr43; bool mu__boolexpr44; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr44 = FALSE ; else { mu__boolexpr44 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr44)) mu__boolexpr43 = FALSE ; else { mu__boolexpr43 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_init_spi)) ; } if (!(mu__boolexpr43)) mu__boolexpr42 = FALSE ; else { mu__boolexpr42 = ((mu_spi.mu_state) == (mu_MOBIKE_8)) ; } if ( mu__boolexpr42 ) { if ( !((mu_inM.mu_cookie) == (mu_spi.mu_cookie)) ) Error.Error("Assertion failed: mobike.m, line 759."); if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "responder: mismatch of msgid\n"; } else { cout << "Cookie received, we're done\n"; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_responder_spi[mu_spi.mu_spi_id].mu_state = mu_MOBIKE_DONE; } } else { cout << "responder received unsolicited MOBIKE_8 message\n"; } break; } }; bool UnFair() { return FALSE; } }; /******************** RuleBase4 ********************/ class RuleBase4 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; return tsprintf("initiator_p main process, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } return (mu_net[mu_j].mu_dest) == (mu_i); } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 173; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; while (what_rule < 174 && mu_j.value()<1 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { if ((mu_net[mu_j].mu_dest) == (mu_i)) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 173; mu_j.value((r % 1) + 0); r = r / 1; mu_i.value((r % 1) + 2); r = r / 1; } } void Code(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Message mu_inM("inM",356); /*** Variable declaration ***/ mu_1_SpiId mu_spi_id("spi_id",712); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",716); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_spi_id = mu_inM.mu_init_spi; mu_spi = mu_initiator_spi[mu_spi_id]; if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "initiator: mismatch of msgid\n"; } else { switch ((int) mu_inM.mu_mType) { case mu_MOBIKE_6: bool mu__boolexpr45; bool mu__boolexpr46; bool mu__boolexpr47; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr47 = FALSE ; else { mu__boolexpr47 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr47)) mu__boolexpr46 = FALSE ; else { mu__boolexpr46 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_resp_spi)) ; } if (!(mu__boolexpr46)) mu__boolexpr45 = FALSE ; else { mu__boolexpr45 = ((mu_spi.mu_state) == (mu_MOBIKE_6)) ; } if ( mu__boolexpr45 ) { cout << "initiator received expected MOBIKE_6 message\n"; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_state = mu_MOBIKE_7; mu_initiator_spi[mu_spi_id] = mu_spi; } else { cout << "initiator received unsolicited MOBIKE_6 message\n"; } break; case mu_MOBIKE_7: bool mu__boolexpr48; bool mu__boolexpr49; bool mu__boolexpr50; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr50 = FALSE ; else { mu__boolexpr50 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr50)) mu__boolexpr49 = FALSE ; else { mu__boolexpr49 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_resp_spi)) ; } if (!(mu__boolexpr49)) mu__boolexpr48 = FALSE ; else { mu__boolexpr48 = ((mu_spi.mu_state) == (mu_MOBIKE_7)) ; } if ( mu__boolexpr48 ) { cout << "initiator received MOBIKE_7 message\n"; mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_inM.mu_source; mu_outM.mu_init_spi = mu_spi.mu_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_mType = mu_MOBIKE_8; mu_outM.mu_cookie = mu_inM.mu_cookie; mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_msgid = mu_outM.mu_msgid; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_state = mu_MOBIKE_DONE; mu_initiator_spi[mu_spi_id] = mu_spi; } else { cout << "initiator received unsolicited MOBIKE_7 message\n"; } break; } } }; bool UnFair() { return FALSE; } }; /******************** RuleBase5 ********************/ class RuleBase5 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; static mu_1_SpiId mu_spi_id; mu_spi_id.value((r % 11) + 0); r = r / 11; return tsprintf("initiator address change (step 6), i:%s, spi_id:%s", mu_i.Name(), mu_spi_id.Name()); } bool Condition(unsigned r) { static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; static mu_1_SpiId mu_spi_id; mu_spi_id.value((r % 11) + 0); r = r / 11; bool mu__boolexpr51; if (!((mu_initiator_spi[mu_spi_id].mu_in_use) == (mu_true))) mu__boolexpr51 = FALSE ; else { mu__boolexpr51 = ((mu_initiator_spi[mu_spi_id].mu_state) == (mu_MOBIKE_ADDR_CHANGE)) ; } return mu__boolexpr51; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 174; static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; static mu_1_SpiId mu_spi_id; mu_spi_id.value((r % 11) + 0); r = r / 11; while (what_rule < 185 ) { if ( ( TRUE ) ) { bool mu__boolexpr52; if (!((mu_initiator_spi[mu_spi_id].mu_in_use) == (mu_true))) mu__boolexpr52 = FALSE ; else { mu__boolexpr52 = ((mu_initiator_spi[mu_spi_id].mu_state) == (mu_MOBIKE_ADDR_CHANGE)) ; } if (mu__boolexpr52) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 174; mu_i.value((r % 1) + 2); r = r / 1; mu_spi_id.value((r % 11) + 0); r = r / 11; } } void Code(unsigned r) { static mu_1_InitiatorIdP mu_i; mu_i.value((r % 1) + 2); r = r / 1; static mu_1_SpiId mu_spi_id; mu_spi_id.value((r % 11) + 0); r = r / 11; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",356); mu_outM.undefine(); mu_spi.undefine(); mu_spi = mu_initiator_spi[mu_spi_id]; cout << "received addr change message\n"; mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_init_spi = mu_spi.mu_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_mType = mu_MOBIKE_5; mu_outM.mu_from_intruder = mu_false; if ( mu_NO_NATS_ALLOWED ) { mu_outM.mu_no_nats_allowed_source = mu_outM.mu_source; mu_outM.mu_no_nats_allowed_dest = mu_outM.mu_dest; } mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_initiator_spi[mu_spi_id].mu_msgid = mu_outM.mu_msgid; mu_initiator_spi[mu_spi_id].mu_state = mu_MOBIKE_6; }; bool UnFair() { return FALSE; } }; /******************** RuleBase6 ********************/ class RuleBase6 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; return tsprintf("initiator main process, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } return (mu_net[mu_j].mu_dest) == (mu_i); } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 185; static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; while (what_rule < 186 && mu_j.value()<1 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { if ((mu_net[mu_j].mu_dest) == (mu_i)) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 185; mu_j.value((r % 1) + 0); r = r / 1; mu_i.value((r % 1) + 1); r = r / 1; } } void Code(unsigned r) { static mu_1__type_2_id mu_j; mu_j.value((r % 1) + 0); r = r / 1; static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Message mu_inM("inM",356); /*** Variable declaration ***/ mu_1_SpiId mu_spi_id("spi_id",712); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",716); /*** Variable declaration ***/ mu_1_Auth mu_auth("auth",970); /*** Variable declaration ***/ mu_0_boolean mu_continue_MOBIKE("continue_MOBIKE",1098); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_spi_id = mu_inM.mu_init_spi; mu_spi = mu_initiator_spi[mu_spi_id]; mu_continue_MOBIKE = mu_true; switch ((int) mu_inM.mu_mType) { case mu_MOBIKE_2: bool mu__boolexpr53; bool mu__boolexpr54; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr54 = FALSE ; else { mu__boolexpr54 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr54)) mu__boolexpr53 = FALSE ; else { mu__boolexpr53 = ((mu_spi.mu_state) == (mu_MOBIKE_2)) ; } if ( mu__boolexpr53 ) { if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "initiator: mismatch of msgid\n"; } else { mu_spi.mu_state = mu_MOBIKE_4; mu_spi.mu_peer_spi_id = mu_inM.mu_resp_spi; mu_spi.mu_peer_nonce = mu_inM.mu_nonce_r; mu_spi.mu_peer_ke = mu_inM.mu_ke_r; mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_session_key = mu_make_session_key( mu_inM.mu_ke_r, mu_spi.mu_exponent ); cout << "Initiator: session_key: "; mu_spi.mu_session_key.print(); mu_auth.undefine(); mu_auth.mu_msgid = mu_spi.mu_msgid; mu_auth.mu_ke = mu_spi.mu_ke; mu_auth.mu_nonce = mu_spi.mu_nonce; mu_auth.mu_spi = mu_spi.mu_spi_id; mu_auth.mu_peer_nonce = mu_spi.mu_peer_nonce; mu_auth.mu_id_p = mu_i; mu_auth.mu_shared_secret = mu_SharedSecret; mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_spi.mu_peer; mu_outM.mu_mType = mu_MOBIKE_3; mu_outM.mu_msgid = (mu_spi.mu_msgid) + (1); if (mu_spi_id.isundefined()) mu_outM.mu_init_spi.undefine(); else mu_outM.mu_init_spi = mu_spi_id; mu_outM.mu_resp_spi = mu_spi.mu_peer_spi_id; mu_outM.mu_id_i = mu_i; mu_outM.mu_auth = mu_auth; if ( mu_NO_NATS_ALLOWED ) { mu_outM.mu_no_nats_allowed_source = mu_outM.mu_source; mu_outM.mu_no_nats_allowed_dest = mu_outM.mu_dest; } mu_outM.mu_mobike_s = mu_true; mu_outM.mu_from_intruder = mu_false; mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_msgid = mu_outM.mu_msgid; mu_initiator_spi[mu_spi_id] = mu_spi; } } else { cout << "initiator received unsolicited MOBIKE_2 message\n"; } break; case mu_MOBIKE_4: bool mu__boolexpr55; bool mu__boolexpr56; bool mu__boolexpr57; if (!((mu_spi.mu_in_use) == (mu_true))) mu__boolexpr57 = FALSE ; else { mu__boolexpr57 = ((mu_spi.mu_peer) == (mu_inM.mu_source)) ; } if (!(mu__boolexpr57)) mu__boolexpr56 = FALSE ; else { mu__boolexpr56 = ((mu_spi.mu_peer_spi_id) == (mu_inM.mu_resp_spi)) ; } if (!(mu__boolexpr56)) mu__boolexpr55 = FALSE ; else { mu__boolexpr55 = ((mu_spi.mu_state) == (mu_MOBIKE_4)) ; } if ( mu__boolexpr55 ) { if ( (mu_inM.mu_id_r) != (mu_spi.mu_peer) ) { cout << "initiator: incorrect id_r\n"; mu_continue_MOBIKE = mu_false; } if ( (mu_spi.mu_peer_msgid) != (mu_inM.mu_msgid) ) { cout << "initiator: mismatch of msgid\n"; mu_continue_MOBIKE = mu_false; } mu_auth.undefine(); mu_auth = mu_inM.mu_auth; bool mu__boolexpr58; bool mu__boolexpr59; bool mu__boolexpr60; bool mu__boolexpr61; bool mu__boolexpr62; bool mu__boolexpr63; if ((mu_auth.mu_ke.mu_random) != (mu_spi.mu_peer_ke.mu_random)) mu__boolexpr63 = TRUE ; else { mu__boolexpr63 = ((mu_auth.mu_nonce) != (mu_spi.mu_peer_nonce)) ; } if (mu__boolexpr63) mu__boolexpr62 = TRUE ; else { mu__boolexpr62 = ((mu_auth.mu_spi) != (mu_spi.mu_peer_spi_id)) ; } if (mu__boolexpr62) mu__boolexpr61 = TRUE ; else { mu__boolexpr61 = ((mu_auth.mu_peer_nonce) != (mu_spi.mu_nonce)) ; } if (mu__boolexpr61) mu__boolexpr60 = TRUE ; else { mu__boolexpr60 = ((mu_auth.mu_id_p) != (mu_spi.mu_peer)) ; } if (mu__boolexpr60) mu__boolexpr59 = TRUE ; else { mu__boolexpr59 = ((mu_auth.mu_shared_secret) != (mu_SharedSecret)) ; } if (mu__boolexpr59) mu__boolexpr58 = TRUE ; else { mu__boolexpr58 = ((mu_auth.mu_msgid) != ((mu_spi.mu_peer_msgid) - (1))) ; } if ( mu__boolexpr58 ) { cout << "initiator: invalid auth payload\n"; mu_continue_MOBIKE = mu_false; } if ( (mu_continue_MOBIKE) == (mu_true) ) { mu_spi.mu_peer_msgid = (mu_inM.mu_msgid) + (1); mu_spi.mu_state = mu_MOBIKE_ADDR_CHANGE; mu_initiator_spi[mu_spi_id] = mu_spi; } } else { cout << "initiator received unsolicited MOBIKE_4 message\n"; } break; } }; bool UnFair() { return FALSE; } }; /******************** RuleBase7 ********************/ class RuleBase7 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; static mu_1_ResponderId mu_j; mu_j.value((r % 1) + 3); r = r / 1; return tsprintf("initiator starts protocol (step 1), i:%s, j:%s", mu_i.Name(), mu_j.Name()); } bool Condition(unsigned r) { static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; static mu_1_ResponderId mu_j; mu_j.value((r % 1) + 3); r = r / 1; bool mu__boolexpr64; if (!((mu_initiator_num_spis) == (0))) mu__boolexpr64 = FALSE ; else { /*** begin multisetcount 0 declaration ***/ int mu__intexpr65 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr65++; } if (mu_l == 1-1) break; } } /*** end multisetcount 0 declaration ***/ mu__boolexpr64 = ((mu__intexpr65) < (mu_NetworkSize)) ; } return mu__boolexpr64; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 186; static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; static mu_1_ResponderId mu_j; mu_j.value((r % 1) + 3); r = r / 1; while (what_rule < 187 ) { if ( ( TRUE ) ) { bool mu__boolexpr66; if (!((mu_initiator_num_spis) == (0))) mu__boolexpr66 = FALSE ; else { /*** begin multisetcount 0 declaration ***/ int mu__intexpr67 = 0; { mu_1__type_2_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr67++; } if (mu_l == 1-1) break; } } /*** end multisetcount 0 declaration ***/ mu__boolexpr66 = ((mu__intexpr67) < (mu_NetworkSize)) ; } if (mu__boolexpr66) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 186; mu_i.value((r % 1) + 1); r = r / 1; mu_j.value((r % 1) + 3); r = r / 1; } } void Code(unsigned r) { static mu_1_InitiatorId mu_i; mu_i.value((r % 1) + 1); r = r / 1; static mu_1_ResponderId mu_j; mu_j.value((r % 1) + 3); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Spi mu_spi("spi",356); mu_spi.undefine(); mu_spi = mu_initiator_new_spi( ); cout << "pas initiator_new_spi stuff\n"; mu_spi.mu_peer = mu_j; mu_spi.mu_exponent = mu_new_random( ); mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_j; mu_outM.mu_init_spi = mu_spi.mu_spi_id; mu_outM.mu_resp_spi = 0; mu_outM.mu_mType = mu_MOBIKE_1; mu_outM.mu_ke_i = mu_make_ke( mu_spi.mu_exponent ); mu_outM.mu_nonce_i = mu_new_random( ); mu_outM.mu_from_intruder = mu_false; mu_outM.mu_msgid = 0; mu_outM.mu_session_key = mu_spi.mu_session_key; mu_net.multisetadd(mu_outM); mu_spi.mu_state = mu_MOBIKE_2; mu_spi.mu_peer_spi_id = 0; mu_spi.mu_nonce = mu_outM.mu_nonce_i; mu_spi.mu_ke = mu_outM.mu_ke_i; mu_spi.mu_msgid = mu_outM.mu_msgid; mu_initiator_spi[mu_spi.mu_spi_id] = mu_spi; }; bool UnFair() { return FALSE; } }; class NextStateGenerator { RuleBase0 R0; RuleBase1 R1; RuleBase2 R2; RuleBase3 R3; RuleBase4 R4; RuleBase5 R5; RuleBase6 R6; RuleBase7 R7; public: void SetNextEnabledRule(unsigned & what_rule) { category = CONDITION; if (what_rule<160) { R0.NextRule(what_rule); if (what_rule<160) return; } if (what_rule>=160 && what_rule<161) { R1.NextRule(what_rule); if (what_rule<161) return; } if (what_rule>=161 && what_rule<172) { R2.NextRule(what_rule); if (what_rule<172) return; } if (what_rule>=172 && what_rule<173) { R3.NextRule(what_rule); if (what_rule<173) return; } if (what_rule>=173 && what_rule<174) { R4.NextRule(what_rule); if (what_rule<174) return; } if (what_rule>=174 && what_rule<185) { R5.NextRule(what_rule); if (what_rule<185) return; } if (what_rule>=185 && what_rule<186) { R6.NextRule(what_rule); if (what_rule<186) return; } if (what_rule>=186 && what_rule<187) { R7.NextRule(what_rule); if (what_rule<187) return; } } bool Condition(unsigned r) { category = CONDITION; if (r<=159) return R0.Condition(r-0); if (r>=160 && r<=160) return R1.Condition(r-160); if (r>=161 && r<=171) return R2.Condition(r-161); if (r>=172 && r<=172) return R3.Condition(r-172); if (r>=173 && r<=173) return R4.Condition(r-173); if (r>=174 && r<=184) return R5.Condition(r-174); if (r>=185 && r<=185) return R6.Condition(r-185); if (r>=186 && r<=186) return R7.Condition(r-186); Error.Notrace("Internal: NextStateGenerator -- checking condition for nonexisting rule."); } void Code(unsigned r) { if (r<=159) { R0.Code(r-0); return; } if (r>=160 && r<=160) { R1.Code(r-160); return; } if (r>=161 && r<=171) { R2.Code(r-161); return; } if (r>=172 && r<=172) { R3.Code(r-172); return; } if (r>=173 && r<=173) { R4.Code(r-173); return; } if (r>=174 && r<=184) { R5.Code(r-174); return; } if (r>=185 && r<=185) { R6.Code(r-185); return; } if (r>=186 && r<=186) { R7.Code(r-186); return; } } int Priority(unsigned short r) { if (r<=159) { return R0.Priority(); } if (r>=160 && r<=160) { return R1.Priority(); } if (r>=161 && r<=171) { return R2.Priority(); } if (r>=172 && r<=172) { return R3.Priority(); } if (r>=173 && r<=173) { return R4.Priority(); } if (r>=174 && r<=184) { return R5.Priority(); } if (r>=185 && r<=185) { return R6.Priority(); } if (r>=186 && r<=186) { return R7.Priority(); } } char * Name(unsigned r) { if (r<=159) return R0.Name(r-0); if (r>=160 && r<=160) return R1.Name(r-160); if (r>=161 && r<=171) return R2.Name(r-161); if (r>=172 && r<=172) return R3.Name(r-172); if (r>=173 && r<=173) return R4.Name(r-173); if (r>=174 && r<=184) return R5.Name(r-174); if (r>=185 && r<=185) return R6.Name(r-185); if (r>=186 && r<=186) return R7.Name(r-186); return NULL; } }; const unsigned numrules = 187; /******************** parameter ********************/ #define RULES_IN_WORLD 187 /******************** Startstate records ********************/ /******************** StartStateBase0 ********************/ class StartStateBase0 { public: char * Name(unsigned short r) { return tsprintf("Startstate 0"); } void Code(unsigned short r) { mu_next_random = 7; mu_initiator_num_spis = 0; mu_initiator_spi.undefine(); { for(int mu_i = 0; mu_i <= 10; mu_i++) { mu_initiator_spi[mu_i].mu_ke.mu_random = 0; mu_initiator_spi[mu_i].mu_peer_ke.mu_random = 0; mu_initiator_spi[mu_i].mu_session_key.mu_random = 0; mu_initiator_spi[mu_i].mu_msgid = 0; mu_initiator_spi[mu_i].mu_peer_msgid = 0; mu_initiator_spi[mu_i].mu_nonce = 0; mu_initiator_spi[mu_i].mu_peer_nonce = 0; mu_initiator_spi[mu_i].mu_cookie = 0; mu_initiator_spi[mu_i].mu_exponent = 0; mu_initiator_spi[mu_i].mu_spi_id = mu_i; mu_initiator_spi[mu_i].mu_in_use = mu_false; }; }; mu_responder_spi.undefine(); { for(int mu_i = 0; mu_i <= 10; mu_i++) { mu_responder_spi[mu_i].mu_ke.mu_random = 0; mu_responder_spi[mu_i].mu_peer_ke.mu_random = 0; mu_responder_spi[mu_i].mu_session_key.mu_random = 0; mu_responder_spi[mu_i].mu_msgid = 0; mu_responder_spi[mu_i].mu_peer_msgid = 0; mu_responder_spi[mu_i].mu_nonce = 0; mu_responder_spi[mu_i].mu_peer_nonce = 0; mu_responder_spi[mu_i].mu_cookie = 0; mu_responder_spi[mu_i].mu_exponent = 0; mu_responder_spi[mu_i].mu_spi_id = mu_i; mu_responder_spi[mu_i].mu_in_use = mu_false; }; }; mu_net.undefine(); }; bool UnFair() { return FALSE; } }; class StartStateGenerator { StartStateBase0 S0; public: void Code(unsigned short r) { if (r<=0) { S0.Code(r-0); return; } } char * Name(unsigned short r) { if (r<=0) return S0.Name(r-0); return NULL; } }; unsigned short StartStateManager::numstartstates = 1; /******************** Invariant records ********************/ int mu__invariant_68() // Invariant "responder and initiator have same session key" { bool mu__quant69; mu__quant69 = TRUE; { for(int mu_i = 3; mu_i <= 3; mu_i++) { bool mu__quant70; mu__quant70 = TRUE; { for(int mu_j = 0; mu_j <= 10; mu_j++) { bool mu__boolexpr71; bool mu__boolexpr72; bool mu__boolexpr73; if (!((mu_responder_spi[mu_j].mu_in_use) == (mu_true))) mu__boolexpr73 = FALSE ; else { mu__boolexpr73 = ((mu_responder_spi[mu_j].mu_state) == (mu_MOBIKE_DONE)) ; } if (!(mu__boolexpr73)) mu__boolexpr72 = FALSE ; else { mu__boolexpr72 = ((mu_responder_spi[mu_j].mu_peer>=2 && mu_responder_spi[mu_j].mu_peer<=2)) ; } if (!(mu__boolexpr72)) mu__boolexpr71 = TRUE ; else { bool mu__boolexpr74; if (!((mu_initiator_spi[mu_responder_spi[mu_j].mu_peer_spi_id].mu_in_use) == (mu_true))) mu__boolexpr74 = FALSE ; else { mu__boolexpr74 = ((mu_initiator_spi[mu_responder_spi[mu_j].mu_peer_spi_id].mu_session_key.mu_random) == (mu_responder_spi[mu_j].mu_session_key.mu_random)) ; } mu__boolexpr71 = (mu__boolexpr74) ; } if ( !(mu__boolexpr71) ) { mu__quant70 = FALSE; break; } }; }; if ( !(mu__quant70) ) { mu__quant69 = FALSE; break; } }; }; return mu__quant69; }; bool mu__condition_75() // Condition for Rule "responder and initiator have same session key" { return mu__invariant_68( ); } /**** end rule declaration ****/ int mu__invariant_76() // Invariant "initiator correctly authenticated" { bool mu__quant77; mu__quant77 = TRUE; { for(int mu_i = 3; mu_i <= 3; mu_i++) { bool mu__quant78; mu__quant78 = TRUE; { for(int mu_j = 0; mu_j <= 10; mu_j++) { bool mu__boolexpr79; bool mu__boolexpr80; bool mu__boolexpr81; if (!((mu_responder_spi[mu_j].mu_in_use) == (mu_true))) mu__boolexpr81 = FALSE ; else { mu__boolexpr81 = ((mu_responder_spi[mu_j].mu_state) == (mu_MOBIKE_DONE)) ; } if (!(mu__boolexpr81)) mu__boolexpr80 = FALSE ; else { mu__boolexpr80 = ((mu_responder_spi[mu_j].mu_peer>=2 && mu_responder_spi[mu_j].mu_peer<=2)) ; } if (!(mu__boolexpr80)) mu__boolexpr79 = TRUE ; else { bool mu__boolexpr82; bool mu__boolexpr83; if (!((mu_initiator_spi[mu_responder_spi[mu_j].mu_peer_spi_id].mu_in_use) == (mu_true))) mu__boolexpr83 = FALSE ; else { mu__boolexpr83 = ((mu_initiator_spi[mu_responder_spi[mu_j].mu_peer_spi_id].mu_peer) == (mu_i)) ; } if (!(mu__boolexpr83)) mu__boolexpr82 = FALSE ; else { mu__boolexpr82 = ((mu_initiator_spi[mu_responder_spi[mu_j].mu_peer_spi_id].mu_state) == (mu_MOBIKE_DONE)) ; } mu__boolexpr79 = (mu__boolexpr82) ; } if ( !(mu__boolexpr79) ) { mu__quant78 = FALSE; break; } }; }; if ( !(mu__quant78) ) { mu__quant77 = FALSE; break; } }; }; return mu__quant77; }; bool mu__condition_84() // Condition for Rule "initiator correctly authenticated" { return mu__invariant_76( ); } /**** end rule declaration ****/ int mu__invariant_85() // Invariant "responder correctly authenticated" { bool mu__quant86; mu__quant86 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant87; mu__quant87 = TRUE; { for(int mu_j = 0; mu_j <= 10; mu_j++) { bool mu__boolexpr88; bool mu__boolexpr89; bool mu__boolexpr90; if (!((mu_initiator_spi[mu_j].mu_in_use) == (mu_true))) mu__boolexpr90 = FALSE ; else { mu__boolexpr90 = ((mu_initiator_spi[mu_j].mu_state) == (mu_MOBIKE_DONE)) ; } if (!(mu__boolexpr90)) mu__boolexpr89 = FALSE ; else { mu__boolexpr89 = ((mu_initiator_spi[mu_j].mu_peer>=3 && mu_initiator_spi[mu_j].mu_peer<=3)) ; } if (!(mu__boolexpr89)) mu__boolexpr88 = TRUE ; else { bool mu__boolexpr91; bool mu__boolexpr92; if (!((mu_responder_spi[mu_initiator_spi[mu_j].mu_peer_spi_id].mu_in_use) == (mu_true))) mu__boolexpr92 = FALSE ; else { mu__boolexpr92 = ((mu_responder_spi[mu_initiator_spi[mu_j].mu_peer_spi_id].mu_peer) == (mu_i)) ; } if (!(mu__boolexpr92)) mu__boolexpr91 = FALSE ; else { bool mu__boolexpr93; if ((mu_responder_spi[mu_initiator_spi[mu_j].mu_peer_spi_id].mu_state) == (mu_MOBIKE_DONE)) mu__boolexpr93 = TRUE ; else { mu__boolexpr93 = ((mu_responder_spi[mu_initiator_spi[mu_j].mu_peer_spi_id].mu_state) == (mu_MOBIKE_8)) ; } mu__boolexpr91 = (mu__boolexpr93) ; } mu__boolexpr88 = (mu__boolexpr91) ; } if ( !(mu__boolexpr88) ) { mu__quant87 = FALSE; break; } }; }; if ( !(mu__quant87) ) { mu__quant86 = FALSE; break; } }; }; return mu__quant86; }; bool mu__condition_94() // Condition for Rule "responder correctly authenticated" { return mu__invariant_85( ); } /**** end rule declaration ****/ const rulerec invariants[] = { {"responder correctly authenticated", &mu__condition_94, NULL, FALSE}, {"initiator correctly authenticated", &mu__condition_84, NULL, FALSE}, {"responder and initiator have same session key", &mu__condition_75, NULL, FALSE}, }; const unsigned short numinvariants = 3; /******************/ bool mu__true_live() { return TRUE; } /******************/ /******************** Liveness records ********************/ const liverec livenesses[] = { { NULL, NULL, NULL, NULL, E }}; const unsigned short numlivenesses = 0; /******************** Fairstates records ********************/ const rulerec fairnesses[] = { { NULL, NULL, NULL, FALSE }}; const unsigned short numfairnesses = 0; /******************** Normal/Canonicalization for scalarset ********************/ /* next_random:NoScalarset initiator_spi:NoScalarset responder_spi:NoScalarset initiator_num_spis:NoScalarset net:Complex int:Complex */ /******************** Code for symmetry ********************/ /******************** Permutation Set Class ********************/ class PermSet { public: // book keeping enum PresentationType {Simple, Explicit}; PresentationType Presentation; void ResetToSimple(); void ResetToExplicit(); void SimpleToExplicit(); void SimpleToOne(); bool NextPermutation(); void Print_in_size() { int ret=0; for (int i=0; isym_alg.mode == argsym_alg::Exhaustive_Fast_Canonicalize) { /******************** declaration of class variables ********************/ in = new bool[1]; // Set perm and revperm // setting up combination of permutations // for different scalarset int carry; size = 1; count = 1; for (i=0; i<1; i++) { carry = 1; in[i]= TRUE; } } else { /******************** declaration of class variables ********************/ in = new bool[1]; in[0] = TRUE; } } void PermSet::ResetToSimple() { int i; AlreadyOnlyOneRemain = FALSE; Presentation = Simple; } void PermSet::ResetToExplicit() { for (int i=0; i<1; i++) in[i] = TRUE; Presentation = Explicit; } void PermSet::SimpleToExplicit() { int i,j,k; int start, class_size; // Setup range for mapping // To be In or not to be // setup explicit representation // Set perm and revperm for (i=0; i<1; i++) { in[i] = TRUE; } Presentation = Explicit; if (args->test_parameter1.value==0) Print_in_size(); } void PermSet::SimpleToOne() { int i,j,k; int class_size; int start; // Setup range for mapping Presentation = Explicit; } bool PermSet::NextPermutation() { bool nexted = FALSE; int start, end; int class_size; int temp; int j,k; // algorithm // for each class // if forall in the same class reverse_sorted, // { sort again; goto next class } // else // { // nexted = TRUE; // for (j from l to r) // if (for all j+ are reversed sorted) // { // swap j, j+1 // sort all j+ again // break; // } // } if (!nexted) return FALSE; return TRUE; } /******************** Symmetry Class ********************/ class SymmetryClass { PermSet Perm; bool BestInitialized; state BestPermutedState; // utilities void SetBestResult(int i, state* temp); void ResetBestResult() {BestInitialized = FALSE;}; public: // initializer SymmetryClass() : Perm(), BestInitialized(FALSE) {}; ~SymmetryClass() {}; void Normalize(state* s); void Exhaustive_Fast_Canonicalize(state *s); void Heuristic_Fast_Canonicalize(state *s); void Heuristic_Small_Mem_Canonicalize(state *s); void Heuristic_Fast_Normalize(state *s); void MultisetSort(state* s); }; /******************** Symmetry Class Members ********************/ void SymmetryClass::MultisetSort(state* s) { mu_next_random.MultisetSort(); mu_initiator_spi.MultisetSort(); mu_responder_spi.MultisetSort(); mu_initiator_num_spis.MultisetSort(); mu_net.MultisetSort(); mu_int.MultisetSort(); } void SymmetryClass::Normalize(state* s) { switch (args->sym_alg.mode) { case argsym_alg::Exhaustive_Fast_Canonicalize: Exhaustive_Fast_Canonicalize(s); break; case argsym_alg::Heuristic_Fast_Canonicalize: Heuristic_Fast_Canonicalize(s); break; case argsym_alg::Heuristic_Small_Mem_Canonicalize: Heuristic_Small_Mem_Canonicalize(s); break; case argsym_alg::Heuristic_Fast_Normalize: Heuristic_Fast_Normalize(s); break; default: Heuristic_Fast_Canonicalize(s); } } /******************** Permute and Canonicalize function for different types ********************/ void mu_1_InitiatorId::Permute(PermSet& Perm, int i) {} void mu_1_InitiatorId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_InitiatorId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_InitiatorId::SimpleLimit(PermSet& Perm) {} void mu_1_InitiatorId::ArrayLimit(PermSet& Perm) {} void mu_1_InitiatorId::Limit(PermSet& Perm) {} void mu_1_InitiatorId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_InitiatorIdP::Permute(PermSet& Perm, int i) {} void mu_1_InitiatorIdP::SimpleCanonicalize(PermSet& Perm) {} void mu_1_InitiatorIdP::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_InitiatorIdP::SimpleLimit(PermSet& Perm) {} void mu_1_InitiatorIdP::ArrayLimit(PermSet& Perm) {} void mu_1_InitiatorIdP::Limit(PermSet& Perm) {} void mu_1_InitiatorIdP::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_ResponderId::Permute(PermSet& Perm, int i) {} void mu_1_ResponderId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_ResponderId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_ResponderId::SimpleLimit(PermSet& Perm) {} void mu_1_ResponderId::ArrayLimit(PermSet& Perm) {} void mu_1_ResponderId::Limit(PermSet& Perm) {} void mu_1_ResponderId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_IntruderId::Permute(PermSet& Perm, int i) {} void mu_1_IntruderId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_IntruderId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_IntruderId::SimpleLimit(PermSet& Perm) {} void mu_1_IntruderId::ArrayLimit(PermSet& Perm) {} void mu_1_IntruderId::Limit(PermSet& Perm) {} void mu_1_IntruderId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_SpiId::Permute(PermSet& Perm, int i) {}; void mu_1_SpiId::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_SpiId::Canonicalize(PermSet& Perm) {}; void mu_1_SpiId::SimpleLimit(PermSet& Perm) {}; void mu_1_SpiId::ArrayLimit(PermSet& Perm) {}; void mu_1_SpiId::Limit(PermSet& Perm) {}; void mu_1_SpiId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_Random::Permute(PermSet& Perm, int i) {}; void mu_1_Random::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_Random::Canonicalize(PermSet& Perm) {}; void mu_1_Random::SimpleLimit(PermSet& Perm) {}; void mu_1_Random::ArrayLimit(PermSet& Perm) {}; void mu_1_Random::Limit(PermSet& Perm) {}; void mu_1_Random::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_Integer::Permute(PermSet& Perm, int i) {}; void mu_1_Integer::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_Integer::Canonicalize(PermSet& Perm) {}; void mu_1_Integer::SimpleLimit(PermSet& Perm) {}; void mu_1_Integer::ArrayLimit(PermSet& Perm) {}; void mu_1_Integer::Limit(PermSet& Perm) {}; void mu_1_Integer::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_AgentId::Permute(PermSet& Perm, int i) { if (Perm.Presentation != PermSet::Explicit) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::SimpleCanonicalize(PermSet& Perm) { int i, class_number; if (Perm.Presentation != PermSet::Simple) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_AgentId::SimpleLimit(PermSet& Perm) { int i, class_number; if (Perm.Presentation != PermSet::Simple) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::ArrayLimit(PermSet& Perm) {} void mu_1_AgentId::Limit(PermSet& Perm) {} void mu_1_AgentId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for union type.\n"); }; void mu_1_MessageType::Permute(PermSet& Perm, int i) {}; void mu_1_MessageType::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_MessageType::Canonicalize(PermSet& Perm) {}; void mu_1_MessageType::SimpleLimit(PermSet& Perm) {}; void mu_1_MessageType::ArrayLimit(PermSet& Perm) {}; void mu_1_MessageType::Limit(PermSet& Perm) {}; void mu_1_MessageType::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for enum type.\n"); }; void mu_1_Ke::Permute(PermSet& Perm, int i) { }; void mu_1_Ke::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: Simple Canonicalization of Record with no scalarset variable\n"); }; void mu_1_Ke::Canonicalize(PermSet& Perm) { }; void mu_1_Ke::SimpleLimit(PermSet& Perm){} void mu_1_Ke::ArrayLimit(PermSet& Perm){} void mu_1_Ke::Limit(PermSet& Perm) { }; void mu_1_Ke::MultisetLimit(PermSet& Perm) { }; void mu_1_SessionKey::Permute(PermSet& Perm, int i) { }; void mu_1_SessionKey::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: Simple Canonicalization of Record with no scalarset variable\n"); }; void mu_1_SessionKey::Canonicalize(PermSet& Perm) { }; void mu_1_SessionKey::SimpleLimit(PermSet& Perm){} void mu_1_SessionKey::ArrayLimit(PermSet& Perm){} void mu_1_SessionKey::Limit(PermSet& Perm) { }; void mu_1_SessionKey::MultisetLimit(PermSet& Perm) { }; void mu_1_Spi::Permute(PermSet& Perm, int i) { }; void mu_1_Spi::SimpleCanonicalize(PermSet& Perm) { mu_peer.SimpleCanonicalize(Perm); }; void mu_1_Spi::Canonicalize(PermSet& Perm) { }; void mu_1_Spi::SimpleLimit(PermSet& Perm) { mu_peer.SimpleLimit(Perm); }; void mu_1_Spi::ArrayLimit(PermSet& Perm){} void mu_1_Spi::Limit(PermSet& Perm) { }; void mu_1_Spi::MultisetLimit(PermSet& Perm) { }; void mu_1_Auth::Permute(PermSet& Perm, int i) { }; void mu_1_Auth::SimpleCanonicalize(PermSet& Perm) { mu_id_p.SimpleCanonicalize(Perm); }; void mu_1_Auth::Canonicalize(PermSet& Perm) { }; void mu_1_Auth::SimpleLimit(PermSet& Perm) { mu_id_p.SimpleLimit(Perm); }; void mu_1_Auth::ArrayLimit(PermSet& Perm){} void mu_1_Auth::Limit(PermSet& Perm) { }; void mu_1_Auth::MultisetLimit(PermSet& Perm) { }; void mu_1_Message::Permute(PermSet& Perm, int i) { }; void mu_1_Message::SimpleCanonicalize(PermSet& Perm) { mu_source.SimpleCanonicalize(Perm); mu_dest.SimpleCanonicalize(Perm); mu_id_i.SimpleCanonicalize(Perm); mu_id_r.SimpleCanonicalize(Perm); mu_auth.SimpleCanonicalize(Perm); mu_upd_addr.SimpleCanonicalize(Perm); mu_no_nats_allowed_source.SimpleCanonicalize(Perm); mu_no_nats_allowed_dest.SimpleCanonicalize(Perm); }; void mu_1_Message::Canonicalize(PermSet& Perm) { }; void mu_1_Message::SimpleLimit(PermSet& Perm) { mu_source.SimpleLimit(Perm); mu_dest.SimpleLimit(Perm); mu_id_i.SimpleLimit(Perm); mu_id_r.SimpleLimit(Perm); mu_auth.SimpleLimit(Perm); mu_upd_addr.SimpleLimit(Perm); mu_no_nats_allowed_source.SimpleLimit(Perm); mu_no_nats_allowed_dest.SimpleLimit(Perm); }; void mu_1_Message::ArrayLimit(PermSet& Perm){} void mu_1_Message::Limit(PermSet& Perm) { }; void mu_1_Message::MultisetLimit(PermSet& Perm) { }; void mu_1__type_0::Permute(PermSet& Perm, int i) { static mu_1__type_0 temp("Permute_mu_1__type_0",-1); int j; for (j=0; j<4; j++) array[j].Permute(Perm, i); }; void mu_1__type_0::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: Simple Canonicalization of Scalarset Array\n"); }; void mu_1__type_0::Canonicalize(PermSet& Perm) { // indexes int i,j,k,z; // sorting static mu_0_boolean value[4]; int compare; // limit bool exists; bool split; // range mapping int start; int class_size; // canonicalization static mu_1__type_0 temp; } void mu_1__type_0::SimpleLimit(PermSet& Perm){} void mu_1__type_0::ArrayLimit(PermSet& Perm) { // indexes int i,j,k,z; // sorting int compare; static mu_0_boolean value[4]; // limit bool exists; bool split; } void mu_1__type_0::Limit(PermSet& Perm){} void mu_1__type_0::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset array.\n"); }; void mu_1__type_1::Permute(PermSet& Perm, int i) { static mu_1__type_1 temp("Permute_mu_1__type_1",-1); int j; for (j=0; j<10; j++) array[j].Permute(Perm, i); }; void mu_1__type_1::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: calling SimpleCanonicalize for a multiset.\n"); }; void mu_1__type_1::Canonicalize(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_1::SimpleLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_1::ArrayLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_1::Limit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_1::MultisetLimit(PermSet& Perm) { // indexes int i,j,k,z; // while guard bool while_guard, while_guard_temp; // sorting static mu_1_Message value[10]; // limit bool exists; bool split; int i0; int count_multisetindex, oldcount_multisetindex; bool pos_multisetindex[10][10]; bool goodset_multisetindex[10]; mu_1_Message temp; // compact for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (CompareWeight(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } // initializing pos array for (i=0; i0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } // initializing pos array for (i=0; isymmetry_reduction.value) { if ( args->sym_alg.mode == argsym_alg::Exhaustive_Fast_Canonicalize) { Perm.ResetToExplicit(); for (i=0; imultiset_reduction.value) mu_next_random.MultisetSort(); mu_initiator_spi.Permute(Perm,i); if (args->multiset_reduction.value) mu_initiator_spi.MultisetSort(); mu_responder_spi.Permute(Perm,i); if (args->multiset_reduction.value) mu_responder_spi.MultisetSort(); mu_initiator_num_spis.Permute(Perm,i); if (args->multiset_reduction.value) mu_initiator_num_spis.MultisetSort(); mu_net.Permute(Perm,i); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,i); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } } StateCopy(workingstate,&temp); return FALSE; } else { Perm.ResetToSimple(); Perm.SimpleToOne(); if (ns != workingstate) StateCopy(workingstate, ns); mu_next_random.Permute(Perm,0); if (args->multiset_reduction.value) mu_next_random.MultisetSort(); mu_initiator_spi.Permute(Perm,0); if (args->multiset_reduction.value) mu_initiator_spi.MultisetSort(); mu_responder_spi.Permute(Perm,0); if (args->multiset_reduction.value) mu_responder_spi.MultisetSort(); mu_initiator_num_spis.Permute(Perm,0); if (args->multiset_reduction.value) mu_initiator_num_spis.MultisetSort(); mu_net.Permute(Perm,0); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,0); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } while (Perm.NextPermutation()) { if (ns != workingstate) StateCopy(workingstate, ns); mu_next_random.Permute(Perm,0); if (args->multiset_reduction.value) mu_next_random.MultisetSort(); mu_initiator_spi.Permute(Perm,0); if (args->multiset_reduction.value) mu_initiator_spi.MultisetSort(); mu_responder_spi.Permute(Perm,0); if (args->multiset_reduction.value) mu_responder_spi.MultisetSort(); mu_initiator_num_spis.Permute(Perm,0); if (args->multiset_reduction.value) mu_initiator_num_spis.MultisetSort(); mu_net.Permute(Perm,0); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,0); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } } StateCopy(workingstate,&temp); return FALSE; } } if (!args->symmetry_reduction.value && args->multiset_reduction.value) { if (ns != workingstate) StateCopy(workingstate, ns); mu_next_random.MultisetSort(); mu_initiator_spi.MultisetSort(); mu_responder_spi.MultisetSort(); mu_initiator_num_spis.MultisetSort(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } StateCopy(workingstate,&temp); return FALSE; } return (p.compare(ns)); } /******************** Canonicalization by fast exhaustive generation of all permutations ********************/ void SymmetryClass::Exhaustive_Fast_Canonicalize(state* s) { int i; static state temp; Perm.ResetToExplicit(); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_next_random.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_initiator_spi.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_responder_spi.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_initiator_num_spis.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_net.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_int.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); }; /******************** Canonicalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and fast exhaustive generation of all permutations for other variables ********************/ void SymmetryClass::Heuristic_Fast_Canonicalize(state* s) { int i; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_initiator_spi.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_responder_spi.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_net.MultisetLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_int.MultisetLimit(Perm); } }; /******************** Canonicalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and fast exhaustive generation of all permutations for other variables and use less local memory ********************/ void SymmetryClass::Heuristic_Small_Mem_Canonicalize(state* s) { unsigned long cycle; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_initiator_spi.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_responder_spi.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_net.MultisetLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_int.MultisetLimit(Perm); } }; /******************** Normalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and for all other variables, pick any remaining permutation ********************/ void SymmetryClass::Heuristic_Fast_Normalize(state* s) { int i; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_initiator_spi.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_responder_spi.SimpleLimit(Perm); } }; /******************** Include ********************/ #include "mu_epilog.inc"