Man Linux: Main Page and Category List


       lysa2mcrl2 - Convert Typed LySa to mCRL2


       lysa2mcrl2 [OPTION]... [INFILE [OUTFILE]]


       Converts  a security protocol specified in Typed LySa in INFILE into an
       mCRL2 process specification in OUTFILE.  If  OUTFILE  is  not  present,
       stdout is used. If INFILE is not present, stdin is used.


       OPTION can be any of the following:

       -aNUM, --attacker-index=NUM
              Assume  that  the  attacker  may be a legitimate (but dishonest)
              agent participating in the protocol, corresponding to meta-level
              index number NUM.  The effect of setting this option is that the
              attacker’s crypto-point CPDY is added to all  dest/orig  clauses
              where  one or more of the current meta-variables equal NUM. This
              option corresponds to the attackerIndex option of the LySa tool.

       -l, --lysa
              Converts  a  Typed  LySa process to LySa and not to mCRL2. Makes
              all other non-standard options illegal.

       -i[PREFIX], --prefix-idents[=PREFIX]
              Prefixes all identifiers found in  the  Typed  LySa  process  in
              INPUT  with an underscore or with PREFIX to prevent clashes with
              mCRL2 keywords or identifiers used in the preamble.

       -s[STRATEGY], --strategy[=STRATEGY]
              Apply conversion using the specified strategy:
                ’straightforward’  for  a  straightforward  conversion;   most
              likely this yields
                an infinite state space.
                ’symbolic’  for a conversion in which symbolic representations
              are chosen to
                represent possibly infinite numbers of ciphertexts  and  names

       -z, --zero-action
              Generates  a  ’zero’ action before deadlocking when Typed LySa’s
              empty process (0) is encountered. This is a valid action in  the
              supplied  preambles.  This  option  may  help  to  differentiate
              between a deadlock and a correct protocol run termination.

       Standard options:

       -q, --quiet
              do not display warning messages

       -v, --verbose
              display short intermediate messages

       -d, --debug
              display detailed intermediate messages

       -h, --help
              display help information

              display version information


       Written by Egbert Teeselink.


       Report bugs at <>.


       Copyright © 2010 Technische Universiteit Eindhoven.
       This is free software.  You may redistribute copies  of  it  under  the
       terms         of        the        Boost        Software        License
       <>.  There is NO WARRANTY,  to  the
       extent permitted by law.


       See              also             the             manual             at

lysa2mcrl2 mCRL2 toolset July 2010 Mayv2010ment)