NAME
lysa2mcrl2 - Convert Typed LySa to mCRL2
SYNOPSIS
lysa2mcrl2 [OPTION]... [INFILE [OUTFILE]]
DESCRIPTION
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.
OPTIONS
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
(default).
-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
--version
display version information
AUTHOR
Written by Egbert Teeselink.
REPORTING BUGS
Report bugs at <http://www.mcrl2.org/issuetracker>.
COPYRIGHT
Copyright © 2010 Technische Universiteit Eindhoven.
This is free software. You may redistribute copies of it under the
terms of the Boost Software License
<http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the
extent permitted by law.
SEE ALSO
See also the manual at
<http://www.mcrl2.org/mcrl2/wiki/index.php/User_manual/lysa2mcrl2>.
lysa2mcrl2 mCRL2 toolset July 2010 Mayv2010ment)