What does well-typed mean? I am currently studying Cryptography and I don't really understand what does 'well-typed' mean when talking about secure cryptographic protocols. I can't find any reasonable explanation on the internet either.

It would be great if someone could give definition and maybe example.

For example quote from “prosecco.gforge.inria.fr”: 


  The basic soundness theorem for the type system states that well-typed process do not reveal their secrets." So what is 'well-typed'?
“Well-typed” relates to a type system. This is a general concept in computer science, the usage here is an example of the general concept and is not specific to cryptography. “Well-typed” does not refer to a cryptographic protocol, but to a theory (model) in which a protocol is described.

A type system is a way to assign properties (called types) to components of programs. For example, a type system might make stipulations like the following:


The program fragment int x; declares a variable called x whose type is “integer”.
Integer literals such as 3 and 42 are expressions of the type “integer”.
String literals such as "hello" and "42" are expressions of the type “string”.
If x is a variable with the type “integer”, then x is an expression of the type “integer”.
If E_1 and E_2 are expressions of the type “integer”, then E_1 + E_2 is an expression of the type “integer”.
If x is a variable which has the type “integer” and E is an expression of the type “integer”, then x := E is a valid (well-typed) program. If E does not have the type “integer”, then x := E is an invalid (ill-typed) program.


The ultimate goal of most type systems is to declare that certain programs are well-typed, i.e. that they're correct (with respect to this type system). They achieve this by assigning types to program fragments, to variables, to functions, etc. and detecting conflicts (e.g. trying to assign a string value to an integer variable, trying to apply a function to an argument which is not of a type that it can handle). Most programming languages have a type system, such that ill-typed programs are rejected, either at run time (dynamic typing) or at compile time (static typing).

Type systems can encompass a wide variety of properties. The most common class of property has to do with the structure of data, such as:


“this is an integer“
“this is an integer modulo $2^{32}$ using the smallest nonnegative representative”
“this is a list of integers”
“this is a function that takes an integer as argument and returns an integer”


But type systems can describe arbitrarily complex properties. That makes it harder to decide whether a program has a correct type, but makes the type system provide more useful information. Here are some example properties that a sufficiently sophisticated type system might model:


“this is a prime integer”
“this is a list of integers whose length is the value of the expression x + y”
“this is a terminating function that takes an integer as argument and returns an integer”
“this function $f$ takes two arguments $(p,s)$ and returns two values $(p',s')$, such that the value of $p'$ depends only on $p$ and not on $s$”


In that last example, you can see a security property emerging: if we think of $p$ and $p'$ as public values and $s$ and $s'$ as secret values, the property states that public values do not depend on secret values. In other words, the function $f$ preserves the confidentiality of secret values.

Soundness relates a type system with execution rules (an execution semantics) for the programming language. It is a formal property that states that if a program is well-typed, then all runtime states of the program (as modeled in the semantics) are also well-typed. Most type systems are designed to be sound for the usual semantics of the language. This way, information given by the type system about the program translates into information about the program's execution. 

The paper that you're reading defines a type system for processes (describing communication protocols) that classifies messages according to which principals know their content. The execution rules describe the propagation of messages. The soundness of the type system means that the initial classification of who knows what is preserved during the execution of the protocol. This holds for well-typed processes, i.e. processes for which the classification (typing) rules give a result. Thus processes that are classified as valid by the type system will not reveal secret data during their execution.