Package anbxj

Class AnB_Protocol<S extends Enum<?>,R extends Enum<?>,ST>

java.lang.Object
anbxj.AnB_Protocol<S,R,ST>
Type Parameters:
S - class steps
R - roles class
ST - type of per-session state (used by generated roles)

public abstract class AnB_Protocol<S extends Enum<?>,R extends Enum<?>,ST> extends Object
AnB Protocol: an abstract class for defining AnB protocols
  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected Map<String,String>
    Mapping of aliases for protocol roles.
    The cryptographic engine
    protected static final AnBx_Layers
    The layer for debugging purposes.
    Mapping of session names to session instances.
    protected AnBx_Agent
    the identity of the agent
    protected String
    The name of the protocol.
    protected R
    The role of the protocol.
    protected final AtomicLong
    Per-instance session ID counter (one per role instance).
    protected String
    The path for sharing data in the protocol.
    A byte array of zeros used in the protocol.
  • Constructor Summary

    Constructors
    Modifier
    Constructor
    Description
     
    Default constructor
    protected
    AnB_Protocol(R role, String name, String sharepath, Crypto_EncryptionEngine ee)
    Constructs a protocol instance with the specified role, agent name, shared‑data path, and cryptographic engine.
  • Method Summary

    Modifier and Type
    Method
    Description
    protected void
    Abort the protocol with a specified error message
    protected void
    abort(String msg, Exception e, long sessionID)
    Abort the protocol with a specified error message, exception, and session ID.
    protected abstract ST
    createSessionState(long sessionID)
    Creates the per-session state object for a new protocol session.
    protected boolean
    eqCheck(Object obj1, Object obj2)
    Checks if two objects are equal without a specific label.
    protected boolean
    eqCheck(Object obj1, Object obj2, boolean mayfail)
    Checks if two objects are equal with a flag indicating possible failure.
    protected boolean
    eqCheck(String label, Object obj1, Object obj2)
    Checks if two objects are equal with a specified label.
    protected boolean
    eqCheck(String label, Object obj1, Object obj2, boolean mayfail)
    Checks if two objects are equal with a specified label and a flag indicating possible failure.
    protected abstract void
    executeStep(AnB_Session session, ST state, S step)
    Abstract method to execute a step in the AnB protocol.
    protected String
    Get the alias for the current role.
    protected long
    Returns the number of sessions that are currently being executed.
    protected abstract void
    Abstract method to initialise the AnB protocol.
    protected boolean
    Perform an inverse check without a label for a single object.
    protected boolean
    invCheck(Object obj, Class<?> cls)
    Perform an inverse check without a label for an object and a class.
    protected boolean
    invCheck(Object obj1, Object obj2)
    Perform an inverse check without a label for two objects.
    protected boolean
    invCheck(String label, Object obj)
    Perform an inverse check with a label for a single object.
    protected boolean
    invCheck(String label, Object obj, Class<?> cls)
    Perform an inverse check with a label for an object and a class.
    protected boolean
    invCheck(String label, Object obj1, Object obj2)
    Perform an inverse check with a label for two objects.
    protected boolean
    Get the value of abortOnFail.
    protected boolean
    Return the value of checkAnyway
    protected long
    Returns the next unique session ID (thread-safe).
    protected boolean
    noteqCheck(Object obj1, Object obj2)
    Checks if two objects are not equal without a specific label.
    protected boolean
    noteqCheck(String label, Object obj1, Object obj2)
    Checks if two objects are not equal with a specified label.
    void
    Runs the protocol with the given maps of sessions and aliases.
    protected void
    runProtocol(Map<String,AnB_Session> channelTemplates)
    Runs the protocol using the session count defined in the crypto configuration.
    protected void
    runProtocol(Map<String,AnB_Session> channelTemplates, long sessions)
    Runs the protocol using the supplied channel templates and session count.
    protected abstract void
    runSession(Map<String,AnB_Session> channelMap, ST state)
    Executes the complete protocol for one logical session.
    protected boolean
    seen(Object obj)
    Checks if the specified object has been seen.
    protected boolean
    seen(String label, Object obj)
    Checks if the specified object has been seen with a given label.
    protected void
    setAbortOnFail(boolean abortOnFail)
    Set the value of abortOnFail.
    protected void
    setCheckAnyway(boolean checkAnyway)
    Set the value of checkAnyway.
    protected void
    status(S step)
    Outputs the status of the protocol with a specific step.
    protected void
    status(S step, Object payload)
    Outputs the status of the protocol with a specific step and payload.
    protected void
    Outputs the status label for a check with a given label.
    protected boolean
    Checks if the given object is a well-formed formula (WFF) without a specific label.
    protected boolean
    wffCheck(Object obj, Class<?> cls)
    Checks if the given object is a well-formed formula (WFF) with a specified class type.
    protected boolean
    wffCheck(String label, Object obj)
    Checks if the given object is a well-formed formula (WFF) with a specified label.
    protected boolean
    wffCheck(String label, Object obj, Class<?> cls)
    Checks if the given object is a well-formed formula (WFF) with a specified label and class type.

    Methods inherited from class java.lang.Object

    clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
  • Field Details

    • layer

      protected static final AnBx_Layers layer
      The layer for debugging purposes.
    • name

      protected String name
      The name of the protocol.
    • sharepath

      protected String sharepath
      The path for sharing data in the protocol.
    • role

      protected R extends Enum<?> role
      The role of the protocol.
    • me

      protected AnBx_Agent me
      the identity of the agent
    • ee

      The cryptographic engine
    • aliases

      protected Map<String,String> aliases
      Mapping of aliases for protocol roles.
    • lbs

      protected Map<String,AnB_Session> lbs
      Mapping of session names to session instances.
    • sessionID

      protected final AtomicLong sessionID
      Per-instance session ID counter (one per role instance).
    • zero

      protected Crypto_ByteArray zero
      A byte array of zeros used in the protocol.
  • Constructor Details

    • AnB_Protocol

      public AnB_Protocol()
      Default constructor
    • AnB_Protocol

      protected AnB_Protocol(R role, String name, String sharepath, Crypto_EncryptionEngine ee)
      Constructs a protocol instance with the specified role, agent name, shared‑data path, and cryptographic engine.
      Parameters:
      role - the role this instance plays
      name - the agent name
      sharepath - the directory where shared variables are stored
      ee - the pre‑configured cryptographic engine
  • Method Details

    • nextSessionID

      protected long nextSessionID()
      Returns the next unique session ID (thread-safe).
      Returns:
      the next unique session ID
    • run

      public void run(Map<String,AnB_Session> lbs, Map<String,String> aliases)
      Runs the protocol with the given maps of sessions and aliases.
      Parameters:
      lbs - Mapping of session names to session instances.
      aliases - Mapping of aliases for protocol roles.
    • executeStep

      protected abstract void executeStep(AnB_Session session, ST state, S step)
      Abstract method to execute a step in the AnB protocol.
      Parameters:
      session - the session to use
      state - the per-session state object (specific to the protocol)
      step - the step to execute
    • init

      protected abstract void init()
      Abstract method to initialise the AnB protocol.
    • createSessionState

      protected abstract ST createSessionState(long sessionID)
      Creates the per-session state object for a new protocol session.

      The returned object must be initialised with the given session identifier and any global (shared) variables that were loaded during init(). This method is called once for each logical session before runSession(Map, Object).

      Parameters:
      sessionID - the unique identifier assigned to this session
      Returns:
      a newly created session-state instance, never null
    • runSession

      protected abstract void runSession(Map<String,AnB_Session> channelMap, ST state)
      Executes the complete protocol for one logical session.

      The supplied channelMap contains every channel required by the role, already opened and keyed by the channel name used in the protocol definition (e.g. "ROLE_M_channel_ROLE_C_Server_Insecure"). Implementations must run all steps of the protocol on the appropriate channel(s), using the given session-state object.

      Parameters:
      channelMap - a mapping from channel name to an open session; never null, and no entry is null
      state - the per-session state previously created by createSessionState(long); never null
    • isAbortOnFail

      protected boolean isAbortOnFail()
      Get the value of abortOnFail.
      Returns:
      true if the protocol should abort on failure, false otherwise.
    • setAbortOnFail

      protected void setAbortOnFail(boolean abortOnFail)
      Set the value of abortOnFail.
      Parameters:
      abortOnFail - The value to set for abortOnFail.
    • isCheckAnyway

      protected boolean isCheckAnyway()
      Return the value of checkAnyway
      Returns:
      the checkAnyway
    • setCheckAnyway

      protected void setCheckAnyway(boolean checkAnyway)
      Set the value of checkAnyway.
      Parameters:
      checkAnyway - The value to set for checkAnyway.
    • abort

      protected void abort(String msg)
      Abort the protocol with a specified error message
      Parameters:
      msg - The error message.
    • abort

      protected void abort(String msg, Exception e, long sessionID)
      Abort the protocol with a specified error message, exception, and session ID.
      Parameters:
      msg - The error message.
      e - The exception (can be null).
      sessionID - The session ID.
    • getAlias

      protected String getAlias()
      Get the alias for the current role.
      Returns:
      The alias for the current role.
    • invCheck

      protected boolean invCheck(String label, Object obj1, Object obj2)
      Perform an inverse check with a label for two objects.
      Parameters:
      label - The label for the check.
      obj1 - The first object.
      obj2 - The second object.
      Returns:
      True if the check is successful, false otherwise.
    • invCheck

      protected boolean invCheck(String label, Object obj, Class<?> cls)
      Perform an inverse check with a label for an object and a class.
      Parameters:
      label - The label for the check.
      obj - The object.
      cls - The class to check against.
      Returns:
      True if the check is successful, false otherwise.
    • invCheck

      protected boolean invCheck(String label, Object obj)
      Perform an inverse check with a label for a single object.
      Parameters:
      label - The label for the check.
      obj - The object.
      Returns:
      True if the check is successful, false otherwise.
    • invCheck

      protected boolean invCheck(Object obj1, Object obj2)
      Perform an inverse check without a label for two objects.
      Parameters:
      obj1 - The first object.
      obj2 - The second object.
      Returns:
      True if the check is successful, false otherwise.
    • invCheck

      protected boolean invCheck(Object obj, Class<?> cls)
      Perform an inverse check without a label for an object and a class.
      Parameters:
      obj - The object.
      cls - The class to check against.
      Returns:
      True if the check is successful, false otherwise.
    • invCheck

      protected boolean invCheck(Object obj)
      Perform an inverse check without a label for a single object.
      Parameters:
      obj - The object.
      Returns:
      True if the check is successful, false otherwise.
    • wffCheck

      protected boolean wffCheck(String label, Object obj)
      Checks if the given object is a well-formed formula (WFF) with a specified label.
      Parameters:
      label - the label for the check
      obj - the object to be checked
      Returns:
      true if the object is a well-formed formula, false otherwise
    • wffCheck

      protected boolean wffCheck(String label, Object obj, Class<?> cls)
      Checks if the given object is a well-formed formula (WFF) with a specified label and class type.
      Parameters:
      label - the label for the check
      obj - the object to be checked
      cls - the expected class type for the object
      Returns:
      true if the object is a well-formed formula, false otherwise
    • wffCheck

      protected boolean wffCheck(Object obj)
      Checks if the given object is a well-formed formula (WFF) without a specific label.
      Parameters:
      obj - the object to be checked
      Returns:
      true if the object is a well-formed formula, false otherwise
    • wffCheck

      protected boolean wffCheck(Object obj, Class<?> cls)
      Checks if the given object is a well-formed formula (WFF) with a specified class type.
      Parameters:
      obj - the object to be checked
      cls - the expected class type for the object
      Returns:
      true if the object is a well-formed formula, false otherwise
    • noteqCheck

      protected boolean noteqCheck(String label, Object obj1, Object obj2)
      Checks if two objects are not equal with a specified label.
      Parameters:
      label - the label for the check
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      Returns:
      true if the objects are not equal, false otherwise
    • noteqCheck

      protected boolean noteqCheck(Object obj1, Object obj2)
      Checks if two objects are not equal without a specific label.
      Parameters:
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      Returns:
      true if the objects are not equal, false otherwise
    • eqCheck

      protected boolean eqCheck(String label, Object obj1, Object obj2)
      Checks if two objects are equal with a specified label.
      Parameters:
      label - the label for the check
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      Returns:
      true if the objects are equal, false otherwise
    • eqCheck

      protected boolean eqCheck(String label, Object obj1, Object obj2, boolean mayfail)
      Checks if two objects are equal with a specified label and a flag indicating possible failure.
      Parameters:
      label - the label for the check
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      mayfail - flag indicating whether the check may fail
      Returns:
      true if the objects are equal, false otherwise
    • eqCheck

      protected boolean eqCheck(Object obj1, Object obj2)
      Checks if two objects are equal without a specific label.
      Parameters:
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      Returns:
      true if the objects are equal, false otherwise
    • eqCheck

      protected boolean eqCheck(Object obj1, Object obj2, boolean mayfail)
      Checks if two objects are equal with a flag indicating possible failure.
      Parameters:
      obj1 - the first object to be compared
      obj2 - the second object to be compared
      mayfail - flag indicating whether the check may fail
      Returns:
      true if the objects are equal, false otherwise
    • seen

      protected boolean seen(String label, Object obj)
      Checks if the specified object has been seen with a given label.
      Parameters:
      label - the label for the check
      obj - the object to be checked
      Returns:
      true if the object has been seen before, false otherwise
    • seen

      protected boolean seen(Object obj)
      Checks if the specified object has been seen.
      Parameters:
      obj - the object to be checked
      Returns:
      true if the object has been seen before, false otherwise
    • status

      protected void status(S step)
      Outputs the status of the protocol with a specific step.
      Parameters:
      step - the step in the protocol
    • statusLabel

      protected void statusLabel(String label)
      Outputs the status label for a check with a given label.
      Parameters:
      label - the label for the check
    • status

      protected void status(S step, Object payload)
      Outputs the status of the protocol with a specific step and payload.
      Parameters:
      step - the step in the protocol
      payload - the payload associated with the step
    • getSessions

      protected long getSessions()
      Returns the number of sessions that are currently being executed. This is a convenience proxy for the value stored in the crypto configuration.
      Returns:
      the total session count
    • runProtocol

      protected void runProtocol(Map<String,AnB_Session> channelTemplates)
      Runs the protocol using the session count defined in the crypto configuration.
      Parameters:
      channelTemplates - a map from channel name to its session template
    • runProtocol

      protected void runProtocol(Map<String,AnB_Session> channelTemplates, long sessions)
      Runs the protocol using the supplied channel templates and session count. Automatically chooses the execution mode (multi-threaded server, parallel clients, or single-threaded) based on the crypto configuration.
      Parameters:
      channelTemplates - a map from channel name to its session template (the sessions passed via lbs)
      sessions - the total number of sessions to execute