---
name: "lysa2mcrl2"
section: "1"
platform: "linux"
package: "mcrl2"
version: "201007~rc1-1"
release: "Debian 6.0 (Squeeze)"
platforms: ["linux"]
url: "https://new.carta.tech/lysa2mcrl2"
---

# lysa2mcrl2(1)

Convert Typed LySa to mCRL2

## 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:

  - **-a***NUM*, **--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.

- **--mcrl2-gui**

  outputs information about the visual representation of this option in the mCRL2  GUI

- **-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\>.