User manual/lysa2mcrl2

From MCRL2

User manual

Tool manual pages chi2mcrl2 diagraphica formcheck grapemcrl2 lps2lts lps2pbes lps2torx lpsactionrename lpsbinary lpsbisim2pbes lpsconfcheck lpsconstelm lpsinfo lpsinvelm lpsparelm lpsparunfold lpspp lpsrealelm lpsrewr lpssim lpssumelm lpssuminst lpsuntime lpsxsim lts2lps ltscompare ltsconvert ltsgraph ltsinfo ltsmin ltsview lysa2mcrl2 mcrl22lps mcrl2-gui mcrl2i pbesinst pbes2bool pbesconstelm pbesinfo pbesparelm pbespareqelm pbespgsolve pbespp pbesrewr pnml2mcrl2 squadt tbf2lps tracepp txt2lps txt2pbes

Contents

Convert a Typed LySa specification to an mCRL2 process specification. (EXPERIMENTAL)

Contents 1 Synopsis 2 Short Description 3 Options 4 Author 5 Reporting bugs

Synopsis

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

Short 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 [1].

---

ltsview

mcrl22lps